簡単な OCaml パーサを書いてみてる。関数値と関数適用は引数の有無で判別できる……だったかな(ひさしぶりなので忘れてる)。

冬休みなのでそのうちやろうと思ってたこれをやってます。

[S-8] 関数プログラミング
logic.cs.tsukuba.ac.jp/jikken/

let x: int = 1 in x
までできた。なるほど、型検査ってこんな感じなんだなー。

7-4. Type Checking for Functions
logic.cs.tsukuba.ac.jp/jikken/

7-4 のあたりまで進んだ。最初なのでゆるくやっていて、CPSとかは後回しにしてる。

kuis-isle3sw/IoPLMaterials: Materials for the class "Implementation of Programming Languages" in Kyoto University.
github.com/kuis-isle3sw/IoPLMa

あー……こっちでやればよかった(知ってたのに忘れてた)

unify, ちょっと雰囲気が分かってきた。ちょっとだけ。

木を辿りながら、構造が一致する部分ごとに比較用の対(等式)を作って、型代入を更新していく

とりあえずテストが通る実装できたけど理解が全然追いついてない

let x = 1 in x の推論できた。 Plus を踏まえた形にしてみたけどこれで合ってるのかまだよく分からず。

フォロー

『プログラミング言語の基礎概念』の型推論の章を読み返したら知りたかったことが書かれてた

> さて,上に示した型推論アルゴリズムは、方程式を全て求めてから、それをまとめて解く(単一化する),というものになっているが,方程式の生成と単一化を少しずつ交互に行うようなアルゴリズムとして定式化することも可能である.

『プログラミング言語の基礎概念』 p168

(今の自分には)前者の方が考え方としては分かりやすい気がする。後者は実装・実用上の都合なのかな。

👀

「型推論」特別講義 (プログラミング言語の基礎理論シリーズ)第1回 - YouTube
youtube.com/watch?v=Ju-vJilPjE

「型推論」特別講義 (プログラミング言語の基礎理論シリーズ) - YouTube
youtube.com/playlist?list=PLp1

リストはこっち

mal を拡張する形で型推論部分を作るルートもよさそう

stdin/out とやりとりする組み込み関数 read, write を追加して (write (read)) が動くようになった

do も追加して1バイトずつ読み書きするだけの cat が動いた

(letrec
f
(fun ()
(let n (read)
(if (= n -1)
0 ;; EOF
(do
(write n)
(f)))))
(f))

やっぱりめんどくさくなったのでパーサは後回しにしてとりあえずS式で。

eval を末尾呼び出し最適化対応版にしてみた。mal と同じ方式。

mal を真似して try/catch を追加して cat を書き直し。型まわりはよく分からないのでとりあえず適当。

(letrec
f
(fun ()
(do (write (read))
(f)))
(try* (f)
(catch* ex ex)))

型推論のある言語作った - Route 477(2014-06-05)
route477.net/d/?date=20140605#

github.com/pi8027/typeinfer
をベースにして Ruby で書かれたもの

let rec 〜 and 〜 をやるために let rec をおさらい

単純型付きラムダ計算(前半) - YouTube
youtube.com/watch?v=Q9NWbKFhmS

単純型付きラムダ計算(後半) - YouTube
youtube.com/watch?v=Vm-7KTpj1d

ログインして会話に参加
Fedibird

様々な目的に使える、日本の汎用マストドンサーバーです。安定した利用環境と、多数の独自機能を提供しています。