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

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

  data T a = MkT (Either a b) (b -> b)

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

  data T a = MkT (forall b. Either a b) (forall b. b -> b)

つまり、型変数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.12.7. 字句的スコープを持つ型変数 を見よ)を使う。

     \ 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