簡単な型システムを実装していく8 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)
となる。
型
新しい型はなし。
式
式ひとつをとる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型を追加する。