日々の流転

λ. 大堀流のランク1多相についての勘違い

Lightweight Languge Spirit のときに、疑問と誤解が解けた話。

私は value restriction や値多相(value polymorphism)*1をよく知らなかったことから、大堀流のランク1多相の目的は、直積や直和の成分を多相型に出来ること自体だと思い込んでいた。 そして、Haskell(GHC)の場合、その際に問題になったのは型変数、特に (,) :: ∀a b. a -> b -> (a, b) のようなコンストラクタの型に現れる型変数を多相型でインスタンス化することを許すかどうか、つまり非可述的多相(impredicative polymorphism)の問題だった(GHC and impredicativity)。それなのに、MLでは何故ランクの話になるのだろう???　……と疑問に思っていたのだった。

実際には、コンストラクタは普通の関数とは別扱いで、コンストラクタの型に現れる型変数を多相型でインスタンス化しているわけではないそうだ。考えてみれば、上記のようなコンストラクタの型変数を多相型でインスタンス化するとランク2の型になってしまうしな。

で、何故コンストラクタが普通の関数と別扱いになっているかというと、もともと値多相では式にexpansiveな式とnon-expansiveな式という区別があり、non-expansiveな式のみが多相型を持てるようになっているため。 一般の関数適用はexpansiveな式だけど、コンストラクタの適用は引数がnon-expansiveならばnon-expansiveになるので、区別されていた。 そして、大堀流のランク1多相は、直積や直和の成分を多相的にすることが直接の目的ではなく、値多相による制限を緩和することが目的なので、それに応じた設計になっていると。

λ. 床屋

に行ってきた。