簡単な型システムを実装していく１３ STLC+...+Error (4)

今回はtypeof関数がSTLCのVar, Abs, AppそしてBool, Nat, Let関連でどう部分型に対応していくかを見ていく。

まずは変わらない部分から。

EVar, EAbs, ETrue, EFalse, ENat, ELetは変わらない：

let rec typeof env = function
| EVar var -> List.assoc var env
| EAbs(var, t1, e1) -> TArrow(t1, typeof ((var,t1)::env) e1)
...
| ETrue | EFalse -> TBool
...
| ENat _ -> TNat
...
| ELet(var,e1,e2) -> typeof ((var, typeof env e1)::env) e2

これらのポイントは型の比較やパターンマッチがまったく行われていないところ。部分型による変更は、二つの型を比較するところから起きる。

関数適用のEApp：

| EApp(e1, e2) -> (match typeof env e1 with
   | TArrow(t11, t12) when is_subtype (typeof env e2) t11 -> t12
   | TArrow _ -> failwith "parameter type mismatch"
   | TBottom -> TBottom
   | _ -> failwith "non-arrow type in function position")

関数部分の型を調べるのに、まずそこがTBottomである可能性を新しく考慮に入れる必要があるのと、実引数の型が仮引数の型と合致しているのを調べるところを部分型関係（is_subtype）に代えなければいけなくなっている。

EIf：

| EIf(e1,e2,e3) ->
  if not (is_subtype (typeof env e1) TBool)
    then failwith "guard of conditional not boolean"
    else join (typeof env e2) (typeof env e3)

まず条件部分の型がTBoolの部分型であることを確認し、また結果となる二つの式の上位型を算出して返している。

EAddとEIsZero：

| EAdd(e1,e2) ->
  if is_subtype (typeof env e1) TNat && is_subtype (typeof env e2) TNat then TNat
  else failwith "non-nat argument(s) to add"
| EIsZero e ->
  if is_subtype (typeof env e) TNat then TBool
  else failwith "non-nat argument to iszero"

これら自然数に対する式は、引数の型がTNatであることを確認していたのが、TNatの部分型であることを確認するように変更している。

次回

次回は代数的データ型のためのレコードとバリアント、そして再帰関数のためのFixについて見ていく。