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コードが載っている。ただし多くは写経したらそのまま実…

前回はSubstitution関連で少し寄り道したが、今回こそはPrincipal Type Schemes for Functional Programsの中核である type inference Robinson's unification algorithm algorithm W の話。 type inference For assumptions A, expressions e and type-sche…

前回「type inference、Robinson's unification, algorithm Wを見ていく」と書いたが、その前にsubstitutionについてつらつらと考えてみたい。 S is a substitution of types for type variables, often written [τ_1/α_1,...,τ_n/α_n] or [τ_i/α_i] とある…

型推論のためのAlgorithm Wを実装するため、DamasとMilnerのPrincipal Type Schemes for Functional Programsを読んでいる。 重要そうな概念としては expression type/type-scheme substitution instance/generic instance assumption assertion closure typ…

プログラミング言語理論に関係する論文を結構読み散らかしているのだが、あまりしっかりアウトプットする機会もないので読み込みも甘いし記憶も曖昧になる。 というわけで面白そうなやつは、内容・背景・感想などをブログにメモとして残していこうと考えた。…