HaskellとOCamlの型の違い

Jun Furuse 🐫🌴 @camloeba

@garriguejej ああ良かった… びっくりした 主要性がある完全なシステムは dispatch が陽に出てきたレベルの話ですか？

Jun Furuse 🐫🌴 @camloeba

. @garriguejej 謎の ocamlc -principal

Jacques Garrigue @garriguejej

@camloeba だから最近のような Outside In というある意味でとても弱い型システムが出て来た。あれでは多相関数の型が推論できない。Haskell では型を書く習慣があるのでなんとかなるけど、 ML でそんなことしたら大問題のような気がする。

Jacques Garrigue @garriguejej

そう。Alainから彼らのコードが -principal 付きでコンパイルできないと聞いてショックを受けた。型システムの進んだ機能を使うなら、たまに使って欲しいものだ。 RT @camloeba 謎の ocamlc -principal

Jun Furuse 🐫🌴 @camloeba

Haskell 書いてるときは OCaml 使いたいし OCaml 書いてるときは Haskell 使いたい。というのが今の私の心境です

Jacques Garrigue @garriguejej

いや、単に曖昧な場合を発見して、そういうときはエラーにするだけだったと思う。 QT @camloeba 主要性がある完全なシステムは dispatch が陽に出てきたレベルの話ですか？

山本和彦 @kazu_yamamoto

結局、OCaml の型システムは何と表現すればいいのか、誰かまとめて下さい。

shelarcy（しぇらーしぃ） @shelarcy

See also: Outside In http://t.co/fPpSc3xw http://t.co/HGQ5vUn9 Let generalisation in GHC 7.0 http://t.co/EDMMw6Ug #readghc

shelarcy（しぇらーしぃ） @shelarcy

なお、"Let generalisation in GHC 7.0" に書いてありますが、Outside In の多相関数の型が推論できないという制限は GHC 7.4.1(や 7.2.x)では緩和されています。 http://t.co/F6TM4pT7 #readghc

Jun Furuse 🐫🌴 @camloeba

@garriguejej はて？では、その完全な奴はどのレイヤで定義されてるの？

Jun Furuse 🐫🌴 @camloeba

@garriguejej MLに型クラスを入れるとすればそこだけ限定で使えば良さげだと思っています

Jun Furuse 🐫🌴 @camloeba

作っているんだよw でも仕事と子育て優先 RT @wasabiz HaskellみたいなOCamlつくればええやん

Jacques Garrigue @garriguejej

Haskell の場合は完全ではないと思う。やはり彼らは主要性を ML とちょっと違う意味で使っています。 QT @camloeba はて？では、その完全な奴はどのレイヤで定義されてるの？

Jacques Garrigue @garriguejej

@camloeba ML でいう主要性は、もしも型が付くものがあれば、主要な型が存在する。 Haskell の主要性は、もしも主要な型がなければ、主要でない型を排除する。頑張ると主要性っぽい定義ができるが、自己言及的な感がある。そして主要な場合の発見について完全ではないはずだ。

Shuhei Takahashi @nya3jp

自分の好きなプログラミング言語を dis るのとか好きです。

Jacques Garrigue @garriguejej

@camloeba ちなみに principal typing と principal types は違う、ML は後者、前者は intersection type がないとできない。（突っ込みばかりでごめん）

Jun Furuse 🐫🌴 @camloeba

@garriguejej どんどんお願いします

Jacques Garrigue @garriguejej

@tanakh OCaml だって完全性と色々妥協しているよ。そして Haskell にない型も色々持っている。今になって overloading がないことはかなり重要な気がする。型を考えない意味論が可能だ。しかし、型インデクスの導入も時間の問題か。

Jun Furuse 🐫🌴 @camloeba

かなり型理論にかんする知識が錆び付いている、駄目だな

Jun Furuse 🐫🌴 @camloeba

ウーンタシカに types と typings 違うと書いてあるよ…

Takuya Hitomi @takuchan

OutsideIn(X)で多相関数の型を推論できないっていうのは厳密じゃなくて、letで定義されるローカルな関数に関してのみ多相的に推論しないって言うが厳密かな。トップレベルに定義される関数は多相な型を持つように推論されるから。

Takuya Hitomi @takuchan

そしてOutsideIn(X)でローカルな関数は多相的に推論しなくても問題なっていうことを言うためにhaskellのライブラリを調査して、結論をだしているから、他の関数型言語でもそうしてもあんまり問題ないと思う。

Takuya Hitomi @takuchan

TypeClassによって型システムにもたらされた複雑さもあれだけど、個人的にはGADTの方が型システムにもたらした影響はでかい感じがするな。一部の型推論を遅延しないといけなくなるんだぜ！あいつのせいで。

Takuya Hitomi @takuchan

型推論なんて、制約の生成の後にsyntactic unificationをするだけの簡単なお仕事だったのに、GADTのせいで型推論自体も複雑になるし、型システムの性質に関する証明も複雑になるし…

Jun Furuse 🐫🌴 @camloeba

改造して確かめました。MLでは問題あり RT @takuchan そしてOutsideIn(X)でローカルな関数は多相的に推論しなくても問題なっていうことを言うためにhaskellのライブラリを調査して、結論をだしているから、他の関数型言語でもそうしてもあんまり問題ないと思う。