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

今回はtypeof関数がレコード、バリアント、Fix関連でどう部分型に対応していくかを見ていく。

レコード

レコードはフィールドの値が一つでもBottom型だったら全体がBottom型になる：

| ERecord les ->
  let lts = (List.map (fun (l,e)->(l, typeof env e)) les) in
  if List.exists (fun (_,t) -> t = TBottom) lts then TBottom
  else TRecord lts

ただしBottom型そのままではなくBottom型を含む型（例えば関数型）であればレコードの中にBottomが入ることも可能。

レコードのフィールドアクセス：

| EProj(e,l) -> (match typeof env e with
    | TRecord(lts) -> List.assoc l lts
    | TBottom -> TBottom
    | _ -> failwith "record type expected")

パターンマッチでTBottom型のケースを追加するだけ。

バリアントとパターンマッチ

バリアント型の値を作成するETag：

| ETag(l,e,t) -> (match t with
    | TVariant lts -> 
      let t' = List.assoc l lts in
      if is_subtype (typeof env e) t' then t
      else failwith "field does not have expected type"
    | _ -> failwith "annotation is not a variant type")

今まで通り、ETag式に明示的な型注釈が必要なことに注意。if t' = (typeof env e) ...がif is_subtype (typeof env e) t' ...になっている。

バリアントに対するパターンマッチのECase式：

| ECase(e, cases) -> (match typeof env e with
    | TVariant lts ->
      let labels = List.map fst cases in
      let is_label_in_type l = List.mem_assoc l lts in
      if not (List.for_all is_label_in_type labels) then failwith "label mismatch between case and type";
      let typeof_case_exp (l,(var,exp)) = typeof ((var,List.assoc l lts)::env) exp in
      let ts = List.map typeof_case_exp cases in
      List.fold_left join TBottom ts
    | TBottom -> TBottom
    | _ -> failwith "variant type expected")

TVariant ltsに対するケースの最後にあるList.fold_left join TBottom tsで、例えば{x:int->int, y:bool->bottom}と{x:int->bottom, y:bool->bool}という型に評価されるケースを持つパターンマッチ式全体の結果の型を{x:int->int, y:bool->bool}として算出することができる。

再帰用のFix

EFix式に対するケース：

| EFix e -> (match typeof env e with
    | TArrow(t11,t12) when is_subtype t12 t11 -> t11
    | TArrow _ -> failwith "type mismatch between parameter and return of fix"
    | TBottom -> TBottom
    | _ -> failwith "arrow type expected")

TArrow(t11,t12) when t12 = t11 -> t11が... when is_subtype t12 t11 ...になっているのとTBottomケースが追加されている。

次回

RefとErrorに対するtypeof関数の部分型対応を見ていく。これでエラーに関しての話は終わり。