Hindley Milner型推論に機能を追加していく８ Fixの追加

再帰関数を定義するためのFixオペレータを言語に追加する。

型推論なしで追加した時の記事はこれ：

zehnpaard.hatenablog.com

Fixの使い方などはこの記事を参照してほしい。

今回のコードはここ

型

型には変更なし。

式

Fix式を追加：

type exp =
...
| EFix of exp

EFix式は別の式を一つ保持する。この別の式というのは：

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

この例でいうところのff関数のことだ。

typeof

EFix式の型推論：

let rec typeof env level = function
...
| EFix e -> match_rec_ty (typeof env level e)

保持するe式に対して型推論してから新しく定義するmatch_rec_ty関数に丸投げしている。

ちなみに型推論なしの時のコードはこのようなものだった：

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")

eが関数型で引数と返り値の型が同一であればいい、というもの。型推論ありだと型変数の扱いなども考える必要が出てくるが、基本的には同じ制約を適用すると考えていい。

match_rec_ty

というわけで今回の焦点であるmatch_rec_ty関数：

let rec match_rec_ty ty = match ty with
| TArrow(tparam,tret) -> unify tparam tret; tparam
| TVar {contents=Link ty} -> match_rec_ty ty
| TVar ({contents=Unbound(_,level)} as tvar) ->
  let tparam = new_tvar level in
  let tret = TVar(ref (Link tparam)) in
  tvar := Link(TArrow(tparam,tret));
  tparam
| TVar {contents=Generic _} -> failwith "Generic type encountered, expecting arrow or instantiated variable"
| _ -> failwith "Non-arrow type found in function position"

渡された型に対するパターンマッチ。（ここはlet rec match_rec_ty = function ...でもよかったな・・・）

特筆すべきケースはTArrowとTVar {contents=Unbound ...}な場合。個別に見ていく。

TArrow

| TArrow(tparam,tret) -> unify tparam tret; tparam

前述の通り、Fixに渡す関数は引数と返り値の型が合致している必要があるのでまずunifyして、成功したならどちらかの型を返す（単一化されているのでどちらでもいい）。

「引数と返り値の型が合致している」というのは例えばこのff関数を見てもらえば少し理解しやすいかと思う：

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))

ffはieという引数に(Nat -> Bool)な関数をとり、「xというNatな引数をとりBoolを返す」無名関数（つまりNat->Boolな関数）を返している。

TVar {contents=Unbound ...}

まだ制約のない型変数の場合：

| TVar ({contents=Unbound(_,level)} as tvar) ->
  let tparam = new_tvar level in
  let tret = TVar(ref (Link tparam)) in
  tvar := Link(TArrow(tparam,tret));
  tparam

新しく引数の型をnew_tvarで作り、返り値の型はそれに対するリンクにして、その二つをTArrowとして組み合わせ、大元の型変数をこのTArrowへのリンクに更新し、引数の型を全体の型として返す。

「返り値の型はそれに対するリンクにして、その二つをTArrowとして組み合わせ」の部分、コードでいうと：

  let tret = TVar(ref (Link tparam)) in
  tvar := Link(TArrow(tparam,tret));

ここに関しては本当にリンクを貼る必要があるのかわからない。別のtretを作らずtvar := Link(TArrow(tparam,tparam));にしてしまってもいいような気がするが影響が読みきれていないので安全策とした。

その他

その他の部分はmatch_fun_tyなどとほぼ同等：

...
| TVar {contents=Link ty} -> match_rec_ty ty
...
| TVar {contents=Generic _} -> failwith "Generic type encountered, expecting arrow or instantiated variable"
| _ -> failwith "Non-arrow type found in function position"

他の型へのリンクならリンクを辿って再帰的にmatch_rec_ty。Genericな型変数やTArrow以外の具体的な型ならエラー。

次回

再帰もできるようになって関数型プログラミング言語としての機能はそれなりになった。次回は破壊的代入が可能なRefを追加する。