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

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

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

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

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

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

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

前回の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型の式…

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

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

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…

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

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

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

前回に続いて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) …

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

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

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

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

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

前回に続いて純粋関数型な単相型推論の実装を詳細に見ていく。コードの全容はこちら。 具体的には前回見た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…

型推論がある型システムを実装した上で改善していく。 具体的には TaPLのType Reconstruction準拠の単相な型推論を純粋関数型な単一化で実装 型変数の作成と単一化を破壊的代入で行うようにする（効率化） 型推論をLet多相に拡張 型変数を汎化していいかの確…

typeof関数のRefとError関連のケースを部分型に対応させる。今回でエラーに関する話は最後。 Ref 以前書いたとおり、安易にRefにBottomを含む型を持たせると型安全性が破壊されてしまう。なのでRefに入る値の型にはBottomがまったくないという厳しめの制約を…

今回はtypeof関数がレコード、バリアント、Fix関連でどう部分型に対応していくかを見ていく。 レコード レコードはフィールドの値が一つでもBottom型だったら全体がBottom型になる： | ERecord les -> let lts = (List.map (fun (l,e)->(l, typeof env e)) l…

今回はtypeof関数がSTLCのVar, Abs, AppそしてBool, Nat, Let関連でどう部分型に対応していくかを見ていく。 まずは変わらない部分から。 EVar, EAbs, ETrue, EFalse, ENat, ELetは変わらない： let rec typeof env = function | EVar var -> List.assoc var…

前回に続いて、エラー処理のある言語を型検査できる型システムを実装する話。今回は部分型全般やBottom型に対するチェックを行うヘルパ関数について。 導入するヘルパ関数は四つ： ある型がある型の部分型かどうかを調べるis_subtype 部分型関係を考慮に入れ…

前回書いたとおり、エラー式の型であるBottom型が部分型として正しく振る舞えるような変更を加えていく必要がある。 Bottom型に関して注意しておくべき最大のポイントは以下の二つ： Bottom型はすべての型の部分型である。ということはBottom型の式は他のど…

例外を投げるようなエラー処理のための型システムを追加していく。 今までの変更に比べて圧倒的に複雑なので複数回にわけている。 何が複雑かというと、「エラーが投げられた箇所の式の型は何か？」という問題の答えが「任意の型を取り得る」というものだか…

MLの一つの特徴として、デフォルトではほとんどの変数やデータ構造に破壊的代入が不可だが、破壊的代入が可能なデータ構造を明示的に選択することが可能、という非純粋な関数型プログラミング言語であることが挙げられる。そういった非純粋性を支える一つの…

再帰関数を定義できるようにするために不動点オペレータFixを追加する。型のないラムダ計算だと普通のラムダ抽象として定義できるのだが、STLCでは型をつけることができないので組み込みのオペレータとして用意する必要がある。 TaPLからの例を取ると： ff =…