7.13. 型システムへのその他の拡張

7.13.1. 明示的な全称量化(forall)

Haskellの型シグネチャは暗黙に量化される。言語オプション-XExplicitForAllが使われている場合、これが正確にどういう意味なのかをforallキーワードを使って言うことができる。例えば、

g :: b -> b

は、次のものを意味している。

g :: forall b. (b -> b)

この二つは同じものとして扱われる。

もちろん、forallはキーワードになる。型変数としてforallを使うことはもはやできないのである。

7.13.2. 型シグネチャの文脈

-XFlexibleContextsフラグを使うと、型シグネチャ中の型クラス制約が(class type-variable)または(class (type-variable type1 type2 ... typen))という形でなければならないという、Haskell 98の制限を撤廃する。-XFlexibleContextsが有効な場合、以下のような型シグネチャは完全に正しい。

g :: Eq [a] => ...
g :: Ord (T a ()) => ...

-XFlexibleContextsフラグは、クラス宣言(7.6.1.2. クラス宣言のスーパークラス)およびインスタンス宣言(7.6.3.3. インスタンス文脈に関する規則の緩和)における同様の制約も撤廃する。

7.13.3. 曖昧な型、および曖昧性検査

ユーザが書いた個々の型シグネチャは、曖昧性検査の対象になる。曖昧性検査は、決して呼べない関数を検出し、エラーにする。例を挙げる。

f :: C a => Int

fのあらゆる呼び出しが曖昧な制約を発生させるので、これを合法に呼ぶことができない、というのが考え方である。実際、曖昧性検査の唯一の目的は、決して呼べない関数について報告することである。曖昧性検査を完全に省略しても、それが健全性を犠牲にすることはないが、曖昧性エラーを呼び出し地点まで遅らせることになる。言語拡張-XAllowAmbiguousTypesは実際に曖昧性検査を無効にする。

ある関数が曖昧かどうかは微妙な問題になることがある。次の、関数従属を使った例を考えよ。

class D a b | a -> b where ..
h :: D Int b => Int 

呼び出し地点において、Intbを固定する可能性は十分にあるので、このシグネチャは拒絶されるべきでない。さらに、依存性は隠れていることがある。次の例を考えよ。

class X a b where ...
class D a b | a -> b where ...
instance D a b => X [a] b where...
h :: X a b => a -> a

ここで、hの型は、bについて曖昧なように見える。しかし、以下のような合法な呼び出しがある。

...(h [True])...

これは(X [Bool] beta)という制約を発生させる。インスタンスを使うことで、必要な制約は(D Bool beta)になり、これがDの関数従属を通してbetaを固定するのである!

これらの特殊例全てに通底する、指針となる原則がある。以下を考えよ。

f :: type
f = ...blah...

g :: type
g = f

gの定義は、当然型検査を通ると期待されるだろう。つまるところ、fは全く同じ型を持っており、 g=fである。しかし、実際には、fの型が具体化され、具体化された制約が、gのシグネチャで束縛された制約を使って解かれる。よって、型が曖昧である場合、これを解くのは失敗する。例えば、上に出てきたf :: C a => Intの場合を考えよ。

f :: C a => Int
f = ...blah...

g :: C a => Int
g = f

gの定義において、我々はこれを(C alpha)へと具体化し、(C a)から(C alpha)を演繹しようと試み、失敗する。

実は、我々はこれを曖昧性の定義として使っている。すなわち、型tyは、((undefined :: ty) :: ty)が型検査に失敗するとき、かつそのときに限り曖昧である。また、推論された型に対しても良く似た検査が行なわれ、曖昧でないことが確かめられる。

曖昧性検査を無効にする。 関数の型が上記の「指針となる原則」に照らして曖昧であっても、この関数を呼ぶことができる場合がある。例を挙げる。

class D a b where ...
instance D Bool b where ...

strange :: D a b => a -> a
strange = ...blah...

foo = strange True

ここで、strangeの型は曖昧であるが、fooでの呼び出しは問題ない。なぜなら、これは制約(D Bool beta)を要求するが、この制約は(D Bool b)インスタンスによって満たせるからである。よって、言語拡張-XAllowAmbiguousTypesを使うことで、曖昧性検査を切ることができるようになっている。ただし、曖昧性検査が無効になっている場合でも、決して呼ぶことのできない関数についてはGHCは文句を言う。次のような場合である。

f :: (Int ~ Bool) => a -> a

歴史的経緯について。 過去には、GHCは、もっと制限が強く、より場当たり的な条件を型シグネチャに課していた。型forall tv1..tvn (c1, ...,cn) => typeに対して、GHCは(a)全称量化されている型変数tviが全てtypeから「到達可能」であること、(b)全ての制約ciが少なくとも一つの全称量化された型変数tviに言及すること、を要求していた。これらのアドホックな制約は、新しい曖昧性検査によって完全に包含される。以上、歴史的経緯について。

7.13.4. 暗黙パラメタ

暗黙パラメタは、"Implicit parameters: dynamic scoping with static types", J Lewis, MB Shields, E Meijer, J Launchbury, 27th ACM Symposium on Principles of Programming Languages (POPL'00), Boston, Jan 2000に述べられている通りに実装されている。(以下の文書(まだかなり不完全だが)はJeff Lweisによる)

暗黙パラメタのサポートは-XImplicitParamsオプションで有効になる。

変数は、それが関数の呼び出し元の文脈によって束縛されているとき動的に束縛されていると言い、呼ばれた関数の文脈によって束縛されているとき静的に束縛されていると言う。Haskellでは全ての変数が静的に束縛される。変数の動的束縛の概念はLispにまで遡るが、Schemeのような現代的な現れにおいては捨てられることとなった。動的束縛は型のない言語においては非常に混乱的であるし、残念なことに、型のある言語においてもそうである。特に、HaskellのようにHindley-Milterの型システムの付けられた言語は、変数について静的スコープしか認めない。

ところが、Haskellの型クラスの構造に単純な拡張を施すことで、動的束縛を手に入れることができる。基本的には、動的に束縛された変数を使うということを、型への制約として表現するのである。このような制約を使うと、型は(?x::t') => tという形になるが、これは「この関数は動的に束縛された型t'の変数?xを使っている」という意味である。例えば、以下に示すのは、cmpという名前の比較関数で暗黙にパラメタ化されたソート関数の型である。

sort :: (?cmp :: a -> a -> Bool) => [a] -> [a]

動的束縛制約は、型クラス機構に追加された、一つの新しい形の述語に過ぎない。

暗黙パラメタは?xという特殊形式を使った式に現れる。ここでxは有効な識別子である。(例えば、ord ?xは正しい式である)。この要素を使うことで、式の型も影響され、新しい動的束縛制約が導入される。例えば、以下では、明示的にパラメタ化されたsortBy関数を基にして暗黙にパラメタ化されたソート関数を定義している。

sortBy :: (a -> a -> Bool) -> [a] -> [a]

sort   :: (?cmp :: a -> a -> Bool) => [a] -> [a]
sort    = sortBy ?cmp

7.13.4.1. 暗黙パラメタ型制約

動的束縛制約は自動的に伝播される。この点で、型クラス制約と同じ振る舞いである。つまり、ある関数が使われるとき、その関数の暗黙パラメタはその関数を呼んだ関数に受け継がれる。例えば、上記のsort関数は、リストの最小要素を得るのに使うことができる。

least   :: (?cmp :: a -> a -> Bool) => [a] -> a
least xs = head (sort xs)

特に何もしなくても、?cmpパラメタは伝播され、leastのパラメタにもなっている。明示的なパラメタでは、パラメタを明示的に受け渡さなければならないのがデフォルトであるのに対し、暗黙パラメタでは、常に伝播するのがデフォルトである。

暗黙パラメタ型制約と通常のクラス制約の違いは以下の通りである。特定の暗黙パラメタは、何回使われようと、同じ型を持っていなければならない。つまり、(?x, ?x)の型は(?x::a) => (a, a)であり、クラス制約の場合のように(?x::a, ?x::b) => (a, b)となることはない。

クラス宣言やインスタンス宣言の文脈で暗黙パラメタを使うことはできない。例えば、以下の宣言はどちらも不正である。

class (?x::Int) => C a where ...
instance (?x::a) => Foo [a] where ...

理由: 暗黙パラメタとしてどれを選ぶかはどこで関数を呼ぶかに依存する。しかし、インスタンス宣言を「呼ぶ」のはコンパイラによって裏で行われることであり、それがどこで行われているか正確なことを決めるのは難しい。最も簡単なのは、これに違反する型を非合法化することである。

暗黙パラメタ制約は曖昧性を引き起こさない。以下の例を考えてみよう。

f :: (?x :: [a]) => Int -> Int
f n = n + length ?x

g :: (Read a, Show a) => String -> String
g s = show (read s)

ここで、gの型は曖昧であり、受け付けられない。一方、fは問題ない。fの呼び出し地点での?xの束縛は全く曖昧でなく、aの型を固定する。

7.13.4.2. 暗黙パラメタの束縛

暗黙パラメタは通常のletwhere束縛形式を使って束縛することができる。例として、cmpを束縛することでmin関数を定義する。

min :: [a] -> a
min  = let ?cmp = (<=) in least

暗黙パラメタの束縛グループは、通常のHaskellの束縛グループが出現できるところなら、最上位を除いてどこに現れても良い。つまり、let(リスト内包表記、do記法、パターンガード中のものも含む)またはwhere節に現れることができる。以下のことに注意。

  • 暗黙パラメタの束縛グループは暗黙形式の変数への単純束縛の集まり(関数形式は禁止。型シグネチャも禁止)でなければならない。これらの束縛は多相的であってはならず、再帰的であってもならない。

  • 一つのlet式に暗黙パラメタ束縛と通常の束縛を混ぜることはできない。代わりに入れ子になったletを使うこと。(whereの場合はどうしようもない。where節を入れ子にすることはできないので)

  • 単一の束縛グループに複数の暗黙パラメタ束縛を配置することは可能だが、それらは(通常のlet束縛のような)相互再帰的なグループとはみなされない。それらは、非再帰的なグループで、全ての暗黙引数を同時に束縛するものとして扱われる。束縛は入れ子になっておらず、順番を入れ替えてもプログラムの意味は変わらない。例として以下の例を考えよ。

    f t = let { ?x = t; ?y = ?x+(1::Int) } in ?x + ?y

    ?yの束縛中で?xが使われているが、直前の?xの束縛はそこからは「見え」ないので、fの型は以下のようになる。

    f :: (?x::Int) => Int -> Int

7.13.4.3. 暗黙パラメタと多相再帰

次の二つの定義を考えてみよう。

len1 :: [a] -> Int
len1 xs = let ?acc = 0 in len_acc1 xs

len_acc1 [] = ?acc
len_acc1 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc1 xs

------------

len2 :: [a] -> Int
len2 xs = let ?acc = 0 in len_acc2 xs

len_acc2 :: (?acc :: Int) => [a] -> Int
len_acc2 [] = ?acc
len_acc2 (x:xs) = let ?acc = ?acc + (1::Int) in len_acc2 xs

この二つのグループの違いは、二番目のグループではlen_accに型シグネチャが与えられているという点だけである。前者では、len_acc1はその右辺について単相的であり、再帰呼び出しでは暗黙パラメタ?accが渡されない。後者では、len_acc2に型シグネチャがあるので、再帰呼び出しは多相的になり、?accを暗黙パラメタとして取る。よって、GHCiで試してみると、以下の結果が得られる。

Prog> len1 "hello"
0
Prog> len2 "hello"
5

型シグネチャを追加することで結果が劇的に変わってしまった。これはかなり直観に反する現象であり、注意するに値する。

7.13.4.4. 暗黙パラメタと単相性

GHCは、例の恐るべき単相性限定(Haskellレポートの4.5.5節)を暗黙パラメタにも適用する。例として以下を考えよう。

f :: Int -> Int
 f v = let ?x = 0     in
       let y = ?x + v in
       let ?x = 5     in
       y

yの束縛は単相性限定の適用下にあり、一般化されないので、yの型は単なるIntであり、(?x::Int) => Intではない。従って、(f 9)は結果9を返す。yに型シグネチャを追加すると、yの型は(?x::Int) => Intになり、letの本体におけるyの出現は内側の?xの束縛を見ることになるので、(f 9)14を返す。

7.13.5. 明示的に種付けされた量化

Haskellでは全ての型変数の種は推論される。(機械で検査できる)文書化のために、種を明示的に与えるのが良いことがある。これは関数に型シグネチャを与えると良いのと同様である。場合によっては、これが本質的に必要になることもある。例えば、John Hughesは、彼の論文"Restricted Data Types in Haskell" (Haskell Workshop 1999)のなかで、次のようにデータ型を定義しなければならなかった。

data Set cxt a = Set [a]
               | Unused (cxt a -> ())

構築子Unusedは、型変数cxtが正しい種を与えられるようにするためだけに存在する。

GHCでは、このようなことをしなくても、-XKindSignaturesを使えば、型変数が明示的に束縛されるときはいつでも、その型変数の種を直接指定できるようになった。

このフラグによって、以下の場所で種シグネチャを使えるようになる。

  • data宣言。

    data Set (cxt :: * -> *) a = Set [a]
  • type宣言。

    type T (f :: * -> *) = f Int
  • class宣言。

    class (Eq a) => C (f :: * -> *) a where ...
  • 型シグネチャ中のforall

    f :: forall (cxt :: * -> *). Set cxt Int

括弧は必須である。いくつかのスペースも、字句要素を分離するために必要である。(f::*->*)と書いたとすると、「::*->*」はHaskellでは一つの字句要素なので、パースエラーになる。

この拡張の一部として、型に種注釈を加えることもできる。

f :: (Int :: *) -> Int
g :: forall a. a -> (a :: *)

構文は以下のとおり。

atype ::= '(' ctype '::' kind ')

括弧は必須である。

7.13.6. 任意ランク多相

GHCの型システムでは、型に対して任意ランクの明示的な量化が認められる。例えば、以下の例は全て合法である。

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)

ここで、f1g1はランク1の型で、標準のHaskellで書くことができる。(例えば、f1 :: a->b->a)。これらのforallは、Haskellが暗黙に加える全称量化を明示的なものにしている。

関数f2g2の型はランク2である。forallが関数矢印の左にあるからである。g2を見れば分かるとおり、関数矢印の左の多相型は多重定義されていても良い。

関数f3はランク3の型を持っている。関数矢印の左にランク2の型があるからである。

言語オプション-XRankNTypes(-XExplicitForAll(7.13.1. 明示的な全称量化(forall))もこれによって有効になる)は、高いランクの型を有効にする。つまり、関数矢印に必要なだけ深くforallを入れ子にすることができる。特に、forallの付いた型(「型スキーム」とも呼ばれる)は、型クラス文脈も含めて、以下の場所で使える。

  • 関数矢印の左側または右側(例えばf4を見よ)

  • データ型宣言で、構築子の引数として、またはフィールドの型として。例えば、上記のf1,f2,f3,g1,g2はどれも、フィールドの型シグネチャとして合法である。

  • 暗黙パラメタの型として

  • パターン型シグネチャ(7.13.8. 字句的スコープを持つ型変数 を見よ)の中

forallや文脈が矢印の右側にあるような型(たとえば、f :: Int -> forall a. a->aや、g :: Int -> Ord a => a -> a)を使うのにも、-XRankNTypesが必要である。このような型は技術的にはランク1であるが、明らかにHaskell-98でなく、わざわざ別のフラグを用意するほどでもなさそうである。

-XPolymorphicComponentsおよび-XRank2Typesという廃止予定の言語オプションは、-XRankNTypesの別名である。これらは、より細かい違いを指定するために使われていたが、GHCはもはやこの区別をしない。(これらのオプションは本来、廃止予定の警告を発生させるべきであるが、そうはなっていない。これは純粋に、ライブラリ作者が古いフラグ指定を変更する必要をなくすためである)

7.13.6.1. 例

data宣言やnewtype宣言において、構築子の引数の型を量化することができる。いくつか例を挙げる。

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 (Ord a => [a] -> [a])

これらの構築子は、以下のように、ランク2の型を持つ。

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 :: (Ord a => [a] -> [a]) -> Swizzle

明示的な文脈があるならforallを使う必要はないということに注意。例えば、構築子MkSwizzleの第一引数について、引数の型には暗黙に「forall a.」が付いているとみなされる。このような暗黙のforallは、問題の型に言及されているもののスコープにない型変数全てを量化する。(おそらく、構築子の引数では、量化が必要なら明示的にそうすることを必須にした方が良いだろう。Trac #4426を見よ)

型シグネチャと同様に、多重定義されていない型についても暗黙の量化は発生する。次のように書いたとする。

f :: (a -> a) -> a

これは、次のように書いたのと同じである。

f :: forall a. (a -> a) -> a

つまり、型変数bはスコープにないので、暗黙に全称量化される。

T1, MonadT, Swizzleの値を構築するには、通常と同じように、構築子を適切な値に適用すれば良い。例を示す。

    a1 :: T Int
    a1 = T1 (\xy->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]
    mkTs f x y = [T1 f x, T1 f y]

(MkSwizze reverse)の例から分かるように、構築子の引数は、通常と同じく、必要以上に一般的な型をもっていても良い。(reverseOrd制約を必要としない)

パターン照合を使うとき、束縛される変数が多相型を持つことがあり得る。例を示す。

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では、MonadTデータ構造から多相的なbindとreturn関数を抽出するのに、パターン照合ではなく、レコード選択関数であるreturnbindを使っている。

7.13.6.2. 型推論

一般に、任意ランクの型に対する型推論は決定不能である。GHCでは、OderskyとLauferによって提案されたアルゴリズム("Putting type annotations to work", POPL'96)を使って、プログラマの助けを当てにすることでアルゴリズムを決定可能にしている。「プログラマの助け」についての形式的な仕様はまだないが、規則はこうである。

ラムダ束縛された、あるいはcase束縛された変数xについて、プログラマがxに多相的な型を明示的に与えない限り、GHCの型推論は、xの型にforallが含まれないとみなす

xに明示的な型を「与える」とはどういう意味か。まず、xに直接型シグネチャを与えることができる。これにはパターン型シグネチャ(7.13.8. 字句的スコープを持つ型変数 を見よ)を使う。

\ f :: (forall a. a->a) -> (f True, f 'c')

別の方法として、これを取り巻く文脈に型シグネチャを与えることもできる。GHCはこれを「押し進め」て、その変数の型を知ることができる。

(\ f -> (f True, f 'c')) :: (forall a. a->a) -> (Bool,Char)

この例では、式の型シグネチャを内側に押し進めることで、fの型シグネチャを得ることができる。同様に、(こちらの方が良く使われるが)関数自体に型シグネチャを与えても良い。

h :: (forall a. a->a) -> (Bool,Char)
h f = (f True, f 'c')

ラムダ束縛された変数が構築子の引数なら型シグネチャは必要ない。以下は既に見た例である。

f :: T a -> a -> (a, Char)
f (T1 w k) x = (w k x, w 'c' 'd')

ここでwに型シグネチャを与える必要はない。これは構築子T1の引数であり、必要なことは全てこのことから分かる。

7.13.6.3. 暗黙の量化

GHCが暗黙の量化を行う手順は次のとおり。ユーザが書いた型の最上位(のみ)において、明示的なforallがないなら、またその時に限り、その型で言及されているもののスコープにない型変数を調べ上げ、それらを全称量化する。例えば、以下の組は互いに同等である。

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は、可能な最も内側の量化点を探したりしないことに注意。例を示す。

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型についてはそうすることが強く推奨される。

7.13.7. 非叙述的多相

GHCは非叙述的多相(impredicative polymorphism)を扱え、-XImpredicativeTypesで有効になる。これは、多相的関数を多相型で呼ぶことができ、データ構造に多相的な型をパラメタとして与えることができるということである。例を挙げる。

f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
f (Just g) = Just (g [3], g "hello")
f Nothing  = Nothing

Maybe多相的な型である(forall a. [a] -> [a])が与えられていることに注意。

この拡張についての技術的な詳細は、論文Boxy types: type inference for higher-rank types and impredicativityにある。これはICFP 2006に現れた。

7.13.8. 字句的スコープを持つ型変数

GHCは字句的スコープを持つ型変数をサポートしている。これがないと、ある種の型シグネチャは書く方法が全くない。例を挙げる。

f :: forall a. [a] -> [a]
f xs = ys ++ ys
     where
       ys :: [a]
       ys = reverse xs

fの型シグネチャには明示的なforallがあるので、型変数aがスコープに導入されている(7.13.8.2. 宣言型シグネチャ)。forallで束縛された型変数のスコープは、それが付属している値の宣言の全体にわたる。この例では、型変数aのスコープはfの定義全体であり、ysの型シグネチャも含む。Haskell 98では、ysの型を宣言するのは不可能であった。これが可能になったことは、型変数が字句的スコープを持つことの重要な利点の一つである。

字句的スコープを持つ型変数は-XScopedTypeVariablesで有効になる。このフラグを指定すると、-XRelaxedPolyRecも有効になる。

7.13.8.1. 概観

以下の原則に沿って設計されている。

  • スコープを持つ型変数は型変数を表すものであり、を表すものではない。(これはGHCの以前の設計との相異点である)

  • さらに、異なる字句的な型変数は異なる型変数を表す。従って、プログラマの書いた型シグネチャ(スコープを持つ型変数を含む物も)は固い(rigid)型を表す。つまり、その型は型検査器にとって完全に既知であり、推論は関与しない。

  • 字句的スコープを持つ型変数は、プログラムの意味を変えることなく、自由にα改名できる。

字句的スコープを持つ型変数は以下の方法で束縛できる。

Haskellでは、プログラマの書いた型シグネチャは、その自由変数について暗黙に量化される(Haskellレポートの4.1.2節(和訳))。字句的スコープを持つ型変数がこの暗黙量化規則に与える影響として、スコープにある型変数は全称量化されない。例えば、型変数aがスコープにあるとすると、

(e :: a -> a)     は     (e :: a -> a)          を意味する
(e :: b -> b)     は     (e :: forall b. b->b)  を意味する
(e :: a -> b)     は     (e :: forall b. a->b)  を意味する

7.13.8.2. 宣言型シグネチャ

明示的な量化(forallを使ったもの)を伴う型シグネチャがあると、その明示的に量化された型変数は、その関数の定義内において、スコープに導入される。例を挙げる。

f :: forall a. [a] -> [a]
f (x:xs) = xs ++ [ x :: a ]

forall aによって、afの定義内でスコープに導入されている。

これは、以下の場合にのみ発生する。

  • fの型シグネチャにおける量化が明示的である。例えば、

    g :: [a] -> [a]
    g (x:xs) = xs ++ [ x :: a ]
    

    このプログラムは拒絶される。afの定義においてスコープにないので、x::aは、通常のHaskellの暗黙量化規則に従って、x::forall a. aと解釈される。

  • シグネチャの対象とする束縛が関数束縛または裸の変数束縛であって、パターン束縛でない。例えば、

    f1 :: forall a. [a] -> [a]
    f1 (x:xs) = xs ++ [ x :: a ]   -- 良い
    
    f2 :: forall a. [a] -> [a]
    f2 = \(x:xs) -> xs ++ [ x :: a ]   -- 良い
    
    f3 :: forall a. [a] -> [a]
    Just f3 = Just (\(x:xs) -> xs ++ [ x :: a ])   -- これは駄目!
    

    f3の束縛はパターン束縛なので、この型シグネチャはaをスコープに導入しない。一方、f1は関数束縛で、f2は裸の変数を束縛している。したがって、これらでは両方ともシグネチャがaをスコープに導入している。

7.13.8.3. 式型シグネチャ

明示的な(forallを使った)量化を伴った式型シグネチャがあると、それらの型変数は、その型シグネチャの付いた式の内部において、スコープに導入される。例を挙げる。

f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )

この場合、forall s. ST s Boolという型シグネチャによって、型変数sが、シグネチャの付いた式(op >>= \(x :: STRef s Int) -> g x)の内部においてスコープに導入される。

7.13.8.4. パターン型シグネチャ

型シグネチャは任意のパターンの中に現れても良い。これはパターン型シグネチャと呼ばれる。例を挙げる。

-- f と g では、'a'が既にスコープにあることを期待している
f = \(x::Int, y::a) -> x
g (x::a) = x
h ((x,y) :: (Int,Bool)) = (y,x)

パターン型シグネチャに現れる型変数がすべて既にスコープにある場合(つまり、外側の文脈で束縛されている場合)、事態は簡単である。そのシグネチャは、パターンの型を当たり前の方法で制限するだけのものである。

式型シグネチャや宣言型シグネチャと違って、パターン型シグネチャは暗黙に一般化されることがない。パターン束縛中のパターンは、既にスコープにある型変数にしか言及してはならない。例を示す。

f :: forall a. [a] -> (Int, [a])
f xs = (n, zs)
  where
    (ys::[a], n) = (reverse xs, length xs) -- OK
    zs::[a] = xs ++ ys                     -- OK

    Just (v::b) = ...  -- 駄目。bがスコープにないので。

ここで、yszsのパターンシグネチャは問題ないが、vのパターンシグネチャは、bがスコープにないので、不正である。

一方、パターン束縛以外の全てのパターンでは、パターン型シグネチャがスコープにない型変数に言及しても良い。この場合、このシグネチャがこの型変数をスコープに導入する。これは、存在的データ構築子の場合に特に重要である。例えば以下のような場合。

data T = forall a. MkT [a]

k :: T -> T
k (MkT [t::a]) = MkT t3
               where
                 t3::[a] = [t,t,t]

ここで、パターン型シグネチャ(t::a)は、スコープにない字句的型変数に言及している。実際、これはスコープにあってはならない。このパターン照合で束縛されるからである。このような状況では(そしてこのような状況でのみ)、パターン型シグネチャがまだスコープにない型変数に言及できる、というのがGHCの規則である。作用として、その型変数はスコープに導入され、存在的に束縛された型変数を表すことになる。

パターン型シグネチャがこの方法で型変数を束縛する場合、GHCはその型変数が固い(完全に既知の)型変数に束縛されたと見なす。これによって、ユーザの書いた型シグネチャが全て完全に既知の型を表すことになる。

このあたりのことは少し奇妙に思えるかもしれない。我々もそう思う。しかし、このような型変数をスコープに導入するなんらかの方法は必要であり、さもなくば、後続の型シグネチャから存在束縛された型変数を名前で呼ぶことができなくなってしまう。

これはパターン型シグネチャがスコープにない字句的型変数に言及できる唯一の状況(になった)である。例えば、aがまだスコープにないなら、fgは両方とも不正である。

7.13.8.5. クラス宣言とインスタンス宣言

classまたはinstance宣言の頭部の中の型変数は、対応するwhere部分の全体に渡るスコープを持つ。例。

class C a where
  op :: [a] -> a

  op xs = let ys::[a]
              ys = reverse xs
          in
          head ys

7.13.9. 束縛および一般化

7.13.9.1. 恐怖の単相性限定を無効にする

Haskellの単相性限定(Haskellレポートの4.5.5節(和訳)を見よ)は、-XNoMonomorphismRestrictionで完全に無効にできる。GHC 7.8.1以降では、GHCiにおいて単相性限定がデフォルトで無効になる。

7.13.9.2. 相互再帰的な束縛に対する型付けの一般化

Haskellレポートでは、束縛のグループ(最上位、またはletwhere中のもの)は、まず強連結な成分に分割され、次に依存性の順に型検査されると規定されている(Haskellレポートの4.5.1節(和訳))。個々のグループが型検査されるとき、グループの中の明示的な型シグネチャのある束縛は、指定された多相型を持つものとして型環境に入れられ、そうでないものは全て、グループが一般化されるまで単相的でありつづける。(Haskellレポートの4.5.2節(和訳))

Mark Jonesの論文Typing Haskell in Haskellでの提案に従って、GHCはより一般的な様式を実装している。-XRelaxedPolyRecが指定されているとき、依存性解析において、明示的な型シグネチャのある変数への参照は無視される。依存性解析がこのように変更される結果、依存性グループは小さくなり、より多くの束縛が型検査を通るようになる。例として以下を考える。

f :: Eq a => a -> Bool
f x = (x == x) || g True || g "Yes"

g y = (y <= y) || f True

Haskell 98ではこれは不正であるが、Jonesの様式の元では、まずgの定義の型検査が、fとは独立に行われる。これは、gの右辺でのfへの参照が依存性解析に無視されるからである。次にgの型が一般化され、以下のものが得られる。

g :: Ord a => a -> Bool

今度は、gの型を型環境に置いて、fの定義が型検査される。

また、この改良された依存性解析によって、相互再帰的な関数のシグネチャが互いに異なる文脈を持つことができるようになった。これはHaskell 98では不正である(4.5.2節の最後の文)。-XRelaxedPolyRecが使われているとき、GHCは改良されたグループについてのみ、シグネチャが同じ文脈を持っていることを要求する。これは実際的には、同じ文脈を持たなければならないのは、一つのパターン束縛で束縛された複数の変数だけだということである。例えば、以下のものは問題ない。

f :: Eq a => a -> Bool
f x = (x == x) || g True

g :: Ord a => a -> Bool
g y = (y <= y) || f True

7.13.9.3. letにおける一般化

ML風の言語は通常、letやwhereで束縛された変数すべてについて、可能な限り多相的になるように一般化を行なう。-XMonoLocalBindsが指定されると、GHCはこれよりもやや保守的な指針を実装する。すなわち、「閉じた」束縛のみを一般化する。束縛が「閉じている」とみなされるのは、以下のいずれかの場合である。

  • モジュールの最上位束縛の一つである

  • その束縛の自由変数が全てそれ自身閉じている

例として、以下を考えよ。

f x = x + 1
g x = let h y = f y * 2
          k z = z+x
      in  h x + k x

ここで、fgは、最上位で定義されているので閉じている。また、hは、唯一の自由変数であるfが閉じているので、閉じている。一方、kは、局所的に定義された変数であるxに言及しているので、閉じていない。これは、次のように考えることもできる。すなわち、閉じた束縛はすべて、最上位で定義することも理論上可能である。(この例では、hを最上位にもっていくことが可能である)。

これは全て、束縛に型シグネチャがなく、GHCがその型を推論しなければならない場合にのみ当てはまる。型シグネチャがある場合、それは束縛の型を決定する。これだけである。

この保守的な戦略の理由は以下の論文 "Let should not be generalised" と "Modular type inference with local assumptions"、およびこれに関連したブログ記事にある。

フラグ-XMonoLocalBinds-XTypeFamiliesおよび-XGADTsによって自動的に有効になる。-XNoMonoLocalBindsを使うと、これを無効に戻すことができるが、そうすると型推論の結果が予測しにくくなる。(論文参照のこと!)