Arantium Maestum

プログラミング、囲碁、読書の話題

型推論を実装する その1 (型なしの言語を作る)

とあるように、最近型推論や型クラスに興味があり、界隈では非常に著名なOleg先生の書いたものをなんとか読もうと考えている。(実はそれもModular Implicitsの論文をちゃんと理解するためなのだが、道は遠い・・・)

Essentials of Programming Languagesでは第七章で型推論のある言語をracketで実装するので、それをOCamlで試しつつ、具体的に何が起きているかをある程度メモっておこうと考えている。

EoPLの流れとしては * 第三章で再帰関数をサポートする純粋関数型言語LETRECを実装 * 第四章〜第六章では状態やCPSによる例外やスレッド実装など(型には直接関係なし) * 第七章ではまたLETREC言語に戻ってそこに型注釈・型検査ありのCHECKED言語、そしてCHECKEDから型注釈を省ける型推論付きのINFERRED言語を実装 となっている

なのでLETREC、CHECKED、INFERREDを見ていけば型無しから型推論への道が少しわかってくるはず。

今回はLETRECの実装をやっていく。

github.com

言語仕様

LETRECはその名の通り、再帰関数を使える言語である。かなり機能としては最低限に絞ってある。

  • 正数値リテラル
  • 数値間の引き算 -(x, y)
  • 数値のゼロチェック zero?(x)
  • 分岐 if ... then ... else
  • 変数束縛 let x = ... in ...
  • 再帰の無名関数 proc (x) ...
  • 再帰関数 letrec f (x) = ... in ...
  • 関数呼び出し (f x)

whitespaceは無意味(Lexerが取り除く)。

サンプルプログラム:

letrec double(x)
  = if zero?(x) then 0 else -((double -(x, 1)), -(0, 2))
  in
  (double 6)

これは12として評価される。

実装

パーサはocamllex/menhirで作成。この部分はとくに真新しいところはなし。(letlangについて書いた記事の内容を微調整しただけ)

以下の記事でも書いた:

zehnpaard.hatenablog.com

純粋関数型言語クロージャを持つ関数を実装する場合、クロージャを直接「変数環境」の型として表現してしまい、その型を含む直和型のバリアントを「関数」として値の型に追加するのが自然だと思う。しかし、変数環境自体が変数を表す文字列と、その変数の値とのマップとして表現している。というわけで変数環境の型と値の型が相互再帰になってしまうのをどう解決するか(というか相互再帰になっている型を二つのモジュールにどうわけるか)がポイント。

上記の記事の通り、Valenvモジュールを作って型を定義し、その型を使ってValEnvモジュールを定義している。

再帰関数を実装するために変数環境に少し工夫してある:

module Env = struct
  type t = envt

  let empty = Empty
  
  let rec find env s = match env with
    | Empty -> None
    | Extend (s', v', env') ->
        if s = s' then Some v'
        else find env' s
    | ExtendRec (fname, arg, body, env') ->
        if s = fname then Some (Val.Proc (arg, body, env)) 
        else find env' s 
  
  let extend env s v = Extend (s, v, env)
  let extend_rec env f a b = ExtendRec (f, a, b, env)
end

再帰関数を実現するために変数環境にExtendRec of string * string * Exp.t * Env.t(関数名、仮引数、関数の内容、元々の変数環境)のようなバリアントを入れ、その関数が参照されるたびに新たな関数値を作成して返している。

あまり効率のいいやり方とは言えない(EoPLでも破壊的代入を使ったより効率的な実装を演習問題として紹介している)が、まあ挙動は正しいのでよしとする。

実装の心臓部分はEvalモジュール。再帰関数eval'をパターンマッチで定義している。

まずは数値リテラルの式:

let rec eval' env = function
  | Exp.Const n -> Val.Num n

リテラルそのままの数値を表すValに評価される。

zero?-(x, y)

  | Exp.ZeroP e -> (match eval' env e with
      | Val.Num n -> Val.Bool (n = 0)
      | _ -> failwith "Zero-checking non-numeric value")
  | Exp.Diff (e1, e2) -> (match eval' env e1, eval' env e2 with
      | Val.Num n1, Val.Num n2 -> Val.Num (n1 - n2)
      | _ -> failwith "Diffing non-numeric value(s)")

まず引数を評価し、数値Valになることを確かめてから計算して結果を返している。

条件分岐:

  | Exp.If (e1, e2, e3) -> (match eval' env e1 with
      | Val.Bool b -> eval' env (if b then e2 else e3)
      | _ -> failwith "Using non-boolean if-condition")

まず条件を評価し、それを元に分岐の一方だけを評価している。

let式と束縛変数:

  | Exp.Let (s1, e1, e2) ->
      let v1 = eval' env e1 in
      let env' = Env.extend env s1 v1 in
      eval' env' e2
  | Exp.Var s -> (match Env.find env s with
      | Some v -> v
      | None -> failwith "Variable not found in environment")

letではまず束縛する値を評価し、それを変数とともに環境に加え、その拡張された環境を使ってbody部分を評価している。

変数の評価は環境から結果を探し出すだけ。

関数定義と呼び出し:

  | Exp.Proc (s, e) -> Val.Proc (s, e, env)
  | Exp.Call (e1, e2) -> (match eval' env e1 with
      | Val.Proc (s, e, env') ->
          let v = eval' env e2 in
          let env'' = Env.extend env' s v in
          eval' env'' e
      | _ -> failwith "Calling non-procedure")

関数定義は評価は全くせず、ただ仮引数とbody式と現在の環境をクロージャとしてVal.Procコンストラクタに渡すだけ。

関数呼び出しでは、まず関数部分を評価し関数Valだと確かめてから、引数を評価し、クロージャに仮引数とともに追加し、それを環境としてbody式を評価する。

再帰関数:

  | Exp.LetRec (fname, arg, body, e) ->
      eval' (Env.extend_rec env fname arg body) e

再帰関数は定義されるときは特殊なロジックがある(前述のExtendRecで変数環境を拡張する)が、関数呼び出しの際は非再帰関数と同じ扱い。

これでeval'は定義完了。あとは:

let f = eval' Env.empty

eval'に空の変数環境を与え、式だけを引数としてとる関数fを定義して終わり。

使ってみる

この言語を使ってみるために、bin/ex.mlにメイン関数的なものを用意する:

open Letreclang

let f s =
  Lexing.from_string s
  |> Parser.f Lexer.f
  |> Eval.f
  |> Val.to_str
  |> print_endline

let rec rep acc =
  let s = read_line () in
  if s = "" then f acc
  else rep (acc ^ "\n" ^ s)

let _ = (print_string ">>> "; rep "")

これでbashなどでdune exec bin/ex.bcというコマンドを叩くと >>>というプロンプトが表示され、複数行にまたがる文字列を入力として受け取り(空行を入力の終わりとして解釈する)、パース・評価して結果を表示する。

例えば:

$ dune exec bin/ex.bc
>>> letrec double(x)
  = if zero?(x) then 0 else -((double -(x, 1)), -(0, 2))
  in
  (double 6)

12

これから

前述の通り、次はこの言語に型注釈と型検査を加える。