型推論を実装する その２ （型検査のある言語を作る）

前回登場したLETREC言語に型注釈と型検査をつけたCHECKED言語を実装する。

github.com

具体的には無名関数を定義するprocの仮引数、再帰関数を定義するletrecの仮引数と戻り値に対して型注釈を必要とし、その情報を元に型検査する。

型

CHECKEDで使う型は以下のように定義されている：

type t = Int
       | Bool
       | Proc of t * t

整数と真偽と、あとは任意の二つの型を組み合わせる関数のための再帰型。後者はネストが可能で(Bool -> Bool) -> Intなどといった型を作ったりできる。

型注釈の記述はこんな感じ：

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

これがパースされて、ASTに取り込まれる：

type t =
  | Const of int
  | Var of string
  | ZeroP of t
  | Diff of t * t
  | If of t * t * t
  | Let of string * t * t
  | Proc of string * Type.t * t
  | Call of t * t
  | LetRec of Type.t * string * string * Type.t * t * t

評価される時点ではこの型は無視される。式評価のためのEvalモジュールおよび評価結果の値を表すValモジュールにはTypeモジュールはまったく出てこない。

そのかわり、Evalモジュールと構造がよく似たTypecheckモジュールが定義されていて、Eval.fが呼ばれる前にTypecheck.fが呼ばれる。

型検査

型検査器の構造は評価器と非常に近い。まずは、変数の型を保持する型環境：

type env = (string * Type.t) list
let empty = []
let rec find tenv s = match tenv with
  | [] -> None
  | (s', t')::tenv' -> if s = s' then Some t' else find tenv' s
let extend tenv s t = (s, t)::tenv

Envと同じように別モジュールにわけてもよかったのだが、横着して同じモジュール内で定義してある。

次に型検査用の再帰関数check：

let rec check tenv = function
  | Exp.Const _ -> Type.Int

Constは当然Int型。

ZeroP、Diff、If：

  | Exp.ZeroP e -> (match check tenv e with
      | Type.Int -> Type.Bool
      | _ -> failwith "Non-numeric type passed to zero?")
  | Exp.Diff (e1, e2) -> (match check tenv e1, check tenv e2 with
      | Type.Int, Type.Int -> Type.Int
      | _ -> failwith "Non-numeric type passed to -(x,y)")
  | Exp.If (e1, e2, e3) -> (match check tenv e1 with
      | Type.Bool ->
          let t = check tenv e2 in
          if t = check tenv e3 then t
          else failwith "Different types in if then and else clauses"
      | _ -> failwith "Non-boolean passed as if condition")

各部分の型が期待通りであることを（再帰的にcheckを呼び出して）確かめ、その上で式全体の型を返す。

変数Var:

  | Exp.Var s -> (match find tenv s with
      | Some t -> t
      | None -> failwith "Variable not typed")

変数に対応する型が型環境に入っているので、それを取得する（評価時に変数に対応する値を環境から取得するのと全く同じ）。

変数束縛Let:

  | Exp.Let (s1, e1, e2) ->
      let t1 = check tenv e1 in
      let tenv' = extend tenv s1 t1 in
      check tenv' e2

変数に束縛される値の型を計算し、その対応関係を型環境にいれてからbody部分（e2）の型検査を行う。

関数Proc:

  | Exp.Proc (s, t, e) ->
      let tenv' = extend tenv s t in
      let rettype = check tenv' e in
      Type.Proc (t, rettype)

仮引数に型注釈がついているので、型環境に仮引数とその型の対応を入れて、関数のbody部分の型を検査。それで帰ってきた型が戻り値の型なので、関数自体の型は（仮引数の型 -> 戻り値の型）となる。

再帰関数LetRec:

  | Exp.LetRec (t1, fname, farg, t2, fbody, e) ->
      let t' = Type.Proc(t2, t1) in
      let tenv' = extend tenv fname t' in
      let tenv'' = extend tenv' farg t2 in
      (ignore @@ check tenv'' fbody; check tenv' e)

再帰関数の再帰部分もProcと同じように型検査しようとすると再帰的呼び出しにあたったところで、型環境に関数名がはいっていなくてエラーになってしまう。なので再帰関数の場合、仮引数だけではなく戻り値の型も注釈が必要で、それを元に関数の型を作成、型環境にいれる。その上で、まず関数body部分を仮引数とその型の対応を入れた新しい型環境を使って型検査し（これで再帰関数の戻り値部分の型注釈が正しいかどうかがわかる）、その後letrec ... in ...の後半部分を検査する。

関数呼び出しCall:

  | Exp.Call (e1, e2) -> (match check tenv e1 with
      | Type.Proc (t1, t2) ->
          if t1 = check tenv e2 then t2
          else failwith "Proc signature and argument types are mismatched"
      | _ -> failwith "Non-proc type in proc position of call")

関数部分の型を調べ、その型の仮引数部分と引数の型が合致しているかを確認した上で、関数の型の戻り値部分を「関数適用」全体の型として返す。

最後にEvalと全く同じように、check関数に空の環境を渡してTypecheck.f関数を作成している：

let f = check empty

使ってみる

高階関数を使ってみる：

>>> let f = proc (x:int) -(x, 1) in
let g = proc(h : (int -> int)) (h 1) in
(g f)

0

高階関数の型を間違えるとエラー：

>>> let f = proc (x:int) -(x, 1) in
let g = proc(h:int) (h 1) in
(g f)

Fatal error: exception Failure("Non-proc type in proc position of call")

再帰を使った例：

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

12

型があっていないと：

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

Fatal error: exception Failure("Non-numeric type passed to -(x,y)")

関数内にあるdoubleの呼び出しがboolを返すはずなのだが、その結果がその後intしか取らないはずの-(x, y)に渡されていて型検査が（正しく）失敗する。

これから

これで前準備は完了となり、次回はついに型推論を実装したINFERRED言語の話。