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

明示的な全称量化(forall)

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

        g :: b -> b

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

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

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

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

型シグネチャの文脈

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

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

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

GHCは、型シグネチャに関して以下の制限を課す。次の型を考える。

  forall tv1..tvn (c1, ...,cn) => type

(ここでは「forall」を明示的に書いたが、Haskellソース言語では省略される。Haskell 98では、ソース言語中の明示的な型シグネチャにおける型変数は全て全称量化される(クラス宣言中のクラス型変数の場合を除く)。ただし、GHCでは、望むならforallを与えても良い。7.8.1. 明示的な全称量化(forall)を見よ)

  1. 全ての全称量化された型変数tvitypeから到達可能でなければならない。型変数aが「到達可能」なのは、typeに現れる型変数または別の到達可能な型変数と、その型変数が、同じ制約の中に現れるときである。この到達可能性制限に従わない型を持つ値は、曖昧性を導入することなく使うことができない。これがこういう型が禁止される理由である。例えば、以下の型は許されない。

      forall a. Eq a => Int
    

    この型の値が使われるとき、tvを新しい型変数として、Eq tvという制約が導入され、(辞書渡し実装では)この値がEq tvの辞書に適用される。問題は、tvについてこれ以上情報を得ることができないため、どのEqのインスタンスを使うべきか決して知ることがきないということである。

    この到達可能条件は「atype中の型変数に関数従属している(7.6.2. 関数従属 を見よ)」という条件よりも弱いことに注意。これは、場合によっては、スーパークラスに「隠された」従属性があり得るからである。従って、到達可能性は関数従属性に対する保守的な近似である。例えば、以下の例を考えてみよう。

      class C a b | a -> b where ...
      class C a b => D a b where ...
      f :: forall a b. D a b => a -> a
    

    これは問題ない。実際、aは関数的にbを決定する。しかし、このことはfの型だけからは明らかでない。

  2. 制約ciは全て、少なくとも一つの全称量化された型変数tviに言及せねばならない。例えば、以下の型は、C a bが、全称量化された型変数bに言及しているので問題ない。

      forall a. C a b => burble
    

    次に示す型は、制約Eq baに言及していないので不正である。

      forall a. Eq b => burble
    

    この制限がある理由は、上のものほど深刻ではない。この制限によって排除されるのは、有用でも必要でもない型だけである。(この制約に反する文脈は、その位置にある必要がなく、より外側に移動させることができるからである)。さらに、これらを外側に移すことで共有が促進される。最後に、これを除外するというのは保守的な選択であり、後で必要になるかもしれない領域を取っておくことになる。

暗黙パラメタ

暗黙パラメタは、"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

暗黙パラメタ型制約

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

暗黙パラメタの束縛

暗黙パラメタは通常の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
    

暗黙パラメタと多相再帰

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

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

明示的に類付けされた量化

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 ')

括弧は必須である。

任意ランク多相

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の型があるからである。

GHCには、ランクの高い型を制御するための三つのフラグがある。

  • -XPolymorphicComponents: データ構築子(だけ)が、多相的な引数の型を持てる。

  • -XRank2Types: あらゆる関数(データ構築子を含む)が、ランク2の型を持てる。

  • -XRankNTypes: あらゆる関数(データ構築子を含む)が、任意のランクの型を持てる。つまり、関数矢印に必要なだけ深くforallを入れ子にすることができる。特に、forallの付いた型(「型スキーム」とも呼ばれる)は、型クラス文脈も含めて、以下の場所で使える。

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

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

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

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

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

型推論

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

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

xに明示的な型を「与える」とはどういう意味か。まず、xに直接型シグネチャを与えることができる。これにはパターン型シグネチャ(7.8.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型についてはそうすることが強く推奨される。

非叙述的多相

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に現れた。

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

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

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

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

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

注意: GHC 6.6では、字句的スコープを持つ型変数の挙動について大幅な変更が加えられた。この節を注意深く読んでほしい。

概観

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

  • スコープを持つ型変数は型変数を表すものであり、を表すものではない。(これは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)  を意味する

宣言型シグネチャ

明示的な量化(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をスコープに導入している。

式型シグネチャ

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

ここで、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は両方とも不正である。

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

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

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

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

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

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

単相的な局所束縛

我々は、局所的な束縛を一般化しないことによってGHCの型システムを単純化するという案を、活発に検討している。これについての論拠は論文Let should not be generalisedに記述されている。

この実験的な新しい振る舞いは、-XMonoLocalBindsフラグによって有効になる。これの効果は、局所的な(つまり最上位でない)束縛に型シグネチャがない場合、それが全く一般化されなくなるということである。これは、単相性限定を極端に(しかし、ずっと予測可能に)したものだと考えることができる。型シグネチャを与えた場合、このフラグに効果はない。