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

type t (* void *)

関数型言語や英語学習の事とか。

OCaml: 型注釈って面倒ですね。

卒論で死にそうです。色々。

PPLのポスター発表に間に合うのでしょうか、その前に卒論発表会に間に合うのか…。

それはさておき、型注釈を色々見ていたら、MLも闇だなぁと思ってたのでちょっとメモしてみます。

 

 追記の追記の追記:

@camloebaさんにツッコミをいただきました。型注釈という言葉は不適切ということでした。

毎度ありがとうございます[´・_・`]

 

http://caml.inria.fr/pub/docs/manual-ocaml-4.00/expr.html

をよんでも確かにtype annotationという言葉は使われてないですね。ありがとうございます!!!

 

例題はこちら。

type annotation

 

言われてみればまぁ通らないよねって感じです。

 

追記:

何も通らない理由を書いてなかったので、勿論MLに親しんでいる諸兄らは問題なく理解されると思いますが、一応理由を追記しておきます。

型変数のスコープの問題です。ちゃんとしたテクニカルな説明はちょっと難しいので、自分の理解を書いておきます。

 

上の通らない例で、'aのスコープはfの定義が始まって終わるまでです。

なので、fの中でgが使われるとき、まだ'aの型推論は終わっていません。なのでgは多相関数にはなりません。

 

MLの型推論は大雑把に言って、型の制約に関する方程式を解いて、残った型変数に(制約がないもの)にforallをつける、というものです。

推論が行われている最中では、関数は単相的であるとして扱われます。なぜならばpolymorphic recursionは許されていないからです。

(なぜ許されないかというと、これを許すと型が決定不能になるからです。なぜ型が決定不能になるかは論文を読んでください…。)

 

というわけで、上の例ではgの型について推論が終わっていない段階で多相的に扱おうとしているため、エラーが発生するのです。

(追記ここまで)

 

追記の追記:

もしかしたらちょっとした落とし穴になるんじゃないかな?と思いました。

let (g:'a) なんてわざとらしいですが、例えばこれがlet (g:'a -> 'a)と書くのはありえそうじゃないですか?

あまりしそうにないですが、ないことはないだろうなぁと思いました。

はて、世の中のOCamlの解説している文献に、型変数のスコープのことは書いてあったかしら…。

(追記の追記おわり)

 

ちょっと卒論と関わるので調べていました。

それ以外にもOCamlソースコード読んでると、副作用バリバリだったりtypedtreeの構造がこうなっているーとか面白いこといっぱいあるのですが、今回はこれくらいで。

あ、これは紹介します。ちょっと前に教えてもらったものですが、

How OCaml type checker works -- or what polymorphism and garbage collection have in common

http://okmij.org/ftp/ML/generalization.html

 

OCaml型推論の話。levelを用いた型推論方法について、です。