簡単な型システムを実装していく８ STLC+...+Variant+Fix

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

TaPLからの例を取ると：

ff = lambda ie : (Nat -> Bool).
        lambda x : Nat.
          if iszero x then true
          else if iszero (pred x) then false
          else ie (pred (pred x))

is_even = fix ff

というような使い方になる。ieというのはis_evenの略である。is_even関数を引数に取りis_even関数を返すような関数ffを定義して、そのffをfixに渡すとis_even関数が出来上がる、という寸法だ。「is_even関数を引数に取りis_even関数を返す」というと訳がわからないが、普通の再帰関数と同じで、停止条件を書くのと再起呼び出し時に渡す引数が小さくなっているという条件を満たすことで延々とループしないようになっている。

ffの型は何か。見てみると引数のieが(Nat -> Bool)で、返り値もNatを受け取りBoolを返す関数、つまり(Nat -> Bool)である。なのでff : (Nat -> Bool) -> (Nat -> Bool)、別の書き方をすると(Nat -> Bool) -> Nat -> Bool`である。

これは一般化できて、fixに渡すことのできるすべての「再帰関数の素」の型は(A -> B) -> (A -> B)となる。

gist.github.com

型

新しい型はなし。

式

式ひとつをとるFix式を用意する：

type exp =
...
| EFix of exp

typeof関数

let rec typeof env = function
...
| EFix e -> (match typeof env e with
    | TArrow(t11,t12) when t11 = t12 -> t11
    | TArrow _ -> failwith "type mismatch between parameter and return of fix"
    | _ -> failwith "arrow type expected")

前述のとおり

fixに渡すことのできるすべての「再帰関数の素」の型は(A -> B) -> (A -> B)となる。

なので| TArrow(t11,t12) when t11 = t12 -> t11でそれを確認している。

型推論がないので関数はすべて引数に対して型注釈がついている。なので再帰関数であろうと型検査するのは非常に楽だ。評価器関数を実装するのはもう少し複雑だろうが・・・。

実装しておいてなんだが、再帰関数をFixで表現する必要はあったのだろうか？OCamlなどで見るようなlet rec ... and ...構文のASTに対して直接型検査するのでもいい気がするのだが・・・

次回

次は破壊的代入が可能なref型を追加する。