この記事は言語実装 Advent Calendar 2020 の5日目の記事です．
一度でも型推論器を書いたことがあれば，そのあまりの邪悪さ，あるいはその複雑さに恐れ慄いたことでしょう． 参照を用いて単一化を実現しようものなら構文木は参照に汚染され，純粋関数型に実装しようものなら大量の型代入をどのような順序で適用したものか悩まされる． これは Hindley-Milner 型推論器を実装する上での宿命のようなものです．
本記事では，MLのサブセット——型付きλ計算をletと参照で拡張した，let多相をサポートする言語——の型推論器を Coq で実装し，その正当性を証明します． Coq で検証を行うことで我々は型推論器のバグへの恐怖とデバッグの労力から真に解放され，枕を高くして眠ることができることでしょう． もっとも、型付きλ計算を let 多相で拡張した言語の型推論器の正当性は実はすでに証明していて， あとは対象言語を参照で拡張するだけという話もありますが．
本記事で実装する型推論器とその正当性，型安全性の証明は GitHub にあるので，Coq のコードを眺めながら 記事を読みたい方はそちらを参照してください．
let多相と参照型
何故本記事で扱う ML のサブセットは参照をサポートするのでしょうか？それは，多相型と参照（のような副作用のある計算）の両立には本質的に注意を要することが理由として挙げられます．
例えば，以下のように参照に関数を代入するプログラムを考えてみましょう．構文と意味は概ね OCaml のものに準じます．
# let r = ref (fun x -> x);; val r : ('a -> 'a) ref = {contents = <fun>}
let 多相を扱えるような言語に何も考えずに参照を追加してしまうと， r には 'a -> 'a 型が付いてしまいます．ref (fun x -> x) は ('_a -> '_a) ref 型が付き，単相の型変数 '_a は型環境に現れませんからね．
そのため，以下のようにして型安全性を壊す——型チェックを通っているにもかかわらず評価できない式に簡約される——ようなプログラムが書けてしまいます．
# r := (fun x -> x + 1);; - : unit = () # !r ();; (* () + 1 となり実行時エラーが発生する *)
このような不都合のなきよう，現実の ML 処理系では let で闇雲に多相型を導入せず，様々な制限を設けています．
OCaml で実装されている緩い値制限， SML# で実装されているランク1多相などが有名ですね．
もっとも，それらを導入すると型安全性の証明や型推論器の実装が大変になったりするので，この記事ではそれら巧妙な実装には立ち入らず単純な値制限を取り扱うことにします．
値制限とは， let 式 let x = e1 in e2 において， e1 が値の場合のみ多相型を導入するような制限です．
例えば上の例 let r = ref (fun x -> x);; r := (fun x -> x + 1);; !r ();; では， ref (fun x -> x) は値ではありませんから r には単相の ('_a -> '_a) ref 型が付き，
# let r = ref (fun x -> x);; val r : ('_a -> '_a) ref = {contents = <fun>}
fun x -> x + 1 を代入すれば r の型は単一化によって (int -> int) ref に固定されます．
# r := (fun x -> x + 1);; - : unit = () # r;; - : (int -> int) ref = {contents = <fun>}
従ってrはもはやint -> int型の参照としか用いることはできず，!r ()のようにunit型を受け取る関数として使おうものなら，問答無用で型エラーになります．
# !r ();; Error : This expression has type unit but an expression was expected of type int
実行時のエラーをコンパイル時の型エラーとして検知できて素晴らしいですね．
対象言語の拡張
それでは実際に，λ計算を let 多相で拡張した言語を拡張し，参照を扱えるようにしましょう．
まず型の構文の定義に，OCaml で言うところの unit 型と 'a ref 型を追加して，以下のように変更します．
Inductive typ : Set := | typ_unit | typ_fvar (x : nat) | typ_bvar (n : nat) | typ_ref (T : typ) | typ_arrow (T1 T2 : typ).
typ_unit が unit 型に， typ_ref A が 'a ref 型に対応しています．それ以外のコンストラクタが何に対応しているかは以前の記事を参照のこと．
OCaml と違って Coq の型引数は後置なので，OCaml で言うところの unit ref みたいな型はこの定義だと typ_ref typ_unit みたいな式で表現することに注意して下さい．
次にプログラムの構文の定義に，参照セルへのポインタおよび，OCaml で言うところの unit 型の即値 ()，参照セルの生成 ref e，参照セルの中身の読み出し !e，参照セルへの破壊的代入 e1 := e2 を追加して，以下のように変更します．
Inductive trm : Set := | trm_unit | trm_var (n : nat) | trm_loc (l : nat) | trm_abs (t : trm) | trm_app (t1 t2 : trm) | trm_ref (t : trm) | trm_deref (t : trm) | trm_update (t1 t2 : trm) | trm_let (t1 t2 : trm).
trm_loc l が参照セルへのポインタに，`trm_unit が () に， trm_ref t が ref e に，trm_deref t が !e に， trm_update t1 t2 が e1 := e2 に対応しています．
割と見れば分かる類なんですがそれ以外のコンストラクタが何を表しているかについて一応解説しておくと，trm_var n が変数 x 1 で，
trm_abs t が無名関数 fun x -> e 2， trm_app t1 t2 が関数適用 e1 e2， trm_let e1 e2 が let x = e1 in e2 3に対応します．
let rec x = e1 in e2 に対応する式は無いんですが，参照を使えば以下のように再帰関数を定義できるので，特に計算能力を損なっている訳ではありません．
# let f = ref (fun x -> x);; val f : ('_a -> '_a) ref = {contents = <fun>} # let fib n = if n <= 1 then n else !f (n - 1) + !f (n - 2);; val fib : int -> int = <fun> # f := fib;; - : unit = () # fib 6;; - : int = 8
ここで，参照セルへのポインタというのは OCaml には対応する式が無いのですが，小ステップ操作的意味論を定義する都合から，プログラムの構文の定義に追加しています．
と言うのも，簡約前のヒープ と項
の組と，簡約後のヒープ
と項
の組の，2項関係として簡約
を定義しようとすると，
実行時にしか現れない参照セルへのポインタ
も式として扱える方が都合が良いんですよね4．Garrigue 先生の論文で緩い値制限の型安全性を証明する時に使われてた小ステップ操作的意味論みたいに，評価文脈を使えば参照セルへのポインタの構文を変数の構文で代用できる話もありますが，まぁ Coq で評価文脈扱うのは別の大変さがあるので．
一応簡約の定義がどうなるか書いておくと，以下のようになります．関係の名前を見れば分かる通り，値呼び（call-by-value）の評価戦略ですね． まぁ ML のサブセットと聞いて non-strict な評価戦略を採用していると思う人は居ないと思いますが．
Inductive cbv H : trm -> seq trm -> trm -> Prop := | cbv_app t11 v2 : value v2 -> cbv H (trm_app (trm_abs t11) v2) H (subst (scons v2 var) t11) | cbv_app_1 H' t1 t1' t2 : cbv H t1 H' t1' -> cbv H (trm_app t1 t2) H' (trm_app t1' t2) | cbv_app_2 H' v1 t2 t2' : value v1 -> cbv H t2 H' t2' -> cbv H (trm_app v1 t2) H' (trm_app v1 t2') | cbv_ref v : value v -> cbv H (trm_ref v) (rcons H v) (trm_loc (size H)) | cbv_ref_1 H' t t' : cbv H t H' t' -> cbv H (trm_ref t) H' (trm_ref t') | cbv_deref l v : (forall d, nth d H l = v) -> cbv H (trm_deref (trm_loc l)) H v | cbv_deref_1 H' t t' : cbv H t H' t' -> cbv H (trm_deref t) H' (trm_deref t') | cbv_update l v2 : value v2 -> cbv H (trm_update (trm_loc l) v2) (set_nth trm_unit H l v2) trm_unit | cbv_update_1 H' t1 t1' t2 : cbv H t1 H' t1' -> cbv H (trm_update t1 t2) H' (trm_update t1' t2) | cbv_update_2 H' v1 t2 t2' : value v1 -> cbv H t2 H' t2' -> cbv H (trm_update v1 t2) H' (trm_update v1 t2') | cbv_let v1 t2 : value v1 -> cbv H (trm_let v1 t2) H (subst (scons v1 var) t2) | cbv_let_1 H' t1 t1' t2 : cbv H t1 H' t1' -> cbv H (trm_let t1 t2) H' (trm_let t1' t2).
参照を扱えるように構文（と操作的意味論）を拡張したので，いよいよ待ちに待った型システムの拡張です．
一般的な let 多相をサポートする型システムでは，let の型付け規則は
「let で束縛される変数の型に現れる型変数のうち，型環境に現れないものは一般化して良い」
といった定義を採用することが多いのですが，前回の記事で let 多相に対応した際はより宣言的に，
「let で束縛される変数の型に現れる型変数のうち，適当な名前に変えても依然として型付けできるようなものは一般化しても良い」
といった風情の定義を採用していました．
Inductive typed : env -> trm -> typ -> Prop := (* 中略 *) | typed_let (L : seq nat) G t1 t2 T1 T2 : (forall s, (forall x, exists2 y, s x = typ_fvar y & y \notin L) -> typed G t1 (typ_open s T1)) -> typed (T1 :: G) t2 T2 -> typed G (trm_let t1 t2) T2.
この方針での定義は参照を扱えるように型システムを拡張する際にも威力を発揮します．
と言うのも，参照を扱えるように型システムを拡張しようとすると，あるアドレスに入っている値の型を表すストア型付け で型付け関係を拡張したくなるのですが，
このストア型付け
は参照セルへのアドレス版の環境みたいなものなので，ここに現れる型変数も一般化してはいけない訳です．
にもかかわらず型安全性の証明では，簡約が進むごとにストア型付けがどんどん拡張されていくので，
一般的な方針で let の型付け規則を定義してしまうと量化する型変数を相当注意深く選ばないと証明が立ち行かなくなってしまいます．
その点ここで採用した let の型付け規則というのは，どのような型を代入しても型付けが成功するような型変数は一般化しても良いと言っているようなもの5 なので， 型付け関係がストア型付けで拡張されてもそのまま使うことができます．
それでは，参照を扱えるように拡張した型付け規則を見ていきましょう．
Inductive typed M : env -> trm -> typ -> Prop := | typed_unit G : typed M G trm_unit typ_unit | typed_var G x s T : (forall d, nth d G x = T) -> (forall x, typ_bv (s x) =i pred0) -> typed M G (trm_var x) (typ_open s T) | typed_loc G l T : typ_bv T =i pred0 -> (forall d, nth d M l = T) -> typed M G (trm_loc l) (typ_ref T) | typed_abs G t T1 T2 : typ_bv T1 =i pred0 -> typed M (T1 :: G) t T2 -> typed M G (trm_abs t) (typ_arrow T1 T2) | typed_app G t1 t2 T1 T2 : typed M G t1 (typ_arrow T1 T2) -> typed M G t2 T1 -> typed M G (trm_app t1 t2) T2 | typed_ref G t T : typed M G t T -> typed M G (trm_ref t) (typ_ref T) | typed_deref G t T : typed M G t (typ_ref T) -> typed M G (trm_deref t) T | typed_update G t1 t2 T : typed M G t1 (typ_ref T) -> typed M G t2 T -> typed M G (trm_update t1 t2) typ_unit | typed_let (L : seq nat) G t1 t2 T1 T2 : value t1 -> (forall s, (forall x, exists2 y, s x = typ_fvar y & y \notin L) -> typed M G t1 (typ_open s T1)) -> typed M (T1 :: G) t2 T2 -> typed M G (trm_let t1 t2) T2.
参照セルへのポインタ trm_loc l の型はストア型付け M から持ってくることと，
値制限のために let 式 trm_let t1 t2 における変数に束縛される式 t1 が値でなければならないこと以外は自然な定義でしょうか．
この定義だと変数に束縛される式 t1 が値ではないような let 式 trm_let t1 t2 には型が付かないんですが，
多相型の付かない let 式なんて (fun x -> e1) e2 で代用できる程度の存在でしかないので．
ここで，何故実行時にしか現れないはずの参照セルへのポインタにまで型付け規則が必要なのか，補足をしておきましょう． 型安全性——型チェックを通っていれば評価できない式に簡約されない——を証明する際に一般的なのが， 進行定理——型チェックを通った式は評価できない式ではない性質——と保存定理——型チェックを通った式を簡約した式も型チェックを通る性質——を用いることです． 後者が成り立つためには簡約後の式，つまり実行時の式に型を付ける必要があり，実行時にしか現れない参照セルへのポインタにも型付け規則が必要という訳です．
型推論器の拡張と，その正当性の証明の修正
参照を扱えるように対象言語を拡張しましたから，この記事の主題の1つである型推論器の拡張を行いましょう． 型付け関係を定義する際，型安全性の証明の都合から，実行時にしか現れないはずの参照セルへのポインタにまで型付け規則を与える必要がありました． 一方で型推論器にはそのような制約も無いので，参照セルへのポインタには型が付かなくても良く，ストア型付けを考慮する必要がありません． 従って，型推論を行う関数は引数を増やす必要もなく場合分けを追加するだけで，まるで四則演算を実装するかのような気楽さで参照に対応できます．
まぁ，いくら straightforward とはいえ，場合分けの数が数なので実装量は多いですが．
Fixpoint typing n G t := match t with | trm_unit => Some (n, typ_fvar, typ_unit) | trm_var x => omap (fun T => ((n + maximum (typ_enum_bv T [::])).+1, typ_fvar, typ_open (typ_fvar \o addn n) T)) (nth None (map Some G) x) | trm_loc _ => None | trm_abs t => omap (fun '(m, s, T2) => (m, s, typ_arrow (s n) T2)) (typing n.+1 (typ_fvar n :: G) t) | trm_app t1 t2 => match typing n G t1 with | None => None | Some (n1, s1, T1) => match typing n1 (env_subst s1 G) t2 with | None => None | Some (n2, s2, T2) => omap (fun s3 => (n2.+1, typ_subst (typ_subst s3 \o s2) \o s1, s3 n2)) (typ_unify (typ_subst s2 T1) (typ_arrow T2 (typ_fvar n2))) end end | trm_ref t => omap (fun '(m, s, T) => (m, s, typ_ref T)) (typing n G t) | trm_deref t => match typing n G t with | None => None | Some (n1, s1, T) => omap (fun 's2 => (n1.+1, typ_subst s2 \o s1, s2 n1)) (typ_unify T (typ_ref (typ_fvar n1))) end | trm_update t1 t2 => match typing n G t1 with | None => None | Some (n1, s1, T1) => match typing n1 (env_subst s1 G) t2 with | None => None | Some (n2, s2, T2) => omap (fun s3 => (n2, typ_subst (typ_subst s3 \o s2) \o s1, typ_unit)) (typ_unify (typ_subst s2 T1) (typ_ref T2)) end end | trm_let t1 t2 => if value t1 then match typing n G t1 with | None => None | Some (n1, s1, T1) => match typing n1 (typ_gen (env_fv (env_subst s1 G)) T1 :: env_subst s1 G) t2 with | None => None | Some (n2, s2, T2) => Some (n2, typ_subst s2 \o s1, T2) end end else None end.
型推論器の実装として自明ではないところがあるとすれば，let 式 trm_let t1 t2 を型付けする際に，t1 が既に値になっているか（値制限を満たしているか）を検査していることぐらいでしょうか．
実は型推論器を実装して正当性を証明する分には，参照を追加しても大して困らなかったりします．考慮が必要なのは型安全性の証明ですね．
ちなみに，型推論器を実装する時の型の一般化がどうとか fresh な型変数をどうやって持ってくるかとかについては，前回の記事や前々回の記事を参照してください．
それでは参照を扱えるように型推論器を拡張したことですし，型推論器の正当性——あるプログラムの型推論が成功することと，そのプログラムに型が付くことが同値であること——のうちの一方向の性質，型推論器の健全性——あるプログラムの型推論が成功したならば，そのプログラムには型推論器の返した型が付くこと——の証明を修正しましょう． 実行時にしか現れない式の型付けをサボったお陰でストア型付けを扱う必要が無くなったので，健全性のステートメントは let 多相だけ扱ってた時と殆ど変わりません．型が付くことを言うときに空なストア型付けを引数に追加しただけ．
Theorem typing_sound : forall t n m G s T, typing n G t = Some (m, s, T) -> typed [::] (env_subst s G) t T /\ forall x, typ_bv (s x) =i pred0.
そればかりか，証明の修正も単純に場合分けのケースが増えるだけで straightforward だったりします．
Proof. elim => /= [ | x ? ? G ? ? | // | t IHt n ? G ? ? | t1 IHt1 t2 IHt2 n ? G ? ? | t IHt n ? G ? ? | t IHt n ? G ? ? | t1 IHt1 t2 IHt2 n ? G ? ? | t1 IHt1 t2 IHt2 n ? G ? ? ]. - by inversion 1 => /=. - case (leqP (size G) x) => ?. + by rewrite nth_default // size_map. + rewrite (nth_map (typ_fvar 0)) //. inversion 1. rewrite env_subst_fvar. split => [ | ? // ]. apply /typed_var => // ?. exact /set_nth_default. - destruct (typing n.+1 (typ_fvar n :: G) t) as [ [ [ ? ? ] ] | ] eqn:Htyping; inversion 1. subst. move: (IHt _ _ _ _ _ Htyping) => [ ? ? ]. eauto. - destruct (typing n G t1) as [ [ [ n1 s1 ] T1 ] | ] eqn:Htyping1 => //. destruct (typing n1 (env_subst s1 G) t2) as [ [ [ n2 s2 ] T2 ] | ] eqn:Htyping2 => //. destruct (typ_unify (typ_subst s2 T1) (typ_arrow T2 (typ_fvar n2))) as [ s3 | ] eqn:Hunify; inversion 1. subst. case (IHt1 _ _ _ _ _ Htyping1) => ? Hs1bv. case (IHt2 _ _ _ _ _ Htyping2) => Htyped2 Hs2bv. have Htyped1' : typed [::] (env_subst s2 (env_subst s1 G)) t1 (typ_subst s2 T1). { exact /(typed_subst_typ [::]). } have : forall x, typ_bv (s3 x) =i pred0 => [ ? x | Hs3bv ]. { apply /negbTE /negP => /(typ_bv_unify _ _ _ Hunify) [ | /= ]. - by rewrite (typed_closed _ _ _ _ Htyped1'). - move: (typed_closed _ _ _ _ Htyped2 x). by rewrite -!topredE => /= ->. } split => [ | ? ? ]. + rewrite -!env_subst_comp. apply /(typed_app _ _ _ _ (typ_subst s3 T2)). * move: (typ_unify_sound _ _ _ Hunify) => /= <-. apply /(typed_subst_typ [::]); eauto. * apply /(typed_subst_typ [::]); eauto. + rewrite typ_bv_subst Hs1bv. apply /negbTE /negP => /hasP [ ? ? ]. rewrite /= typ_bv_subst Hs2bv => /hasP [ ? ? ]. by rewrite Hs3bv. - destruct (typing n G t) as [ [ [ m s ] T ] | ] eqn:Htyping; inversion 1. subst. case (IHt _ _ _ _ _ Htyping). eauto. - destruct (typing n G t) as [ [ [ n1 s1 ] T ] | ] eqn:Htyping => //. destruct (typ_unify T (typ_ref (typ_fvar n1))) as [ s2 | ] eqn:Hunify; inversion 1. subst. case (IHt _ _ _ _ _ Htyping) => Htyped Hs1bv. have : forall x, typ_bv (s2 x) =i pred0 => [ ? x | Hs2bv ]. { apply /negbTE /negP => /(typ_bv_unify _ _ _ Hunify) [ | // ]. by rewrite (typed_closed _ _ _ _ Htyped). } split => [ | ? ? ]. + rewrite -!env_subst_comp. apply /typed_deref. move: (typ_unify_sound _ _ _ Hunify) => /= <-. exact /(typed_subst_typ [::]). + rewrite typ_bv_subst Hs1bv. apply /negbTE /negP => /hasP [ ? ? ]. by rewrite Hs2bv. - destruct (typing n G t1) as [ [ [ n1 s1 ] T1 ] | ] eqn:Htyping1 => //. destruct (typing n1 (env_subst s1 G) t2) as [ [ [ n2 s2 ] T2 ] | ] eqn:Htyping2 => //. destruct (typ_unify (typ_subst s2 T1) (typ_ref T2)) as [ s3 | ] eqn:Hunify; inversion 1. subst. case (IHt1 _ _ _ _ _ Htyping1) => ? Hs1bv. case (IHt2 _ _ _ _ _ Htyping2) => Htyped2 Hs2bv. have Htyped1' : typed [::] (env_subst s2 (env_subst s1 G)) t1 (typ_subst s2 T1). { exact /(typed_subst_typ [::]). } have : forall x, typ_bv (s3 x) =i pred0 => [ ? x | Hs3bv ]. { apply /negbTE /negP => /(typ_bv_unify _ _ _ Hunify) [ | /= ]. - by rewrite (typed_closed _ _ _ _ Htyped1'). - by rewrite (typed_closed _ _ _ _ Htyped2). } split => [ | ? ? ]. + rewrite -!env_subst_comp. apply /(typed_update _ _ _ _ (typ_subst s3 T2)); [ move: (typ_unify_sound _ _ _ Hunify) => /= <- | ]; exact /(typed_subst_typ [::]). + rewrite typ_bv_subst Hs1bv. apply /negbTE /negP => /hasP [ ? ? ] /=. rewrite typ_bv_subst Hs2bv => /hasP [ ? ? ]. by rewrite Hs3bv. - destruct (value t1) eqn:Hvalue => //. destruct (typing n G t1) as [ [ [ n1 s1 ] T1 ] | ] eqn:Htyping1 => //. destruct (typing n1 (typ_gen (env_fv (env_subst s1 G)) T1 :: env_subst s1 G) t2) as [ [ [ n2 s2 ] T2 ] | ] eqn:Htyping2; inversion 1. subst. case (IHt1 _ _ _ _ _ Htyping1) => Htyped1 Hclosed1. case (IHt2 _ _ _ _ _ Htyping2) => ? Hclosed2. split => [ | ? ? ]. + rewrite -env_subst_comp. (apply /(typed_let _ (env_enum_fv (env_subst s1 G) [::])); eauto) => s Hs. rewrite typ_subst_comp typ_open_subst_distr => [ | ? ]. { rewrite typ_open_bvar_eq => [ | ? ]. - rewrite (env_subst_ext s2 (typ_open s \o (typ_subst s2 \o (fun x => if x \in env_fv (env_subst s1 G) then typ_fvar x else typ_bvar x)))) => [ | ? /= -> /= ]. + apply /(typed_subst_typ [::]) => //= x ?. rewrite typ_bv_open. apply /negbTE /negP => /hasP [ y ]. case (Hs y) => ? -> //. + rewrite typ_open_bvar_eq => // ?. by rewrite Hclosed2. - by rewrite (typed_closed _ _ _ _ Htyped1). } by rewrite (typed_closed _ _ _ _ Htyped1). + rewrite typ_bv_subst Hclosed1. apply /negbTE /negP => /hasP [ ? ]. by rewrite Hclosed2. Qed.
何しろ前回 let 多相をサポートする時に鬼門だった， let の型推論が健全であることの証明が殆ど変わってませんからね． let の型付け規則をいい感じに定義した甲斐もあるというものです．6
型推論器の正当性のもう一方向の性質，型推論器の完全性——あるプログラムに型が付くならば，そのプログラムに対しての型推論が成功すること——についても，そのステートメントは let 多相だけ扱ってた時と殆ど変わりません．こちらも型が付くことを仮定するときに空なストア型付けを引数に追加するだけです．
Theorem typing_complete : forall t n G s T, {in env_fv G, forall x, typ_bv (s x) =i pred0} -> (forall x, x \in env_fv G -> x < n) -> typed [::] (env_subst s G) t T -> exists m s' s'' T', typing n G t = Some (m, s', T') /\ n <= m /\ T = typ_subst s'' T' /\ typ_bv T' =i pred0 /\ (forall x, typ_bv (s' x) =i pred0) /\ (forall x y, x \in typ_fv (s' y) -> x = y \/ x < m) /\ (forall x, x \in typ_fv T' -> x < m) /\ (forall x, x < n -> s x = typ_subst s'' (s' x)).
お察しの通り，完全性の証明も場合分けを追加するだけで straightforward に修正できます．
Proof. elim => /= [ | x | l | t IHt | t1 IHt1 t2 IHt2 | t IHt | t IHt | t1 IHt1 t2 IHt2 | t1 IHt1 t2 IHt2 ] n G s T Hclos HG; inversion 1; subst. - (repeat eexists; eauto) => /= ? ?. rewrite inE => /eqP. eauto. - case (leqP (size G) x) => ?. { move: (H1 (typ_fvar 0)). by rewrite -(H1 (typ_bvar 0)) !nth_default // size_map. } exists ((n + maximum (typ_enum_bv (nth (typ_fvar 0) G x) [::])).+1), typ_fvar, (fun x => if x < n then s x else s0 (x - n)), (typ_open (typ_fvar \o addn n) (nth (typ_fvar 0) G x)). (repeat split) => [ | | | ? | ? ? /= | ? /typ_fv_open_elim [ ? | [ ? /= ] ] | ? /= -> // ]. + by rewrite (nth_map (typ_fvar 0)). + apply /leqW /leq_addr. + rewrite -(H1 (typ_fvar 0)) /env_subst (nth_map (typ_fvar 0)) // typ_subst_open_distr => [ | /= x0 ? ? ]. { rewrite (typ_subst_ext (fun x => if x < n then s x else s0 (x - n)) s) => [ | ? ? ]. - apply /typ_open_ext => ? ? /=. by rewrite ltnNge leq_addr /= addKn. - by rewrite HG // (env_fv_intro (nth (typ_fvar 0) G x)) // mem_nth. } by rewrite HG ?Hclos // (env_fv_intro (nth (typ_fvar 0) G x)) // mem_nth. + rewrite typ_bv_open. by apply /negbTE /negP => /hasP [ ? ]. + rewrite inE => /eqP. eauto. + apply /leqW /ltn_addr /HG /(env_fv_intro (nth (typ_fvar 0) G x)) => //. exact /mem_nth. + rewrite inE => /eqP -> ?. by rewrite ltnS leq_add2l maximum_sup // typ_enum_bv_inE_aux in_nil orbF. - move: (H3 typ_unit). by rewrite -(H3 (typ_fvar 0)) !nth_default. - move: (IHt n.+1 (typ_fvar n :: G) (fun x => if x < n then s x else T1) T2) => /= [ ? /orP [ /eqP -> | Hin ] | ? /orP [ /eqP -> | /HG /leqW // ] | | n1 [ s1 [ s' [ T' [ -> [ Hn1 [ -> [ HT'bv [ Hs1bv [ Hs1fv [ HT'fv Hs1 ] ] ] ] ] ] ] ] ] ] ]. { by rewrite ltnn. } { rewrite HG //. exact /Hclos /Hin. } { exact /leqnn. } { by rewrite ltnn -(env_subst_ext s) => // ? /HG ->. } exists n1, s1, s', (typ_arrow (s1 n) T'). (repeat split) => //= [ | | x | ? | ? Hlt ]. + exact /ltnW. + by rewrite -Hs1 // ltnn. + move: (HT'bv x) (Hs1bv n x). by rewrite -!topredE => /= -> ->. + by rewrite inE => /orP [ /Hs1fv [ -> | ] | /HT'fv ]. + rewrite -Hs1 ?Hlt => //. exact /leqW. - move: (IHt1 n G s (typ_arrow T1 T)) => [ ] // n1 [ s1 [ s' [ T2' [ -> [ Hn1 [ HT [ HT2'bv [ Hs1bv [ Hs1fv [ HTfv Hs ] ] ] ] ] ] ] ] ] ]. move: (IHt2 n1 (env_subst s1 G) s' T1) => [ ? /env_fv_subst_elim [ x ? ? ] z | ? /env_fv_subst_elim [ ? /Hs1fv [ -> /HG /((@leq_trans _ _ _)^~Hn1) | ] // ] | | n2 [ s2 [ s'' [ T1' [ -> [ Hn2 [ HT1 [ HT1'bv [ Hs2bv [ Hs2fv [ HT1fv Hs' ] ] ] ] ] ] ] ] ] ] ]. { apply /negbTE /negP => ?. have : z \in typ_bv (typ_subst s' (s1 x)). { apply /typ_bv_subst_intro_sub; eauto. } by rewrite -Hs ?Hclos ?HG. } { by rewrite env_subst_comp -(env_subst_ext s) => // ? /= /HG /Hs. } move: (typ_unify_complete (typ_subst s2 T2') (typ_arrow T1' (typ_fvar n2)) (fun x => if x < n2 then s'' x else T)) => [ | s3 [ Hunify [ s''' Hgen ] ] ] /=. { rewrite ltnn !(typ_subst_ext (fun x => if x < n2 then s'' x else T) s'') => [ | ? /HT1fv -> | ? /typ_fv_subst_elim [ ? /Hs2fv [ ] -> // /HTfv /((@leq_trans _ _ _)^~Hn2) -> ] ] //. rewrite typ_subst_comp (typ_subst_ext (typ_subst s'' \o s2) s') => [ | ? /HTfv /Hs' -> // ]. congruence. } rewrite Hunify. have : forall x, typ_bv (s3 x) =i pred0 => [ ? x | Hs3bv ]. { apply /negbTE /negP => /(typ_bv_unify _ _ _ Hunify) [ /typ_bv_subst_elim [ | [ ? ] ] | /= ]. - by rewrite HT2'bv. - by rewrite Hs2bv. - rewrite !inE orbF. exact /negP /negbT /HT1'bv. } exists n2.+1, (typ_subst (typ_subst s3 \o s2) \o s1), s''', (s3 n2). (repeat split) => [ | | // | x ? | ? ? /typ_fv_subst_elim [ ? /typ_fv_subst_elim [ ? /(typ_fv_unify _ _ _ Hunify) [ -> /Hs2fv [ -> /Hs1fv [ | /((@leq_trans _ _ _)^~Hn2) ] | ] | [ /typ_fv_subst_elim [ ? /Hs2fv [ -> /HTfv /((@leq_trans _ _ _)^~Hn2) | ] ] | /= ] ] ] ] | ? /(typ_fv_unify _ _ _ Hunify) [ -> | [ /typ_fv_subst_elim [ ? /Hs2fv [ -> /HTfv /((@leq_trans _ _ _)^~Hn2) | ] ] | /= ] ] | ? ? /= ]; eauto. + apply /leqW /leq_trans; eauto. + by rewrite -(Hgen (typ_fvar n2)) /= ltnn. + rewrite typ_bv_subst Hs1bv. apply /negbTE /negP => /hasP [ ? ? ]. rewrite /= typ_bv_subst Hs2bv => /hasP [ ? ? ]. by rewrite Hs3bv. + rewrite !inE => /orP [ /HT1fv | /eqP -> ]; eauto. + rewrite !inE => /orP [ /HT1fv | /eqP -> ]; eauto. + rewrite Hs // (typ_subst_ext s' (typ_subst s'' \o s2)) => [ | ? /Hs1fv /= [ -> | /Hs' -> // ] ]. * rewrite -!typ_subst_comp -Hgen. apply /typ_subst_ext => ? /typ_fv_subst_elim [ ? /Hs2fv [ <- /Hs1fv [ -> | /((@leq_trans _ _ _)^~Hn2) -> ] | -> ] // ]. by rewrite ((@leq_trans _ _ _)^~Hn2) // ((@leq_trans _ _ _)^~Hn1). * exact /Hs' /((@leq_trans _ _ _)^~Hn1). - move: (IHt n G s T0) => [ ] // ? [ ? [ ? [ ? [ -> [ ? [ HT0 [ ? [ ? [ ? [ ? ? ] ] ] ] ] ] ] ] ] ]. (repeat eexists) => /=; eauto. by rewrite HT0. - move: (IHt n G s (typ_ref T)) => [ ] // n1' [ s1 [ s' [ T' [ -> [ Hn1 [ HT [ HT'bv [ Hs1bv [ Hs1fv [ HTfv Hs ] ] ] ] ] ] ] ] ] ]. move: (typ_unify_complete T' (typ_ref (typ_fvar n1')) (fun x => if x < n1' then s' x else T)) => [ /= | s2 [ Hunify [ s'' Hgen ] ] ]. { by rewrite ltnn -(typ_subst_ext s') => // ? /HTfv ->. } rewrite Hunify. have : forall x, typ_bv (s2 x) =i pred0 => [ ? x | Hs2bv ]. { apply /negbTE /negP => /(typ_bv_unify _ _ _ Hunify) => /= /orP. by rewrite HT'bv. } exists (n1'.+1), (typ_subst s2 \o s1), s'', (s2 n1'). (repeat split) => [ | | | ? ? | ? ? /typ_fv_subst_elim [ ? /(typ_fv_unify _ _ _ Hunify) /= [ -> /Hs1fv [ -> | ] | [ /HTfv | /eqP -> ] ] ] | ? /(typ_fv_unify _ _ _ Hunify) [ -> | [ /HTfv | /eqP -> ] ] | ? Hlt ]; eauto. + by rewrite -(Hgen (typ_fvar n1')) /= ltnn. + rewrite typ_bv_subst Hs1bv. apply /negbTE /negP => /hasP [ ? ? ]. by rewrite Hs2bv. + rewrite Hs // -Hgen. apply /typ_subst_ext => ? /Hs1fv [ ] -> //. by rewrite (leq_trans Hlt). - move: (IHt1 n G s (typ_ref T0)) => [ ] // n1 [ s1 [ s' [ T0' [ -> [ Hn1 [ HT0 [ HT0'bv [ Hs1bv [ Hs1fv [ HT0'fv Hs ] ] ] ] ] ] ] ] ] ]. move: (IHt2 n1 (env_subst s1 G) s' T0) => [ | | | ] => [ ? /env_fv_subst_elim [ x ? ? ] z | ? /env_fv_subst_elim [ ? /Hs1fv [ -> /HG /((@leq_trans _ _ _)^~Hn1) | ] // ] | | n2 [ s2 [ s'' [ T1' [ -> [ Hn2 [ HT1 [ HT1'bv [ Hs2bv [ Hs2fv [ HT1fv Hs' ] ] ] ] ] ] ] ] ] ] ]. { apply /negbTE /negP => ?. have : z \in typ_bv (typ_subst s' (s1 x)). { apply /typ_bv_subst_intro_sub; eauto. } by rewrite -Hs ?Hclos ?HG. } { by rewrite env_subst_comp -(env_subst_ext s) => // ? /= /HG /Hs. } move: (typ_unify_complete (typ_subst s2 T0') (typ_ref T1') s'') => [ /= | s3 [ Hunify [ s''' Hgen ] ] ]. { by rewrite -HT1 typ_subst_comp -(typ_subst_ext s') -?HT0 => // ? /HT0'fv /Hs'. } rewrite Hunify. exists n2, (typ_subst (typ_subst s3 \o s2) \o s1), s''', typ_unit. (repeat split) => [ | ? ? | ? ? /typ_fv_subst_elim [ ? /typ_fv_subst_elim [ ? /(typ_fv_unify _ _ _ Hunify) [ -> /Hs2fv [ -> /Hs1fv [ -> | /((@leq_trans _ _ _)^~Hn2) ] | ] | /= [ /typ_fv_subst_elim [ ? /Hs2fv [ -> /HT0'fv /((@leq_trans _ _ _)^~Hn2) | ] ] | /HT1fv ] ] ] ] | | ? ? ]; eauto. + apply /leq_trans; eauto. + rewrite typ_bv_subst Hs1bv. apply /negbTE /negP => /hasP [ ? ? ]. rewrite typ_bv_subst Hs2bv => /hasP [ ? ? /(typ_bv_unify _ _ _ Hunify) /= /orP ]. rewrite HT1'bv orbF typ_bv_subst HT0'bv => /hasP [ ? ? ]. by rewrite Hs2bv. + rewrite Hs // (typ_subst_ext s' (typ_subst s'' \o s2)) => [ /= | ? /Hs1fv /= [ -> | /Hs' -> // ] ]. * by rewrite -!typ_subst_comp Hgen. * apply /Hs' /leq_trans; eauto. - rewrite H2. move: (IHt1 n G s (typ_open (typ_fvar \o addn (maximum (env_enum_fv (env_subst s G) (typ_enum_fv T1 L))).+1) T1)) => [ | | | n1' [ s1 [ s' [ T1' [ -> [ Hn1 [ HT [ HT1'bv [ Hs1bv [ Hs1fv [ HTfv Hs ] ] ] ] ] ] ] ] ] ] ] //. { apply /H4 => x. repeat eexists. apply /negP => HinL. have : (maximum (env_enum_fv (env_subst s G) (typ_enum_fv T1 L))).+1 + x \in env_enum_fv (env_subst s G) (typ_enum_fv T1 L) => [ | /maximum_sup ]. { by rewrite env_enum_fv_inE_aux typ_enum_fv_inE_aux HinL !orbT. } by rewrite addSn ltnNge leq_addr. } move: (IHt2 n1' (typ_subst (fun x => if x \in env_fv (env_subst s1 G) then typ_fvar x else typ_bvar x) T1' :: env_subst s1 G) s' T) => /= [ ? /orP [ /typ_fv_subst_elim [ x ] | /env_fv_subst_elim [ x ? ? ] z ] | ? /orP [ /typ_fv_subst_elim [ y ] | /env_fv_subst_elim [ ? /Hs1fv [ -> /HG /((@leq_trans _ _ _)^~Hn1) | ] ] ] // | | n2' [ s2 [ s'' [ T2' [ -> [ Hn2 [ HT2' [ HT2'bv [ Hs2bv [ Hs2fv [ HT2fv Hs' ] ] ] ] ] ] ] ] ] ] ] //. { destruct (x \in env_fv (env_subst s1 G)) eqn:Hfv => //=; rewrite inE => /eqP <- ? z. apply /negbTE /negP => ?. have : z \in typ_bv (typ_subst s' T1'). { apply /typ_bv_subst_intro_sub; eauto. } by rewrite -HT => /typ_bv_open_elim [ ? ]. } { apply /negbTE /negP => ?. have : z \in typ_bv (typ_subst s' (s1 x)). { apply/ typ_bv_subst_intro_sub; eauto. } by rewrite -Hs ?Hclos ?HG. } { move: (y \in env_fv (env_subst s1 G)) => [ /= | // ]. by rewrite inE => /eqP -> /HTfv. } { apply /(typed_weaken_env _ _ _ _ H6) => [ [ ? /(_ (typ_fvar 0)) <- | i ? Hnth ] /= ]. - move: (f_equal (typ_subst (fun x => if x <= maximum (env_enum_fv (env_subst s G) (typ_enum_fv T1 L)) then typ_fvar x else typ_bvar (x - (maximum (env_enum_fv (env_subst s G) (typ_enum_fv T1 L))).+1))) HT). rewrite typ_subst_open_distr => [ | x Hin ? ]. + rewrite typ_subst_fvar_eq => [ | x Hin ]. { rewrite typ_open_bvar_eq => [ -> | ? ? /= ]. - eexists (typ_subst (fun x => if x <= maximum (env_enum_fv (env_subst s G) (typ_enum_fv T1 L)) then typ_fvar x else typ_bvar (x - (maximum (env_enum_fv (env_subst s G) (typ_enum_fv T1 L))).+1)) \o s', _); eauto. rewrite !typ_subst_comp typ_open_subst_distr => [ | ? ]. + rewrite typ_open_bvar_eq => [ | ? ]. { apply /typ_subst_ext => x ? /=. rewrite fun_if /= fun_if /=. destruct (x \in env_fv (env_subst s1 G)) eqn:Henv => //. rewrite typ_open_bvar_eq => [ | y ? ]. - rewrite typ_subst_fvar_eq => [ // | y Hin ]. rewrite maximum_sup // env_enum_fv_inE_aux typ_enum_fv_inE_aux -(env_subst_ext (typ_subst s' \o s1)) => [ | ? /HG /Hs // ]. by rewrite -env_subst_comp (env_fv_subst_intro _ _ x) // orbT. - have : y \in typ_bv (typ_subst s' T1'). { apply /typ_bv_subst_intro_sub; eauto. } by rewrite -HT => /typ_bv_open_elim [ ? ]. } by rewrite HT1'bv. + by rewrite HT1'bv. - by rewrite addSn ltnNge leq_addr /= subSS addKn. } by rewrite maximum_sup // env_enum_fv_inE_aux typ_enum_fv_inE_aux Hin orbT. + by rewrite maximum_sup // env_enum_fv_inE_aux typ_enum_fv_inE_aux Hin orbT. - rewrite env_subst_comp (env_subst_ext (typ_subst s' \o s1) s) => [ | ? /HG /Hs // ]. eexists (_, _). + exact /Hnth. + exact /Logic.eq_sym /typ_open_bvar. } exists n2', (typ_subst s2 \o s1), s'', T2'. (repeat split) => //= [ | ? ? | ? ? /typ_fv_subst_elim [ ? /Hs2fv [ -> /Hs1fv [ | /((@leq_trans _ _ _)^~Hn2) ] | ] ] | ? ? ]; eauto. + exact /(leq_trans Hn1). + rewrite typ_bv_subst Hs1bv. apply /negbTE /negP => /hasP [ ? ]. by rewrite Hs2bv. + rewrite Hs // (typ_subst_ext s' (typ_subst s'' \o s2)) ?typ_subst_comp => /= [ // | ? /Hs1fv [ -> | ] ]; apply /Hs'; exact /((@leq_trans _ _ _)^~Hn1). Qed.
型安全性の証明の修正
型付け規則の定義を工夫すれば，参照を扱えるように型推論器を拡張したとしても，正当性の証明を容易に拡張できることは分かりました． では，型安全性の証明はどうでしょう？こちらは型推論器の正当性ほど拡張が自明ではありません． 何しろ型推論器の時にはサボっていたストア型付けの取り扱いを真面目にやる必要がありますからね．
まず，型安全性を証明する時に重要な性質の一つ，型保存定理というのは
「型が付くようなプログラムを簡約した際，簡約後のプログラムには同じ型が付く」
といったステートメントでした．しかし，参照を扱えるように対象言語を拡張した現在， ストア型付け無くして実行時のプログラムに型を付けることはできません． そのため，Coq で書くなら以下のようにステートメントを拡張する必要があります7．
Lemma preservation : forall H M G, size H = size M -> (forall i, typed M G (nth trm_unit H i) (nth typ_unit M i)) -> forall t H' t', cbv H t H' t' -> forall T, typed M G t T -> exists M', typed M' G t' T /\ (forall x T, (forall d, nth d M x = T) -> forall d, nth d M' x = T) /\ size H' = size M' /\ (forall i, typed M' G (nth trm_unit H' i) (nth typ_unit M' i)).
ノリとしては，簡約前の項だけでなくヒープも型が付く必要があって， ヒープが簡約で変更されたとしても依然として型が付くようなものである，ということでしょうか． ここで注意しなければならないのは，簡約によってヒープに存在する参照セルは増えていくので， 当然それに合わせてストア型付けも単調に増えていく必要があることです8．
Proof. induction 3; inversion 1; subst; eauto. - inversion H7. subst. exists M. repeat split; eauto. apply /(typed_subst_single _ _ _ _ _ _ H11 [::]) => ? Hs. rewrite typ_open_bvar_eq => // ?. by rewrite H10. - move: (IHcbv _ H7) => [ M' [ ? [ ? [ ? ? ] ] ] ]. exists M'. repeat split; eauto. apply /typed_app; eauto. apply /(typed_weaken_store M); eauto. - move: (IHcbv _ H10) => [ M' [ ? [ ? [ ? ? ] ] ] ]. exists M'. repeat split; eauto. apply /typed_app; eauto. apply /(typed_weaken_store M); eauto. - have ? : forall x T, (forall d, nth d M x = T) -> (forall d, nth d (rcons M T0) x = T). { move => x T Hnth d. by move: nth_rcons (leqP (size M) x) (Hnth (if x == size M then T0 else d)) => -> [ /(nth_default _) -> | ]. } exists (rcons M T0). (repeat split; eauto) => [ | | l ]. + apply /typed_loc => /= [ | ? ]. * apply /typed_closed. eauto. * by rewrite nth_rcons H0 ltnn eqxx. + by rewrite !size_rcons H0. + rewrite !nth_rcons -H0. case (ltngtP (size H) l) => ? //; apply /(typed_weaken_store M); eauto. - move: (IHcbv _ H6) => [ ? [ ? [ ? [ ? ? ] ] ] ]. eauto 6. - inversion H6. subst. rewrite -(H2 trm_unit) -(H9 typ_unit). eauto. - move: (IHcbv _ H6) => [ ? [ ? [ ? [ ? ? ] ] ] ]. eauto 6. - inversion H7. subst. exists M. (repeat split; eauto) => [ | l' ]. + rewrite size_set_nth -H0. apply /maxn_idPr. case (leqP (size H) l) => // Hleq. move: (H10 typ_unit). by rewrite -(H10 (typ_fvar 0)) !nth_default -?H0. + rewrite nth_set_nth /=. case (@eqP _ l' l) => [ -> | ]; eauto. by rewrite H10. - move: (IHcbv _ H7) => [ M' [ ? [ ? [ ? ? ] ] ] ]. exists M'. repeat split; eauto. apply /typed_update; eauto. apply /typed_weaken_store; eauto. - move: (IHcbv _ H10) => [ M' [ ? [ ? [ ? ? ] ] ] ]. exists M'. repeat split; eauto. apply /typed_update; eauto. apply /typed_weaken_store; eauto. - exists M. repeat split; eauto. exact /(typed_subst_single _ _ _ _ _ _ H10 L). - by move: (cbv_value _ _ _ _ H2 H6). Qed.
とはいえ，値制限を導入していなかった際には成り立たなかった（= 証明できなかった）性質にしてはいささか単純な証明に見えます． 冒頭で話した型安全性を壊す例
let r = ref (fun x -> x) in r := (fun x -> x + 1); !r ()
で問題になったように，let x = e1 in e2 の e1 で参照セルが作られるようなプログラムは，どの場合分けで考慮されているのでしょうか？
これは実は，簡単化のためにそのような let 式は型が付かなくして，値制限を満たすような let 式だけ型が付くようにしたので，考慮の必要が無くなっています．
過度な単純化のように見えなくもないですが，単相の let は (fun x -> e1) e2 でも代用できるのでまぁ大丈夫でしょう．
次に，型安全性を証明する時に重要なもう一つの性質，進行定理——型チェックを通った式は評価できない式ではない性質——の修正は型保存定理よりも容易です． と言うのも，以下の Coq で書いたステートメントの通り，型が付くという性質は型にしか現れないからです．
Lemma progress H M : size H = size M -> (forall i, typed M [::] (nth trm_unit H i) (nth typ_unit M i)) -> forall t T, typed M [::] t T -> value t \/ exists H' t', cbv H t H' t'.
単純なステートメントから抱く印象に違わず，証明の拡張も型保存定理に比べてかなり楽です．
Proof. move => Hsize Hstore t. induction t; inversion 1; subst; eauto. - move: (H2 typ_unit). by rewrite -(H2 (typ_bvar 0)) !nth_default. - move: (IHt1 _ H4) => [ /((canonical_arrow _ _ _ _)^~H4) [ ? -> ] | [ ? [ ? ? ] ] ]; eauto. move: (IHt2 _ H6) => [ ? | [ ? [ ? ? ] ] ]; eauto. - move: (IHt _ H3) => [ ? | [ ? [ ? ? ] ] ]; eauto. - move: (IHt _ H3) => [ /((canonical_ref _ _ _)^~H3) [ l ? ] | [ ? [ ? ? ] ] ]; subst; eauto. inversion H3. subst. right. repeat eexists. apply /(cbv_deref _ _ (nth trm_unit H l)) => ?. case (leqP (size H) l). + rewrite Hsize => ?. move: (H6 typ_unit). by rewrite -(H6 (typ_fvar 0)) !(@nth_default _ _ M). + exact /set_nth_default. - move: (IHt1 _ H4) => [ /((canonical_ref _ _ _)^~H4) [ l ? ] | [ ? [ ? ? ] ] ]; subst; eauto. inversion H4. subst. move: (IHt2 _ H6) => [ ? | [ ? [ ? ? ] ] ]; eauto. Qed.
まとめ
本記事では，MLのサブセット——型付きλ計算をletと参照で拡張した，let多相をサポートする言語——の型推論器を Coq で実装し，その正当性を証明しました． ここで実装した型推論器とその正当性，型安全性の証明は GitHub に置いてあるので，実際の Coq のコードを動かしてみたい方はそちらを参照してください．
さて，5年前から趣味でコツコツ検証していた型推論器も，思えば立派になったものです． これからはどんな風に型推論器を拡張したものでしょうか？ ぱっとすぐに思い付くのは値制限の部分をランク1多相や緩い値制限といった，より巧妙な制約に置き換えてやることですが…… 僕の定式化は多相型が冠頭標準形であることを前提にしているので，ランク1多相に対応しようとすると殆ど全面的に書き直すはめになります． また，緩い値制限は型推論器の実装と正当性の証明に関しては難しくないのですが，元論文にある型安全性の証明が結構大変そうなので手が伸びません． 結局，この辺で止めておくのが良いということでしょうか．
-
De Bruijn index で束縛を表現している点に注意↩
-
De Bruijn index で束縛を表現しているので，無名関数
fun x -> eの引数を表す変数名xはここで扱う言語の構文には表れない↩ -
無名関数
fun x -> eと同様の理由により，let式let x = e1 in e2のxはここで扱う言語の構文には表れない↩ -
詳しくは TaPL 13章を参照のこと↩
-
定義から fresh な型変数で置き換えても型付けできることは保証されているので，あとはその型変数に好きな型を代入するだけ↩
-
この辺の議論は TaPL 13章に詳しい．実は，この辺りの議論は別に let 多相が入ってなくても参照型を扱う上で欠かせないものだったりする（評価文脈使って小ステップ操作的意味論定義してたら知らんけど）↩
