読者です 読者をやめる 読者になる 読者になる

forall

Haskell の型システムは厳格でありながら柔軟で、大抵の場合は型を記述しなくてもうまく推論してくれる。

だが、一見すると単純に見えるこのような定義でひっかかってしまった。

f :: (a->a) -> (b,c) -> (b,c)
f g (x,y) = (g x, g y)

xy の型が同じである場合は問題ない。

f id (1,2)

問題なのは xy の型が異なる場合だ。

f id (1,'a')

id の型は a -> a である (多相型) から、数値に適用しようと文字に適用しようと問題ないはずなのだが、上で定義した関数 f を通すとエラーになるのである。

idg にマッチしたところで型を具体化しようとするらしいのだ。 と言うより f の型を確定しようとして (Integer -> Integer) -> (Integer, Char) -> (Integer, Char) にしても (Char -> Char) -> (Integer, Char) -> (Integer, Char) にしても矛盾してエラーになるというわけだ。

このような場合に対応するため、 unification を抑制する方法が用意されている。

{-# LANGUAGE Rank2Types #-}
f :: (forall a . a->a) -> (b,c) -> (b,c)
f g (x,y) = (g x, g y)

こうするともう一段階後まで型の確定を遅らせることが出来る。

残念ながら forallGHC の拡張で、規格 (Haskell98) には無いらしい。 ありがちな事例に思えるのだが、 forall 無しで解決する方法はあるのだろうか。

ところで、いきなり話題が変わるが、 forall を表わす記号∀を見るたびに思い出すことがある。 知識工学の講義中に教官が「∀は断じて『ターンエー』とは読まない」としつこく言っていたことだ。 この記号をターンエーと読むのはガンダム∀だけで、要するにあて字のようなものである。

Document ID: e0347a6a9b5d9102e3e0e21f1d53abda