任意ランクの多相
RankNTypes
ExplicitForAllを含む
6.8.1以降
任意ランクの型を許す.
Rank2Types
6.8.1以降
RankNTypesの非推奨な別名.
GHCの型システムは型の中での任意ランクの明示的な全称量化をサポートしている.例えば,以下の型は全て問題ない.
code:ar01.hs
f1 :: forall a b. a -> b -> a
g1 :: forall a b. (Ord a, Eq b) => a -> b -> a
f2 :: (forall a. a - >a) -> Int -> Int
g2 :: (forall a. Eq a => a -> a -> Bool) -> Int -> Int f3 :: ((forall a. a -> a) -> Int) -> Bool -> Bool
f4 :: Int -> (forall a. a -> a)
ここで、f1とg1はランク1の型を持ち,標準的なHaskellでも書くことができる(例:f1 :: a -> b -> a).このforallは,Haskellによって暗黙に加えられている全称量化を明示的にしている.
関数f2と関数g2はランク2の型を持つ.つまり,forallが関数矢印の左側にあるということである(訳注:ここで言ってるのは,(->)の左側に全称量化された型が存在するということ.f2の例で言えば,(forall a. a-> a)のことを指しており,カッコ内である意味で局所的に全称量化されているということである).g2の例が示すように,関数の矢印の左にある多相型はオーバーロードできる.
関数f3はランク3の型を持つ.というのも,関数の矢印の左にランク2の型を持っているからだ.
RankNTypes拡張(これはExplicitForAllを含む)は,より高ランクの型を用いることを可能にする.つまり,forallを関数の矢印の中で任意に深くネストできるようになる.例えば,型クラスコンテキストを含む,forall-type(「型構造」(type scheme)とも呼ばれる)は,以下の状況で合法になる.
関数の矢印の左や右において(右の例:f4)
データ型宣言において,コンストラクタの引数として,またはフィールドの型として.例えば,前述のf1・f2・f3・g1・g2はどれもフィールドの型シグネチャとしても合法になる.
暗黙なパラメータの型として.
RankNTypes拡張は,矢印の右にforallやコンテキストのある型(例:f :: Int -> forall a. a->aやg :: Int -> Ord a => a -> a)を書くのにも必要である.このような型は厳密にはランク1なのだが,明らかにHaskell 98の仕様の範囲ではなく,このような型を書けるようにするのに別の拡張をわざわざ追加する手間をかけるまでもないと思われる.
特に,data宣言・newtype宣言内でコンストラクタの引数は任意のランクの多相型であることが許される.次節の例を参照せよ.それでも宣言された型は常に単相的であることに注意せよ.GHCはデフォルトでは型変数を多相型にインスタンス化しないので,これは重要である.(非可述多相) 旧式の言語拡張PolymorphicComponentsとRank2TypesはRankNTypesの同義である.これらはかつてより細かな区別を指定していたが,今やGHCはそれらを区別しない(本当は非推奨であることを知らせるwarningを出すべきなのだろうが,出さない.これは純粋に,ライブラリ作者が古いフラグ指定を変える必要がないようにするためである).
例
以下は,データコンストラクタが多相的な引数の型を持つdata宣言・newtype宣言の例である.
code:ar02.hs
data T a = T1 (forall b. b -> b -> b) a
data MonadT m = MkMonad { return :: forall a. a -> m a,
bind :: forall a b. m a -> (a -> m b) -> m b
}
newtype Swizzle = MkSwizzle (forall a. Ord a => a -> a) コンストラクタはランク2の型を持つ.
code:ar03.hs
T1 :: forall a. (forall b. b -> b -> b) -> a -> T a
MkMonad :: forall m. (forall a. a -> m a)
-> (forall a b. m a -> (a -> m b) -> m b)
-> MonadT m
MkSwizzle :: (forall a. Ord a => a -> a) -> Swizzle 過去のバージョンのGHCでは,明示的な型クラス制約がある場合はコンストラクタの型の中でforallを省くことが許されていた.例えば,
code:ar04.hs
newtype Swizzle' = MkSwizzle' (Ord a => a -> a) GHC8.0以降では,このMkSwizzle'のような宣言はout-of-scopeエラーとなる.
型シグネチャに関しては,オーバーロードされていない型についても暗黙の量化が発生する.ゆえに,以下のように書くと,
code:ar05.hs
f :: (a -> a) -> a
以下のように書いたのと全く同様になる.
code:ar06.hs
f :: forall a. (a -> a) -> a
要するに、型変数aがスコープにないため,aが暗黙に全称量化されるのである.
型T1・MonadT・Swizzleを持つ値を構成するには,通常と同様,コンストラクタを適切な値に適用することで行う.例えば,
code:ar07.hs
a1 :: T Int
a1 = T1 (\x y -> x) 3
a2, a3 :: Swizzle
a2 = MkSwizzle sort
a3 = MkSwizzle reverse
a4 :: MonadT Maybe
a4 = let r x = Just x
b m k = case m of
Just y -> k y
Nothing -> Nothing
in
MkMonad r b
mkTs :: (forall b. b -> b -> b) -> a -> T a 引数の型は,これまた通常通り,要求されている型よりも一般的であることが許される.このことを示す例がMkSwizzle reverseである(reverseはOrd制約を要求しない).
パターンマッチを用いる際には,束縛された変数は多相型を持つことが許される.例えば,
code:ar08.hs
f :: T a -> a -> (a, Char)
f (T1 w k) x = (w k x, w 'c' 'd')
g :: (Ord a, Ord b) => Swizzle -> a -> (a -> b) -> b g (MkSwizzle s) xs f = s (map f (s xs))
h :: MonadT m -> m a -> m a h m [] = return m []
h m (x:xs) = bind m x $ \y ->
bind m (h m xs) $ \ys ->
return m (y:ys)
関数hの中では,パターンマッチを用いるのではなく,レコードセレクタreturnやbindを用いることでMonadTデータ構造から多層的なbind関数とreturn関数を抽出している.
型推論
一般に,任意のランクの型における型推論は決定不能である.GHCはOderskyとLauferによって提案されたアルゴリズム(“Putting type annotations to work”, POPL‘96)を用いて,プログラマからいくらかの助けを要求することで決定性のあるアルゴリズムとなるようにしている.その「いくらかの助け」を形式的に定めた仕様はまだ存在しないが,原則は以下の通りである.
ラムダ束縛かcase束縛されている変数xについて,プログラマが明示的に多相的な型をxに与えるか,さもなくばGHCの型推論はxの型の中に全くforallが無いと仮定する.
「明示的に型をxに与える」とはどういう意味か?パターン型シグネチャ(字句的スコープを持つ型変数)を使って,xの型シグネチャを直接与えることでそれをすることができる.したがって, code:ar09.hs
\ f :: (forall a. a->a) -> (f True, f 'c')
あるいは、enclosing contextに型シグネチャを与えてもよい。GHCはそれを「押し下げる」ことで変数の型を知ることができる。
code:ar10.hs
(\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)
ここでは,式についている型シグネチャを内側に「押し下げる」ことでfに型シグネチャを与えることができる.同様に,そしてこっちのほうがよくある状況だが,型シグネチャを関数そのものに与えることができる.
code:ar11.hs
h :: (forall a. a->a) -> (Bool,Char)
h f = (f True, f 'c')
ラムダ束縛されている変数がコンストラクタの引数である場合,型シグネチャを与える必要はない.以下は,さっき見た例である.
code:ar12.hs
f :: T a -> a -> (a, Char)
f (T1 w k) x = (w k x, w 'c' 'd')
ここでは,型シグネチャをwに与える必要はない.というのも,wがコンストラクタT1の引数であることがGHCに十分な情報を与えるからである.
暗黙の量化
GHCは以下のように暗黙の量化を行う.ユーザによって書かれた型の最も外側のレベル(だけ)では,明示的なforallがないときかつそのときに限り,型の中で言及されている全ての既にスコープに入っていない型変数をGHCは探し,それらを全称量化する.例えば,以下のペアらはそれぞれ等価である.
code:ar13.hs
f :: a -> a
f :: forall a. a -> a
g (x::a) = let
h :: a -> b -> b
h x y = y
in ...
g (x::a) = let
h :: forall b. a -> b -> b
h x y = y
in ...
GHCは暗黙の量化子をユーザ定義型の最も外のレベルに必ず加えることに注意せよ.つまり,可能な限り内側な量化場所を探したりはしない.例えば,
code:ar14.hs
f :: (a -> a) -> Int
-- というのは
f :: forall a. (a -> a) -> Int
-- ↑のことであって↓のことではない
f :: (forall a. a -> a) -> Int
g :: (Ord a => a -> a) -> Int
-- というのは
g :: forall a. (Ord a => a -> a) -> Int
-- ↑のことであって↓のことではない
g :: (forall a. Ord a => a -> a) -> Int
後者の型が欲しい場合,forallを明示的に書くことができる.実際,ランク2の型についてはそうすることが強く推奨される.
ときによっては,そもそも「最も外側のレベル」というもの自体がないということもある.そういう場合には暗黙の量化は起こらない.
code:ar15.hs
data PackMap a b s t = PackMap (Monad f => (a -> f b) -> s -> f t)
これは拒否される.なぜなら、右辺の型にとって「最も外側のレベル」というものはなく(当然ながら,PackMapに追加でパラメータを足すなどということをしてしまったらとんでもないのでダメだ(訳注:fが存在量化されていてほしいのでfをパラメータとして足したら意味がないという意味か?)),ゆえに暗黙の量化は起こらず,そして宣言が拒否されるからだ(「fはスコープにない」というメッセージとともに).解決策:明示的なforallを使おう:
code:ar16.hs
data PackMap a b s t = PackMap (forall f. Monad f => (a -> f b) -> s -> f t)