　この記事は言語実装 Advent Calendar 2017の10日目（！？）のために書かれました． 9日目の記事は@ukitakaさんのSwiftコンパイラで採用されているパターンマッチの網羅性チェックの理論と実装です．

　何やら言語実装Advent Calendar 2017に型推論器の実装をやろうとしている人がちらほら居たので，先にlet多相の型推論の実装と形式的検証をやって威嚇しようと思ったのですが，論文とワークショップで死んでて遅刻してしまいました…お恥ずかしい… まだ単純型付きλ計算にしか対応していませんが，「Done is better than perfect.」ってことでこのまま記事にしてしまいます． let多相に対応できたらまた別のAdvent Calendarに投稿しましょう．

　今回書いたコードはGitHub上で公開しています．https://github.com/fetburner/TypeInfer Coq 8.5.3¹で動作を確認していますが，動かなかったらPRでも投げて下さい．

　型推論の検証ですが，実は僕は2年前にも言語実装 Advent Calendar 2015でやったことがあります．もっともその時は型推論の健全性—型推論のアルゴリズム $\mathrm{typing}(\Gamma,t)$ が正常に終了して型代入 $\sigma$ と型 $\tau$ が帰ってきた場合，項 $\sigma t$ は型環境 $\sigma \Gamma$ の下で $\tau$ 型を持つこと²—しか証明していませんでしたから，リベンジマッチとして完全性—項 $\sigma t$ が型環境 $\sigma \Gamma$ の下で $\tau$ 型を持つような型代入 $\sigma$ が存在する場合，型推論のアルゴリズム $\mathrm{typing}(\Gamma,t)$ は正常に終了して $(\sigma, \tau)$ より一般的な解 $(\sigma', \tau')$ を返すこと—も証明しようと思います．

型についての諸々の定義

　それでは始めにCoq上で単純型付きλ計算の型を定義していきましょう．

Inductive typ : Set :=
  | typ_fvar (x : nat)
  | typ_arrow (T1 T2 : typ).

型変数 $\alpha$ は型で³，関数型 $\tau_1\rightarrow\tau_2$ も型（かつ，それ以外型でない）．簡単ですね．

　型 $\tau$ に対する型代入 $\sigma$ の適用 $\sigma\tau$ はこんな感じ．

Fixpoint typ_subst s T :=
  match T with
  | typ_fvar x => s x
  | typ_arrow T1 T2 => typ_arrow (typ_subst s T1) (typ_subst s T2)
  end.

今回は型代入を，型変数（のシンボル）から型への関数として表現しています．従って，何も置き換えない空な型代入はfun x => typ_fvar x，つまりtyp_fvarで表されます．

Lemma typ_subst_fvar T : typ_subst typ_fvar T = T.

加えて，型代入sとs'の合成はfun x => typ_subst s (s' x)で表されます．

Lemma typ_subst_comp s s' T :
  typ_subst s (typ_subst s' T) = typ_subst (fun x => typ_subst s (s' x)) T.

また，型変数xを型Tに置き換えるだけの型代入typ_subst_single x Tも定義しておきましょう．

Definition typ_subst_single x T := fun y =>
  if eq_nat_dec x y then T else typ_fvar y.

　型推論の検証では型変数がfreshかどうかを延々と議論していく訳ですから，型 $\tau$ に含まれる型変数の集合 $\mathrm{FTV}(\tau)$ を定義します．

Fixpoint typ_fv T :=
  match T with
  | typ_fvar x => Singleton _ x
  | typ_arrow T1 T2 => Union _ (typ_fv T1) (typ_fv T2)
  end.

単一化で必要になるoccurs check—型 $\tau$ の中に型変数 $\alpha$ が現れるかの判定—はこう書けます．

Definition typ_fv_dec x T : { In _ (typ_fv T) x } + { ~ In _ (typ_fv T) x }.
Proof.
  Local Hint Resolve In_Empty_dec In_Union_dec.
  induction T as [ y | ]; simpl; eauto.
  destruct (eq_nat_dec x y).
  - eauto with sets.
  - right. inversion 1. eauto with sets.
Defined.

タクティックでプログラムを書いているので少し分かりづらいですが，型変数からなる型 $\beta$ に型変数 $\alpha$ が現れるか調べる際は， $\alpha$ と $\beta$ が等しいか調べて，型 $\tau_1\rightarrow\tau_2$ に型変数 $\alpha$ が現れるか調べる際は，まず型 $\tau_1$ に現れるか調べて，含まれていなければ型 $\tau_2$ に現れるか調べて…と自然な定義になっています．

　以上を踏まえて，制約 $C$ を解く単一化のアルゴリズム $\mathrm{unify}(C)$ を実装するならば以下のような感じでしょうか．

Function unify C { wf constr_lt C } :=
  match C with
  | nil => Some typ_fvar
  | (T1, T2) :: C =>
      if typ_eq_dec T1 T2 then unify C
      else
        match T1, T2 with
        | typ_fvar x, _ =>
            if typ_fv_dec x T2 then None
            else option_map (fun s z => typ_subst s (typ_subst_single x T2 z)) (unify (constr_subst (typ_subst_single x T2) C))
        | _, typ_fvar y =>
            if typ_fv_dec y T1 then None
            else option_map (fun s z => typ_subst s (typ_subst_single y T1 z)) (unify (constr_subst (typ_subst_single y T1) C))
        | typ_arrow T11 T12, typ_arrow T21 T22 => unify ((T11, T21) :: (T12, T22) :: C)
        end
  end.

制約 $C=\left\{\tau_{11}=\tau_{21},\cdots,\tau_{1n}=\tau_{2n}\right\}$ はリスト[(T11, T21); ... ; (T1n, T2n)]で表現しています． typ_eq_dec T1 T2は型T1とT2が等しいかの判定ですね．この単一化の実装は正直愚直ってレベルではない⁴のですが，今回検証する型推論のアルゴリズムではそこまで複雑な入力を与えられないと思うので，そのままにしておきます．

この単一化の手続きは健全— $\mathrm{unify}(C)$ が正常に停止して代入 $\sigma$ を返した場合， $\sigma$ は制約 $C$ の解になっている—かつ完全—制約 $C$ に解 $\sigma$ が存在する場合， $\mathrm{unify}(C)$ は正常に停止して $\sigma$ より一般的な代入 $\sigma'$ を返す—ですが，それらの証明の大筋は2年前と同様なので省略します．

項についての諸々の定義

　次に，Coq上で単純型付きλ計算の項を定義していきましょう．

Inductive trm : Set :=
  | trm_var (n : nat)
  | trm_abs (T : typ) (t : trm)
  | trm_app (t1 t2 : trm).

変数 $x$ があり，λ抽象 $\lambda \_:\tau. t$ があり，関数適用 $t_1~t_2$ がある．自然ですね．ここで，変数束縛をde Bruijn indicesで表現している⁵ことと，関数引数に型注釈が付いていることに注意して下さい．型注釈があるのに型推論の手続きを考えるのか？と思われるかもしれませんが，型注釈のところをfreshな型変数で補えば型注釈の無い項についての型推論の手続きも実装できます．

　項に関連する定義で注意すべきはそれぐらいで，その他の定義は自明です．項 $t$ に対する型代入 $\sigma$ の適用 $\sigma t$ の定義は以下の通りになり，

Fixpoint trm_subst_typ s t :=
  match t with
  | trm_var x => trm_var x
  | trm_abs T t => trm_abs (typ_subst s T) (trm_subst_typ s t)
  | trm_app t1 t2 => trm_app (trm_subst_typ s t1) (trm_subst_typ s t2)
  end.

項 $t$ に現れる型変数の集合 $\mathrm{FTV}(t)$ の定義は以下の通りになります．

Fixpoint trm_ftv t :=
  match t with
  | trm_var _ => Empty_set _
  | trm_abs T t => Union _ (typ_fv T) (trm_ftv t)
  | trm_app t1 t2 => Union _ (trm_ftv t1) (trm_ftv t2)
  end.

型判断についての諸々の定義

　続いて，単純型付きλ計算の型判断 $\Gamma\vdash t : \tau$ に必要な定義を準備していきましょう．変数束縛をde Bruijn indicesで表現したので，型環境は型の有限列，つまり型のリストで十分です．

Definition env := list typ.

型環境 $\Gamma$ に含まれる型変数の集合 $\mathrm{FTV}(\Gamma)$ はfold_rightで記述でき，

Definition env_ftv (G : env) :=
  fold_right (fun T s => Union _ (typ_fv T) s) (Empty_set _) G.

型環境 $\Gamma$ に対する型代入 $\sigma$ の適用 $\sigma\Gamma$ はmapで記述できます．

Definition env_subst_typ s G := map (typ_subst s) G.

　この型環境の定義を用いると，型判断 $\Gamma\vdash t : \tau$ は以下のように定義できます．

Inductive typed : env -> trm -> typ -> Prop :=
  | typed_var G x T :
      nth_error G x = Some T ->
      typed G (trm_var x) T
  | typed_abs G t T1 T2 :
      typed (T1 :: G) t T2 ->
      typed G (trm_abs T1 t) (typ_arrow T1 T2)
  | typed_app G t1 t2 T1 T2 :
      typed G t1 (typ_arrow T1 T2) ->
      typed G t2 T1 ->
      typed G (trm_app t1 t2) T2.

ここで，型推論の健全性を証明する上で重要となる型代入補題を紹介しておきます．これは $\Gamma\vdash t : \tau$ が成り立つ場合， $\sigma\Gamma\vdash \sigma t : \sigma\tau$ も成り立つという補題で， Coqでは以下のように記述できます．

Lemma typed_subst_typ s G t T :
  typed G t T ->
  typed (env_subst_typ s G) (trm_subst_typ s t) (typ_subst s T).

型推論の実装

　まず，型推論の実装について考えてみましょう．一般的な教科書⁶では型推論を解説する際，型についての方程式を立て，それを解くのだといった喩えが良く用いられています．説明のためにfreshな型変数の生成（gensym）をlet x := fresh in ...と書くことにすると，方程式（制約）を抽出する（と共に単一化前の型を返す）アルゴリズム $\mathrm{extract}(\Gamma, t)$ は以下のような疑似コードで表現できます．

Fixpoint extract G t :=
  match t with
  | trm_var x => option_map (pair nil) (nth_error G x)
  | trm_abs T1 t =>
      match extract (T1 :: G) t with
      | None => None
      | Some (C, T2) => Some (C, typ_arrow T1 T2)
      end
  | trm_app t1 t2 =>
      match extract G t1 with
      | None => None
      | Some (C1, T1) =>
          match extract G t2 with
          | None => None
          | Some (C2, T2) =>
              let x := fresh in
              Some ((T1, typ_arrow T2 (typ_fvar x)) :: C1 ++ C2, typ_fvar x)
          end
      end
  end.

方程式（制約）を解く手続きは，上で解説した単一化のアルゴリズムが該当します．僕が2年前に検証したのも，この制約の抽出と単一化による実装ですね．

　ところがこの二段構えのアプローチは，let多相に拡張する際に問題があります⁷．と言うのも，let多相では項 $\mathrm{let}~x=t_1~\mathrm{in}~t_2$ を型環境 $\Gamma$ の下で型付けする際 $t_1$ の型 $\tau_1$ は $\Gamma$ に含まれない型変数で量化しても良い訳ですが， $\mathrm{extract}(\Gamma, t_1)$ の再帰呼び出しをしただけでは $t_1$ の型 $\tau_1$ が確定しないため，どの型変数を量化して良いか分からないのです．

　そこで，いちいちプログラム全体に型を付けるための制約ができるのを待ってから単一化をするのではなく，必要になった制約をその場で単一化する（つまり，局所的な解を確定させる）ようなアルゴリズムを考えましょう．こうすれば $t_1$ を型付けして $\tau_1$ が得られた時点で，どの型変数が $\Gamma$ に含まれないのか分かりますね．疑似コードにすると以下の通りでしょうか．

Fixpoint typing G t :=
  match t with
  | trm_var x =>
      option_map (fun T => (typ_fvar, T)) (nth_error G x)
  | trm_abs T1 t =>
      match typing (T1 :: G) t with
      | None => None
      | Some (s1, T2) =>
          Some (s1, typ_arrow (typ_subst s1 T1) T2)
      end
  | trm_app t1 t2 =>
      match typing G t1 with
      | None => None
      | Some (s1, T1) =>
          match typing (env_subst_typ s1 G) (trm_subst_typ t2) with
          | None => None
          | Some (s2, T2) =>
              let x := fresh in
              option_map
                (fun s3 => (fun x => typ_subst (fun x => typ_subst s3 (s2 x)) (s1 x), s3 x))
                (unify [ (typ_subst s2 T1, typ_arrow T2 (typ_fvar x)) ])
          end
      end
  end.

実際の型推論器⁸も，（参照を用いているために型代入の適用が隠れているものの）このように制約が必要になった段階で単一化を行う実装になっています．もっとも，この疑似コードは構造的再帰になっていないため，（gensymを何とかしたとしても）Coqの停止性チェッカに怒られてしまうことでしょう．仕方ないので引数を増やして代入を遅延します．

Fixpoint typing s G t :=
  match t with
  | trm_var x =>
      option_map (fun T => (typ_fvar, typ_subst s T)) (nth_error G x)
  | trm_abs T1 t =>
      match typing s (T1 :: G) t with
      | None => None
      | Some (s1, T2) =>
          Some (s1, typ_arrow (typ_subst (fun x => typ_subst s1 (s x)) T1) T2)
      end
  | trm_app t1 t2 =>
      match typing s G t1 with
      | None => None
      | Some (s1, T1) =>
          match typing (fun x => typ_subst s1 (s x)) G t2 with
          | None => None
          | Some (s2, T2) =>
              let x := fresh in
              option_map
                (fun s3 => (fun x => typ_subst (fun x => typ_subst s3 (s2 x)) (s1 x), s3 x))
                (unify [ (typ_subst s2 T1, typ_arrow T2 (typ_fvar x)) ])
          end
      end
  end.

この $\mathrm{typing}(\sigma,\Gamma,t)$ は $\sigma\Gamma$ の下での $\sigma t$ の型を推論するアルゴリズムです．

　そういえば，説明のためにgensymに相当する部分を疑似コードでごまかしていたままでした．と言っても疑似コードでごまかしていた部分を正しいCoqの式に直すのは難しい変更ではなくて，gensymの実装が持っている状態を再帰で引き廻すだけです．

Fixpoint typing n s G t :=
  match t with
  | trm_var x =>
      option_map (fun T => (n, typ_fvar, typ_subst s T)) (nth_error G x)
  | trm_abs T1 t =>
      match typing n s (T1 :: G) t with
      | None => None
      | Some (n, s1, T2) =>
          Some (n, s1, typ_arrow (typ_subst (fun x => typ_subst s1 (s x)) T1) T2)
      end
  | trm_app t1 t2 =>
      match typing n s G t1 with
      | None => None
      | Some (n1, s1, T1) =>
          match typing n1 (fun x => typ_subst s1 (s x)) G t2 with
          | None => None
          | Some (n2, s2, T2) =>
              option_map
                (fun s3 => (S n2, fun x => typ_subst (fun x => typ_subst s3 (s2 x)) (s1 x), s3 n2))
                (unify [ (typ_subst s2 T1, typ_arrow T2 (typ_fvar n2)) ])
          end
      end
  end.

この $\mathrm{typing}(n,\sigma,\Gamma,t)$ は $n$ をgensymの持っている状態として $\sigma\Gamma$ の下での $\sigma t$ の型を推論し，変更されたgensymの状態と共に結果を返すアルゴリズムです．今回はこの型推論の実装を採用し，検証を行います．

型推論の検証

　それでは準備も済んだことですし，型推論の正当性を検証していきましょう．始めに型推論の健全性— $\mathrm{typing}(n,\sigma,\Gamma,t)$ が正常に終了して型代入 $\sigma'$ と型 $\tau$ が帰ってきた場合，項 $\sigma'\sigma t$ は型環境 $\sigma'\sigma \Gamma$ の下で $\tau$ 型を持つこと—から証明します．Coqでstatementを書くと以下の通りです．

Theorem typing_sound t : forall G m n s s' T,
  typing m s G t = Some (n, s', T) ->
  typed (env_subst_typ s' (env_subst_typ s G)) (trm_subst_typ s' (trm_subst_typ s t)) T.

このメタ定理は型代入補題を使えば，項 $t$ についての構造帰納法で簡単に示せます．

Proof.
  induction t as [ x | T1 t | t1 IHt1 t2 IHt2 ]; simpl; intros G m ? s s' T Htyping.
  - destruct (nth_error G x) eqn:?; inversion Htyping; subst.
    rewrite env_subst_typ_fvar. unfold env_subst_typ. eapply map_nth_error in Heqo. eauto.
  - destruct (typing m s (T1 :: G) t) as [ [ [ ] T2 ] | ] eqn:Heqo; inversion Htyping; subst.
    specialize (IHt _ _ _ _ _ _ Heqo). rewrite <- typ_subst_comp. eauto.
  - destruct (typing m s G t1) as [ [ [ n1 s1 ] T1 ] | ] eqn:Heqo1; inversion Htyping.
    specialize (IHt1 _ _ _ _ _ _ Heqo1).
    destruct (typing n1 (fun x => typ_subst s1 (s x)) G t2) as [ [ [ n2 s2 ] T2 ] | ] eqn:Heqo2; inversion Htyping.
    specialize (IHt2 _ _ _ _ _ _ Heqo2).
    destruct (unify [(typ_subst s2 T1, typ_arrow T2 (typ_fvar n2))]) as [ s3 | ] eqn:Heqo3; inversion Htyping.
    apply unify_sound in Heqo3. inversion Heqo3. subst. simpl in *.
    repeat (rewrite <- env_subst_typ_comp in * || rewrite <- trm_subst_typ_comp in *).
    apply typed_subst_typ with (s := s2) in IHt1. apply typed_subst_typ with (s := s3) in IHt1. rewrite H6 in *. eauto.
Qed.

　示すのが大変なのは型推論の完全性—項 $\sigma'\sigma t$ が型環境 $\sigma'\sigma \Gamma$ の下で $\tau$ 型を持つような型代入 $\sigma'$ が存在し，状態 $m$ の下でgensymが $\sigma \Gamma$ や $\sigma t$ に含まれる型変数を返さない場合，型推論のアルゴリズム $\mathrm{typing}(m,\sigma,\Gamma,t)$ は正常に終了して， $(\sigma', \tau)$ より一般的な解 $(\sigma'', \tau')$ と $\sigma''$ と $\tau'$ に含まれる型変数をgensymが返さないような状態 $n$ を返すこと—です．Coqでstatementを書くならば以下の通りでしょうか．

Theorem typing_complete t : forall G m s s' T,
  typed (env_subst_typ s' (env_subst_typ s G)) (trm_subst_typ s' (trm_subst_typ s t)) T ->
  (forall n, In _ (env_ftv (env_subst_typ s G)) n -> n < m) ->
  (forall n, In _ (trm_ftv (trm_subst_typ s t)) n -> n < m) ->
  exists n s'' s''' T', typing m s G t = Some (n, s'', T')
    /\ m <= n /\ T = typ_subst s''' T'
    /\ (forall x m, In _ (typ_fv (s'' x)) m -> x = m \/ m < n)
    /\ (forall m, In _ (typ_fv T') m -> m < n)
    /\ forall n, n < m -> s' n = typ_subst s''' (s'' n).

何かもうstatementからしてグロいんですが，至る所でgensymの返す型変数がfreshであることを示す必要があるので，証明も大変グロいです．

  Local Hint Resolve Nat.lt_le_trans le_trans le_S.
  induction t as [ x | T1 t | t1 IHt1 t2 IHt2 ]; intros G m s s' T; inversion 1; intros Henv Htrm; subst; simpl in *.
  - unfold env_subst_typ in *.
    destruct (nth_error G x) as [ T' | ] eqn:Hnth.
    + apply map_nth_error with (f := typ_subst s) in Hnth.
      exists m, typ_fvar, s', (typ_subst s T'). repeat split; eauto.
      * apply map_nth_error with (f := typ_subst s') in Hnth.
        congruence.
      * inversion 1; eauto.
      * intros ? HIn. apply nth_error_In in Hnth.
        apply Henv. eapply env_ftv_intro; eauto.
    + apply nth_error_None in Hnth.
      assert (Hnth' : nth_error (map (typ_subst s') (map (typ_subst s) G)) x <> None) by congruence.
      apply nth_error_Some in Hnth'. repeat rewrite map_length in *. omega.
  - destruct (IHt (_ :: _) m _ _ _ H4) as [ n [ s'' [ s''' [ T2' [ Htyping [ ? [ HT [ Hsfv [ ? Hs ] ] ] ] ] ] ] ] ]; eauto with sets.
    { inversion 1; eauto with sets. }
    rewrite Htyping. exists n, s'', s''', (typ_arrow (typ_subst s'' (typ_subst s T1)) T2'). rewrite <- typ_subst_comp. simpl. repeat split; eauto.
    + rewrite HT. f_equal. rewrite typ_subst_comp with (s := s''). apply typ_subst_ext. eauto with sets.
    + inversion 1; subst; eauto.
      destruct (typ_fv_subst _ _ _ H3) as [ ? [ ] ].
      edestruct Hsfv; eauto; subst; eauto with sets.
  - destruct (IHt1 _ m _ _ _ H3) as [ n1 [ s1 [ s1' [ T1' [ Htyping1 [ ? [ HT1 [ Hsfv1 [ ? Hs1 ] ] ] ] ] ] ] ] ]; eauto with sets. rewrite Htyping1.
    repeat rewrite env_subst_typ_ext with (s := s') (s' := fun x => typ_subst s1' (s1 x)) in * by eauto with sets.
    repeat rewrite <- env_subst_typ_comp in *.
    rewrite env_subst_typ_comp with (s := s1) in H5.
    repeat rewrite trm_subst_typ_ext with (s := s') (s' := fun x => typ_subst s1' (s1 x)) in * by eauto with sets.
    repeat rewrite <- trm_subst_typ_comp in *.
    rewrite trm_subst_typ_comp with (s := s1) in H5.
    destruct (IHt2 _ n1 _ _ _ H5) as [ n2 [ s2 [ s2' [ T2' [ Htyping2 [ ? [ HT2 [ Hsfv2 [ ? Hs2 ] ] ] ] ] ] ] ] ]; eauto with sets.
    { intros ? HIn. rewrite <- env_subst_typ_comp in HIn. destruct (env_ftv_subst _ _ _ HIn) as [ ? [ HIn' ] ]. destruct (Hsfv1 _ _ HIn'); subst; eauto with sets. }
    { intros ? HIn. rewrite <- trm_subst_typ_comp in HIn. destruct (trm_ftv_subst _ _ _ HIn) as [ ? [ HIn' ] ]. destruct (Hsfv1 _ _ HIn'); subst; eauto with sets. }
    rewrite Htyping2. repeat rewrite <- env_subst_typ_comp in *. repeat rewrite <- trm_subst_typ_comp in *. subst.
    rewrite typ_subst_ext with (s := s1') (s' := fun x => typ_subst s2' (s2 x)) in * by eauto with sets. repeat rewrite <- typ_subst_comp in *.
    destruct unify_complete with
      (C := [(typ_subst s2 T1', typ_arrow T2' (typ_fvar n2))])
      (s := fun x => if lt_dec x n2 then s2' x else T) as [ s3 [ Hunify [ s3' Hmg ] ] ].
    { constructor; eauto. simpl. destruct (lt_dec n2 n2); try omega. repeat rewrite <- typ_subst_comp.
      repeat rewrite typ_subst_ext with (s := fun x => if lt_dec x n2 then s2' x else T) (s' := s2'); eauto.
      - intros x HIn. destruct (lt_dec x n2); eauto. specialize (H4 _ HIn). omega.
      - intros x HIn. destruct (lt_dec x n2); eauto. destruct (typ_fv_subst _ _ _ HIn) as [ ? [ HIns2 HInT1 ] ].
        destruct (Hsfv2 _ _ HIns2); subst; try omega. specialize (H1 _ HInT1). omega. }
    rewrite Hunify. specialize (unifier_dom _ _ Hunify). intros Hsfv3. exists (S n2), (fun x => typ_subst (fun x => typ_subst s3 (s2 x)) (s1 x)), s3', (s3 n2). simpl in *. repeat split; eauto 3.
    + specialize (Hmg n2). destruct (lt_dec n2 n2); eauto; omega.
    + intros.
      repeat match goal with
      | H : In _ (typ_fv (typ_subst _ _)) _ |- _ => destruct (typ_fv_subst _ _ _ H) as [? [ ] ]; clear H
      end.
      edestruct Hsfv3; eauto.
      * subst. edestruct Hsfv2; eauto. subst. edestruct Hsfv1; eauto.
      * repeat match goal with
        | H : In _ (Union _ _ _) _ |- _ => inversion H; clear H
        | H : In _ (Singleton _ _) _ |- _ => inversion H; clear H
        | H : In _ (Empty_set _) _ |- _ => inversion H
        end; subst; eauto.
        destruct (typ_fv_subst _ _ _ H10) as [ ? [ ] ].
        edestruct Hsfv2; eauto. subst. eauto.
    + intros ? HIn. destruct (Hsfv3 _ _ HIn); subst; eauto.
      repeat match goal with
      | H : In _ (Union _ _ _) _ |- _ => inversion H; clear H
      | H : In _ (Singleton _ _) _ |- _ => inversion H; clear H
      | H : In _ (Empty_set _) _ |- _ => inversion H
      end; subst; eauto.
      destruct (typ_fv_subst _ _ _ H7) as [ ? [ ] ].
      edestruct Hsfv2; eauto. subst. eauto.
    + intros ? ?. rewrite Hs1 by eauto.
      rewrite typ_subst_ext with (s := s1') (s' := fun x => typ_subst s2' (s2 x))
        by (intros ? HIn; destruct (Hsfv1 _ _ HIn); subst; eauto with sets). rewrite <- typ_subst_comp.
      rewrite typ_subst_ext with (s := s2') (s' := fun x => typ_subst s3' (s3 x))
        by (intros x HIn; rewrite <- Hmg; destruct (lt_dec x n2); eauto; exfalso; destruct (typ_fv_subst _ _ _ HIn) as [ ? [ ] ];
            edestruct Hsfv2; eauto; subst; edestruct Hsfv1; eauto; subst; omega).
      repeat rewrite <- typ_subst_comp. eauto.
Qed.

　これら健全性と完全性の系として，型環境 $\Gamma$ と項 $t$ が与えられたとき，型付けできるならば主要型⁹とそのwitnessを返し，型付けできないならばそのwitnessを返す関数を書けます．

Definition typing' G t :
  { s : _ & { T | typed (env_subst_typ s G) (trm_subst_typ s t) T /\
    forall s' T', typed (env_subst_typ s' G) (trm_subst_typ s' t) T' ->
      exists s'', typ_subst s'' T = T'
        /\ forall x, In _ (Union _ (env_ftv G) (trm_ftv t)) x -> s' x = typ_subst s'' (s x) } } +
  { forall s T, typed (env_subst_typ s G) (trm_subst_typ s t) T -> False }.

まとめ

　単純型付きλ計算を対象とした効率的な型推論のアルゴリズムを実装し，Coqで健全性と完全性を検証しました．

　let多相に対応するのが今後の目標ですが，その際型スキームを扱う必要があり，どうしても型変数の束縛について考えなくてはなりません．僕はCoq上で束縛を扱う時はいつもde Bruijn indicesを使ってきたのですが，型推論のアルゴリズムを実装する都合上自由変数を名前で扱いたいので，両者の折衷案であるlocally nameless representationを使うことになると考えられます．

　その前に型推論の完全性の証明を簡単にできないか試すのも良いかもしれません．現状ではgensymの返す値がfreshであるかどうかの証明に殆どの行数が割かれているため，上手い定式化でこれを解決したいところです．例えば今回の対象言語の型はtyp型を持ちますが，これに自然数のパラメータnを追加し，typ nと書くとn以下の型変数しか持たない型を表すようにすると良さそうです．

古くないか？↩
型推論によって型変数の中身が確定したら，中身を代入してやる必要があるので $\sigma$ が必要になります．型変数を参照として扱うと，この代入が暗黙のうちに行われるので必要性が分かりづらいかもしれませんが…↩
ここでの型変数とは自由な型変数です．let多相に対応する場合，ここに束縛された型変数を表すtyp_bvarなるコンストラクタが増えることでしょう… 型変数のシンボルを自然数で表すのはde Bruijn indexと紛らわしいですが，参照を使わずにgensymを書く都合上（Gallinaに参照は無いので）こうなっています．↩
型代入 $[\alpha\mapsto \tau$ ]が得られた瞬間に，その場で残りの制約 $C$ への代入を行っています．おまけに経路圧縮も行っていません．↩
型変数の束縛はlocally nameless representationで扱うつもりなのに変数束縛はde Bruijn indicesで扱うのか！？と思うかもしれませんが，これは単に僕がde Bruijn indices好きだからです．型変数の束縛をlocally nameless representationで扱おうと考えているのは，型推論の都合上そちらの方が向いている（自由な型変数は名前として扱いたい）と考えたからにすぎません．↩
TaPLとかプログラミング言語の基礎概念とか↩
まぁまだ拡張してないんですけどね．↩
OCamlとかMinCamlとか↩
~~プリンセス~~プリンシパル・タイプ↩