GHCのforallには一見複数の意味があるように思われます:
- 関数シグネチャの
forall -
RankNTypesによるforall -
ExistentialQuantificationによるforall
けどまあ基本的な考え方は同じで問題ないと思ってます。
関数シグネチャのforall
Haskellで関数の型シグネチャに現れる変数は、暗黙に量化されます。
id :: a -> a
という関数は正確にはforallを用いて以下のように表現されます(forall明示にはExplicitForAllか、それをimplyする言語拡張を指定する必要があります)
id :: forall a. (a -> a)
この変数aが具体化されるのは関数適用時です。
main = putStrLn $ id "Hello, type variables!"
ここで関数idを"Hello, type variables!"に対して適用すると、その適用に応じて型変数が具体的な型に具体化されます。ここではStringと推論されます。
次のコードではidをStringとIntegerに対して適用しています。
main = do
putStrLn $ id "Hello, type variables!"
print $ id 42
こうして複数の型に対応する関数を一つにまとめられることがparametric polymorphismの利点でした。
さて他の言語でジェネリクスでは型変数を<>やら[]やらで囲んで導入すると思いますが、それらの型変数が具体化するタイミングは皆知っていることでしょう。クラスの頭に付いていたらオブジェクト生成時に具体化、メソッドの頭に付いていたらメソッド呼び出し時に具体化されます。
ランク1の型のforallはそれと同じものです。
次のコードはscalaです。scalaでは[]を用いて型変数を導入します。
object Main {
// 型変数 T, S の導入
def map[T,S](f: T => S, seq: Seq[T]): Seq[S] = {
seq match {
case Nil => Nil
case x +: xs => f(x) +: map(f, xs)
}
}
def main(args: Array[String]) = {
// mapの呼び出し時にT, Sは具体化される
// ここでは[Int,String]と明示
val result = map[Int,String]({ n: Int => n.toString }, Seq(1,3,4,5))
println(result)
}
}
Haskellでは冠頭のforallが省略できてしまうので、型変数の導入が曖昧に見えてしまうかもしれません。
mapList :: (a -> b) -> [a] -> [b]
mapList f [] = []
mapList f (x:xs) = f x : mapList f xs
main = print $ mapList show [1,3,4,5]
RankNTypesによるforall
言語拡張RankNTypesを指定すると、任意のランクの型をもつ関数を定義出来ます。例えばforallが付いた関数を渡す高階関数を定義できます。
{-# LANGUAGE RankNTypes #-}
main = putStrLn $ f show 42 True
f :: forall a b. (Show a, Show b)
=> (forall s. Show s => s -> String)
-> a -> b -> String
f toString a b = toString a ++ " " ++ toString b
型変数a, bが具体化されるのはfの関数適用の時、sの具体化は引数で渡した関数toStringを適用する度に行われます。
比較のために全てのforallを冠頭部に持ってきた関数を見てみます。
-- これは型エラー
g :: forall a b s. (Show a, Show b)
=> (Show s => s -> String)
-> a -> b -> String
g toString a b = toString a ++ " " ++ toString b
この関数は型エラーが発生します。gを関数適用した時点でa, b, sは全て決定するのに、aとbとsは同じ型とは限らないためtoStringの型は矛盾します。
これはランク2のケースですが、ランクがいくつでも考え方は同様です。つまり、forallが冠頭に来た関数の適用時に型変数は具体化します。
ExistentialQuantificationによるforall
言語拡張ExistentialQuantificationを指定すると、型定義の右側だけに現れる型変数を使うことが可能です。
data ShowType = forall a. Show a => ST a
これも考え方は同じです。つまり、値コンストラクタSTを呼び出す際に型変数aが決定されます。そして型の上にaは現れません。そういう型です。
まとめ
型変数の具体化がどこで行われるべきかを正確に理解すると、多相性への対処も容易になるでしょう。またRank1で説明したように他の言語でのジェネリクス等の理解も深まるでしょう。