動的束縛制約は自動的に伝播される。この点で、型クラス制約と同じ振る舞いである。つまり、ある関数が使われるとき、その関数の暗黙パラメタはその関数を呼んだ関数に受け継がれる。例えば、上記の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の型を固定する。

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

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

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

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

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

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

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を返す。

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

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

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

一般に、任意ランクの型に対する型推論は決定不能である。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の引数であり、必要なことは全てこのことから分かる。

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

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

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

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)  を意味する

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

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

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

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

明示的な(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)の内部においてスコープに導入される。

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

-- 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がスコープにないので。

ここで、ysとzsのパターンシグネチャは問題ないが、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がまだスコープにないなら、fとgは両方とも不正である。

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

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

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

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

Haskellレポートでは、束縛のグループ(最上位、またはletやwhere中のもの)は、まず強連結な成分に分割され、次に依存性の順に型検査されると規定されている(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

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

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

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

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

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