前回に続いてミュータブルな型変数に対する破壊的代入で実装する効率的な単相型推論について見ていく。今回は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 =…

型システムにバリアント型とケースに対するパターンマッチを追加する。 こういうやつ： type t = Name of string | Id of int let to_str = function Name s -> s | Id n -> string_of_int n 代数的データ型における直和型であり、前回の直積型と合わせると…

前回のLetまで実装した型システムにレコードを追加する。 gist.github.com レコードというのは{x=1; y=true}のような値にラベルのついたデータ構造。ちなみにタプルは型システム的にはレコードの亜種と考えていい（ラベルが0~の整数だと見做せる）。どちらも…

前回のコードにLetによる変数束縛を追加する。 gist.github.com コードの追加としては2行のみと非常に短い。 型 変更なし 式 追加するのはLetだけ： type exp = ... | ELet of string * exp * exp ELet(変数、変数を束縛する式、本体の式）という構成になっ…

前回のSTLC+Boolに自然数と関連する機能を追加していく。 gist.github.com 型 TNatという自然数を表す型を追加： type ty = ... | TNat 式 三種類の式を追加： type exp = ... | ENat of int | EAdd of exp * exp | EIsZero of exp 自然数リテラルを表すENat…

前回のSTLCにBool型と関連する式を追加してみる： gist.github.com まずは型にTBoolを追加： type ty = ... | TBool 式にTrue, FalseとIf式を追加： type exp = ... | ETrue | EFalse | EIf of exp * exp * exp If式はcondition式、if-true-branch式、if-fal…

前回Simple Boolからはじめると書いたのだが、よく考えると単純型付きラムダ計算（STLC）ではじめるのが当然な筋な気がしてきた。 ので急遽Simple BoolからBoolを取っ払ってSTLCだけをまずみてみる： gist.github.com 定義されるものとしては 「型」を表す型…

最近は言語処理系に関してまったく手を動かしていなかった＆ブログに何も書いていなかったので練習がてら・・・ Types and Programming Languagesには非常にたくさんの型システムの実例と関連したOCamlコードが載っている。ただし多くは写経したらそのまま実…

Graydon Hoareが2019年にカナダのブリティッシュ・コロンビア大学でコンパイラ関連のゲスト講義した時の資料21 compilers and 3 orders of magnitude in 60 minutes - a wander through a weird landscape to the heart of compilationを読んだら大変面白か…

前回の記事でも紹介したOlin ShiversのT Programming Languageに関する回顧録で It had a big influence on Andrew Appel, at Princeton, who subsequently adopted a lot of the ideas in it when he and Dave MacQueen's group at Bell Labs built the SML…

CPS形式のコンパイラIRについて調べていてORBITというコンパイラについての話が出てきたので、1986年に出た論文ORBIT: An Optimizing Compiler for Schemeを読んでみた。 ORBITはGuy SteeleのRABBITというScheme Compilerから「CPS形式をIRとして使う」とい…

Abstract machines for programming language implementationを読んだのでメモ。 どのようなAbstract Machineがどのようなプログラミング言語の実装に使われてきたのか、というサーベイ。2000年に書かれており筆頭著者はHaskell界隈ではそれなりに知られてい…

A正規化について非常に参考にさせてもらっているMatt Mightのブログ記事で A later transformation to continuation-passing style (like that in Appel's book) is also simplified if transforming from A-Normal Form. とあるので、これまでのA正規化され…

前回のCEK抽象機械を拡張して、ミュータブルな状態のある言語も自然に実行できるようにする。 CESK抽象機械 CEK抽象機械はControl（実行する式）、Environment（変数環境）、Kontinuation（継続）の三つの要素を持つ。 CESK抽象機械はそこにStore（格納）を…

前回で定義した言語とそのA正規化されたIRをインタプリタで実行したい。 というわけでまたしてもMatt Mightのブログを参考にする： matt.might.net こちらのブログはCESKマシンの話だが、今のところ破壊的変更を言語機能として実装してないので、まずはCESK…

前回の言語に関数定義・適用を追加する。 単一引数の関数 まずは変更を簡単にするために「単一引数の関数」を実装する。 関数自体の式であるFnと関数適用のCallをASTに追加： type t = ... | Fn of string * t | Call of t * t α変換は関数式に関しては（仮…

前回に続いてA正規化の話。前回のミニマルな言語にブール型とifによる条件分岐を加える。実は条件分岐の正しいA正規化に関しては曖昧性があるようなので、後半はその話。 言語拡張 ASTに以下を追加： type t = ... | Bool of bool ... | Lt of t * t ... | I…