Arantium Maestum

プログラミング、囲碁、読書の話題

OCaml

wamlのコードを読んでる

Andreas RossbergがwebassemblyのGC proposalを試すために作ったミニML言語waml。以下の記事で紹介した: zehnpaard.hatenablog.com それからもちょこちょこと眺めていたのだが、 考えれば考えるほどwamlは(wasmとは関係なく)すごいな。正格評価なラムダ計算…

再帰型の実装に関して悩んでいること2 equi-recursive対iso-recursive

TaPLを読むと再帰型の理論と実装について、equi-recursiveとiso-recursiveという二つの流儀があると書いてある。 equi-とiso-については以下の記事でも少し触れた: zehnpaard.hatenablog.com しかし実際どういう違いなのかをメモった上でどちらにするのかを…

再帰型の実装に関して悩んでいること1 再帰する型変数の表現

型システムにどうやって再帰型を追加するかで悩んで手が止まっている。何に悩んでいるのかを書き出して整理していきたい。 今回は「現在、型そのものをtyというバリアント型で表現しているが、その枠組みで再帰型をどう表現するか」について。 そもそも再帰…

wasm GC Proposalのために作られた実験的な関数型言語処理系Wamlが面白そう

自分で実装している型システムに再帰型をつけたくてiso-recursive typesで検索していたらwasm garbage collectorのGitHubレポジトリで行われている侃侃諤諤な議論を見つけて読み漁っていた。 その中で見つけたのがwasmの中心的な人物であるAndreas Rossberg…

型システム実装幕間2 unifyとoccurs check、adjust levelについて

match_fun_tyなどのヘルパ関数をなくす是非を考えていて「型変数を新しく作成して使うコストは低いのだから(破壊的代入でリンクをアップデートしてるので管理する型変数の数が増えても処理が重くならない)、match_fun_tyなどでパターンマッチせずTArrow(tv…

型システム実装幕間1 各種matchヘルパ関数について

ここまで実装した型システムではコアな部分であるtypeofの中で使うヘルパ関数として5つmatch_..._tyという名前の関数を定義している: match_fun_ty match_tuple_ty match_rec_ty match_ref_ty match_list_ty これらは元々効率的なHM型推論のお手本として使…

Hindley Milner型推論に機能を追加していく13 Listの追加(後編)

前回に続いてList追加の実装を見ていく。今回はtypeofで使われるヘルパ関数について。 match_list_ty 前回見ていったtypeof関数で新しく使われたmatch_list_tyは「tyをとりリスト型と単一化させた上でそのリスト型が保持している型を返す」という関数。EHead…

Hindley Milner型推論に機能を追加していく12 Listの追加(前編)

前回「次は再帰型を追加する」と書いたが、その前振りとして関連しているがより簡単な「言語機能としてリスト型を提供する」をまずやっていく。 OCamlでユーザがリスト型を定義するなら: type 'a list = Nil | Cons of 'a * 'a list このように代数的データ…

Hindley Milner型推論に機能を追加していく11 Refの追加(後編)

前回書いたとおり、Let多相とRefとパラメトリックな型を組み合わせても型安全性が維持されるためには、Letで型が全称化される対象の式を制限する必要があり、これをvalue restrictionと呼ぶ。 残念ながらこの「全称化される式」であるsimple valuesのリスト…

Hindley Milner型推論に機能を追加していく10 Refの追加(中編)

前回の終わりに 前述のとおり今回のコードはRefとLet多相の関係により型安全ではない。 と書いた。 しかしよくよく考えてみると、現在実装した型システムだと機能がギリギリなところで弱く、Let多相とRef型があるにもかかわらず型安全性は保たれている、よう…

Hindley Milner型推論に機能を追加していく9 Refの追加(前編)

Ref型とそれに関係した式の処理を追加する。 この記事で(HM型推論なしで)追加したものと同じ: zehnpaard.hatenablog.com ref型を作るためのオペレータref(ここら辺OCamlだと型とオペレータの名前が被ったりしてややこしい)、ref型からデータを取り出すd…

Hindley Milner型推論に機能を追加していく8 Fixの追加

再帰関数を定義するためのFixオペレータを言語に追加する。 型推論なしで追加した時の記事はこれ: zehnpaard.hatenablog.com Fixの使い方などはこの記事を参照してほしい。 今回のコードはここ 型 型には変更なし。 式 Fix式を追加: type exp = ... | EFix…

Hindley Milner型推論に機能を追加していく7 Variant型の追加(後編)

前回に続いてバリアント型を追加していく話。今回はバリアント型を扱うための式とその式に対する型推論のロジックを見ていく。 式 バリアント型の値を作るETagと、パターンマッチでバリアントに保持されている値を取り出すECaseを追加: type exp = ... | ET…

Hindley Milner型推論に機能を追加していく6 Variant型の追加(前編)

バリアント型を追加していく。前回のレコード(あるいは前々回のタプル)と合わせて、代数的データ型の直積、直和が表現できるようになる。 コードはここ。 少し長くなったので今回は型としてバリアントを追加する話のみ。バリアント型の式を言語に追加して…

Hindley Milner型推論に機能を追加していく5 Record型の追加

HM型推論にレコード型を追加していく。今回のコードはこちら。 型 Record型を追加: type ty = ... | TRecord of (string * ty) list 基本的にはタプル型の要素に文字列のラベルがついているというイメージでいい。 TRecord of (string * ty) listとTRecord …

Hindley Milner型推論に機能を追加していく4 Tuple型の追加

HM型推論にタプル型を追加していく。今回のコードはこちら。 型 タプルというのはちょっと不思議な型で、型コンストラクタとして表そうとすると「任意の数の型をとる型コンストラクタ」となる。理論上の考え方としては二つの型をとるPair型コンストラクタとU…

Hindley Milner型推論に機能を追加していく3 Int型の追加

前回のBoolに続いてInt型とそれに関連する式であるIntリテラル、AddとIsZeroを実装する。 型 Int型の追加: type ty = ... | TInt 式 Intリテラル、Add、IsZeroを追加: type exp = ... | EInt of int | EAdd of exp * exp | EIsZero of exp AddはInt型の式…

Hindley Milner型推論に機能を追加していく2 Bool型の追加

前回の記事に続いてHM型推論を少し拡張する。 今回はBool型を追加し、Boolのリテラル式二つとIf式を実装する。 型 Bool型を追加: type ty = ... | TBool 式 True、False、If式の追加: type exp = ... | ETrue | EFalse | EIf of exp * exp * exp If式は条…

Hindley Milner型推論に機能を追加していく1 Unit型の追加

前々回、前回の記事でそれなりに実用的なLet多相型推論が実装できた: 型推論を実装・改善していく9 レベルによるLet多相の効率化(前編) - Arantium Maestum 型推論を実装・改善していく10 レベルによるLet多相の効率化(後編) - Arantium Maestum し…

OCamlコンパイラのバックエンドを提供するMalfunctionが面白そう

OCamlのDiscuss掲示板を眺めていたらこんなプロジェクトについての言及があった: github.com Malfunction is a high-performance, low-level untyped program representation, designed as a target for compilers of functional programming languages. OC…

型推論を実装・改善していく6.5 組み込み関数の多相型推論

このようなツイートを拝見した: instantiationだけ実装すれば組み込み関数の多相化が出来るのでは?— taka2 (@Jj1Fxh) October 30, 2022 確かにそのとおりで、単相型推論からLet多相の間に「ユーザ定義の関数は単相だが特定の組み込み関数は多相」という型…

型推論を実装・改善していく10 レベルによるLet多相の効率化(後編)

前回に続いてLet多相にレベルを導入した実装の詳細を見ていく。 具体的にはinstantiate、match_fun_ty、unify、occursinがレベルの導入でどう影響を受けるかという点と、unifyで新しく使われるadjustlevelの理屈と実装を解説する。 instantiate 汎化された型…

型推論を実装・改善していく9 レベルによるLet多相の効率化(前編)

前回、前々回と見てきたLet多相はgeneralizeが非常に非効率で、環境に含まれている型すべてを調べる必要があった。 初期のML(少なくとも初期のCAML)ではこのような実装になっており、その頃の遅いコンピュータ上でも殊更HM型推論が遅いことが認識されていた…

型推論を実装・改善していく8 Let多相型推論(後編)

前回に続いてLet多相の実装を見ていく。 generalize 前回書いたとおり、generalizeはLet式で「変数の型」を汎化する: let rec typeof env = function ... | ELet(svar, e, ebody) -> let tvar = typeof env e in let tgen = generalize (List.map snd env) …

型推論を実装・改善していく7 Let多相型推論(前編)

今回からHindley Milner型推論の要であるLet多相を実装していく。 これまで見てきた型推論は単相な関数しか扱えなかった。例えばこのようなコードはOCamlでは通る: utop # let id x = x = x in id 1 && id "hello";; - : bool = true しかし単相的な型推論…

型推論を実装・改善していく6 ミュータブルな型変数を使った単相型推論(後編)

前回に続いてミュータブルな型変数に対する破壊的代入で実装する効率的な単相型推論について見ていく。今回はtypeof関数の内部で使われているmatch_fun_ty、そしてunify, occursinの実装について。 match_fun_ty 前回見たとおり、型推論・型検査を行うtypeof…

型推論を実装・改善していく5 ミュータブルな型変数を使った単相型推論(前編)

「型推論を実装・改善していく3 純粋関数型な単相型推論(後編)」で書いたとおり、型推論のTaPL実装は副作用を使わない純粋関数型なもので、型制約のリストを正しく変換するunify関数がリストの長さnに対してO(n**2)な処理になっている。 その非効率さを改…

型推論を実装・改善していく4 状態を持つ型変数生成

前回書いた通り、TaPL準拠の型推論が完全に純粋関数型なのに対して、「ユニークな型変数を作る」new_tvar関数に状態を持たせることでいちいち引数・返り値のタプルの一部として渡し回さなくてもいいようにする。 HaskellだったらStateモナドの出番なのだろう…

型推論を実装・改善していく3 純粋関数型な単相型推論(後編)

前々回、前回に続いて純粋関数型な単相型推論の実装を詳細に見ていく。コードの全容はこちら。 型推論・型検査の関数であるtypeof: let typeof env new_tvar constr e = let (t, new_tvar, constr1) = infer env new_tvar e in let constr = unify (constr …

型推論を実装・改善していく2 純粋関数型な単相型推論(中編)

前回に続いて純粋関数型な単相型推論の実装を詳細に見ていく。コードの全容はこちら。 具体的には前回見たtypeof関数: let typeof env new_tvar constr e = let (t, new_tvar, constr1) = infer env new_tvar e in let constr = unify (constr @ constr1) i…