ML多相の続き - sumiiのブログ
さて、Wrightの論文の当時は、value restrictionは妥当な制限だった。なぜならば、value restrictionのせいで型付けできなくなる主なケースは、多相関数の部分適用がまた多相関数になる（はずの）場合ぐらいで、それはlet x = eのeをfun y -> e yのように書き換えること（η展開）で回避できたからである。 ところが、SML#のような多相レコード、OCamlのような多相オブジェクトないし多相バリアントを利用すると、value restrictionが本当に問題になってくる。たとえば # let f x = `V x ;; val f : 'a -> [> `V of 'a ] = <fun> # let v = f 1 ;;などで、vがpolymorphicにならないとしたら、「（実質的に）多相バリアントを返す関数は書けない」ことに（事実上）なってしま
ML多相 - sumiiのブログ
というわけで大体の解説。 MLの多相型推論は、let x = eのような宣言があったら、eの型を推論して、「決まらなかった」部分は「何でもよい」と解釈し、具体化されなかった型変数について∀を先頭を追加する。たとえば、 let id = fun y -> yだったら、fun y -> yの型がα→αのように推論されるので、idの型は∀α.α→αになる。ただし、OCamlやSML/NJでは、∀α.は省略され、表示されない。 ところが、破壊的代入やcall-with-current-continuationなど「副作用」のある言語では、上述の型推論は不健全になる。たとえば let polyref = ref []においてpolyrefの型が∀α.α list refと推論されてしまったら、 polyref := [true]と 123 + List.hd !polyrefが両方とも型付けできてし
EOPLの再帰関数の実装 - sumiiのブログ
SICPがset!を使っている(4.1.6節)ので当たり前?かもしれないのですが、EOPL（第二版）も再帰関数をややこしく実装している(3.6節)ことを知ってしまいました。いや、以前に輪講したので知っていたはずなのですが忘れていました… EOPLでは再帰関数の名前が参照されるたびにクロージャを生成したり(Figure 3.9)、それを避けるために破壊的代入を使ってメモ化をしたり(Exercise 3.35)しているようです。が、そんなことをしなくても、クロージャの定義を拡張して、 letrec f(x) = eのように再帰関数が定義されたら、fが束縛されるクロージャに自分自身の名前fも格納 しておき、 関数適用時にふたたびfを自分自身のクロージャに束縛 すれば十分です。86ページ中ほどのクロージャ表現に合わせて書くと (define-datatype procval procval? (c
callccによる排中律の証明 - sumiiのブログ
Wadlerのパクリ。というか劣化コピー。 悪魔：「あなたが私と契約してくれたら、(A)『私があなたに一億円をあげる』、(B)『あなたが私に一億円をくれたら、どんな願いでもかなえてあげる』のどちらかをして差し上げます。(A)と(B)のどちらにするかは、私が決めます。」 人間：「どちらにせよ害はなさそうなので、じゃあ契約します。」 悪魔：「はい、では私は(B)を選びます。」 人間：「やっぱりそう来るか。でも一億円なんて持ってないし、まあいいや。」 （十年後） 人間：「気になってしょうがないので、悪いことをして一億円を集めました。だから願いをかなえてください。」 悪魔：「そりゃどうも（と一億円を受け取る）。では私は(A)を選びます。はいどうぞ（と一億円を返す）。」 ICFP 2003の会場ではWadlerとShiversが壇上で寸劇をやりました（本当）。λ式で書くと callcc(λk:¬(T
型推論と型検査、静的な型つけと動的な型つけ、強い型つけと弱い型つけ - sumiiのブログ
ついでに追加。 型推論：変数や式の型をプログラマが宣言しなくても、言語処理系が文脈から推論してくれる機構。MLとかHaskellとか。 型検査：変数や式の型が合っていることを言語処理系が（普通は静的に）チェックしてくれる機構。CとかJavaとか、MLやHaskellも。 静的な型つけ：プログラムの実行前に型を検査する機構。MLとかHaskellとかCとかJavaとか。 動的な型つけ：プログラムの実行中に型を検査する機構。LispとかSchemeとかPerlとか。 強い型つけ：検査を通れば、安全さ(safety)が保証される、という（普通は静的な）型つけ。MLとかHaskellとかJavaとか。Javaはバグがあったりしたので少し怪しいですが。 弱い型つけ：検査を通っても、安全さ(safety)は保証されない、という型つけ。CとかPascalとか。 安全さ(safety)：プログラムが言語仕
OCamlによるプログラミングの日本語教科書、刊行 - sumiiのブログ
「プログラミングの基礎」、Computer Science Library 3、浅井健一著、サイエンス社、ISBN978-4-7819-1160-1、定価2300円＋税。正式には25日刊行のようです。お茶の水女子大学でのOCamlによるプログラミング演習のテキストで、プログラミングの初心者用に、非常に丁寧に説明されています。 追記：もちろん、プログラミングの初心者でなくても、関数型言語の勉強にも有用そうです。 追記２：出版社のサイトに目次等が出ました。元記事↑を書いたときは探しても見つからなかった（と思う）ので、自分でスキャンして載せようか迷ったぐらいですが、さすがにＯＫかどうか自信がなかったので…。Amazonにはまだないらしい。(ISBN:9784781911601)
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
