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

OCamlのStructural Polymorphism

※細かな表現などを修正しました

細かいことですが。

http://d.hatena.ne.jp/mmatsuoka/20060831#1156989501

OCamlのStructural Polymorphismは、(少なくとも)現在はGarrigueの型システムです。多相レコードには、Remyらによる列変数(row variable)を用いた表現と、大堀らによるカインド(kind)を用いた表現があるのですが、カインドを用いた大堀レコードを拡張したものになっています。カインドを利用した表現の方が、多相ヴァリアント(polymorphic variant)も扱う場合に都合が良いんだと思います。型システム自体も列変数を用いた表現よりも、(直感的ではないのですが)フォーマルに考えるときはシンプルです。

http://www.math.nagoya-u.ac.jp/~garrigue/papers/にある「Simple Type Inference for Structural Polymorphism」がその辺の型システムの論文です。「 Private rows: abstracting the unnamed」という論文は、OCaml 3.09で入ったprivate row typeに関する論文で、これを読むとOCamlの型システムがGarrigueの型システムに基づいていることが明らかになります*1

(O'Haskellの論文はOCamlがらみの論文を一つも引用していなかったりして、コミュニティの断絶を感じるなあ)

断絶と言うよりは、もっと自然な立場の違いのようにも思います*2OCamlの型システムは「最も一般的な型が推論されること(principality)」を重視しているので、Peyton Jonesの型システムで許される「最も一般的な型が存在しない型*3」の推論を許したくなかったという話を聞いたことがあります。単純にHaskellの方がアグレッシブな型システムを目指して開発されていることが理由で、細かな違いが発生するのではないか、というイメージを受けます*4

*1:ちなみにPrivate rowsの論文は、Rowとか言ってる割に型システムの話でいきなりカインドが出てくると言う、わけのわからない構成になっています(暴言)

*2:この話に関しては

*3:例: < id : ∀α. α→α >

*4:この姿勢を感じるのは、他には例えばpolymorphic recursionを許すか許さないか、とか