fetburner.core

コアダンプ

let多相を扱える型推論器をCoqで検証する

Coq OCaml SML

以前から僕は単相の型推論アルゴリズムの健全性や完全性をCoqで検証していたのですが，最近*1let多相をサポートするように型推論器の実装と正当性の証明を修正したので記事にしておきましょう*2．

単相型と多相型

以前Coqで検証した型推論アルゴリズムは単相，つまり多相型の扱えないものでした．説明のためにOCamlのREPLのようなものがあると仮定すると，以前の型推論器はこのような動作をすることでしょう．

# let s x y z = (x z) (y z);; (* Sコンビネータ *)
val s : ('_a -> '_b -> '_c) -> ('_a -> '_b) -> '_a -> '_c = <fun>
# let k x y = x;; (* Kコンビネータ *)
val k : '_d -> '_e -> '_d = <fun>
# s k;;
- : ('_a -> '_b) -> '_a -> '_a = <fun>
# k;;
- : '_a -> '_b -> '_a = <fun> (* '_dや'_eといった型変数は単相的な，ある特定の型しか表さないものなので，単一化によって'_aと'_bに固定されてしまう *)
# s k k;; (* let多相があればこの型チェックは通るはず *)
Error (* '_a -> '_b -> '_a型と'_a -> '_b型の単一化に失敗する *)
 (* Kコンビネータの実装を複製すれば，SKKの型チェックが通る *)
# let k' x y = x;;
val k' : '_f -> '_g -> '_f = <fun>
# s k k'
- : '_a -> '_a

とまぁこんな感じで，本来色んな型に対して使えるはずの関数も単相的な型しか推論できないので，型チェックを通すために実装を複製する必要があって残念な感じです．C言語とかで似たような経験をして静的型付きの言語に偏見を持ってしまった人も居るかもしれませんね．

今回検証する型推論器はMLと同様に多相型を扱えるので，次のような動作をします．

# let s x y z = (x z) (y z);; (* Sコンビネータ *)
val s : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c = <fun>
# let k x y = x;; (* Kコンビネータ *)
val k : 'a -> 'b -> 'a = <fun>
# s k;;
- : ('a -> 'b) -> 'a -> 'a = <fun>
# k;;
- : 'a -> 'b -> 'a = <fun> (* 'aや'bといった型変数はパラメーター化された多相的なものなので，単一化でkの型が変わることはない *)
# s k k;;
- :  'a -> 'a = <fun> (* kの型'a -> 'b -> 'aに出現する'aや'bといった型変数はパラメーター化されているので，kの出現ごとに別の型を取ることができる *)

型推論器の都合で実装を複製する必要も無くなって良い感じですね．大学の講義とかで初めに教える静的型付き言語がC言語とかじゃなくてMLだったなら，今より静的型付き言語を好む人が増えることでしょう．

let多相

多相型があると型の付いて欲しいプログラムに型が付いて嬉しいのですが，割と好き放題に多相型を導入できる体系*3System Fなんかは型推論はおろか型チェックをするアルゴリズムすら存在しない，すなわち決定不能であることが知られています．プログラムを扱うプログラムの宿命ですね．込み入ったことをしようとするとすぐ決定不能になってしまう…

型推論の決定可能性を維持したまま多相型を扱う試みはいくつかあって，中でもよく知られているのがlet多相です．ML多相とも言われるように，MLで採用されているあれですね．

let多相ではletで束縛する変数にしか多相型を付けないように制限します．上のSKKの例は

let s x y z = (x z) (y z) in let k x y = x in s k k

みたいなものなので型チェックに通った一方，

(fun f -> (f 0, f true)) (fun x -> x)

みたいな式は型エラーになります． こんな制限があっても込み入ったことをしなければそんなに困らないのは，MLユーザーなら実感していることかと．

参照とか配列みたいに破壊的代入のできる言語機能とlet多相は相性が悪くて，実際のMLではletで変数を束縛する項が値の時しか多相型を付けない*4，とか色々制限をしているのですが，今回Coqで検証する型推論器はλ計算に毛の生えたような言語しか扱わないので考えません．

型推論器の拡張と，その正当性の証明の修正

let多相についての解説も済んだことですし，どのように型推論器の実装を拡張したのか，また正当性の証明を修正したのかについて述べていきましょう．

型の定義の変更

まず型の定義の変更点ですが，単相型しか扱っていなかった頃には

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

と定義されていたのを，

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

に変更します．単に多相的な型変数（以下，型パラメーター）typ_bvar nを単相的な型変数（以下，型変数）typ_fvar xから区別するようになっただけですね．ちなみにtyp_arrow T1 T2がT1を受け取ってT2を返す関数の型です．

ここで，let多相において関数引数を多相型にすることは認められていない*5ため，let多相の扱う多相型は全て，Coq風に書くならforall a b, a -> b -> aみたいな形の冠頭標準形*6になっていることに注意してください．型についての量化子は先頭にしか来ないので，型についての構文では明示的に扱わず，型の中に型パラメーターtyp_bvar nが出現しているとああ省略されてるけど先頭にforall n,付いてるのねって感じで扱います．

型付け規則の変更

次に型付け規則の定義を，

Inductive typed : env -> trm -> typ -> Prop :=
  | typed_var G x s T :
      (forall d, nth d G x = T) ->
      typed G (trm_var x) T
  | typed_abs G t T1 T2 :
      typed (T1 :: G) t T2 ->
      typed G (trm_abs 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
  | typed_let G t1 t2 T1 T2 :
      typed G t1 T1 ->
      typed (T1 :: G) t2 T2 ->
      typed G (trm_let t1 t2) T2.

から

Inductive typed : env -> trm -> typ -> Prop :=
  | typed_var G x s T :
      (forall d, nth d G x = T) ->
      (forall x, typ_bv (s x) = [::]) ->
      typed G (trm_var x) (typ_open s T)
  | typed_abs G t T1 T2 :
      typ_bv T1 = [::] ->
      typed (T1 :: G) t T2 ->
      typed G (trm_abs 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
  | typed_let (L : seq nat) G t1 t2 T1 T2 :
      (forall s, (forall x, exists 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.

に変更します．各規則を順番に見ていきましょう．

まず変数trm_var xの型付け規則typed_varですが，一般的な定義と同様，この規則でtrm_var xの型Tに出現する型パラメーターを全て具体化するようにしています．ちなみにtyp_bvが型に出現する型パラメーターのリストを返す関数で，typ_openが型パラメーターを具体化する関数です．

λ抽象trm_abs tの型付け規則typed_absについては，関数引数は多相型になれない制約が増えてるだけですね．変数束縛はde Bruijn indexで表現しているので注意してください．関数適用trm_app t1 t2の型付け規則typed_appについては変更なしです．

let式trm_let t1 t2の型付け規則typed_let，これが一番大きく変更されています．説明した通りletで束縛する変数は多相型を取っても良くて，一般的な定義だと
「letで変数を束縛する項t1に単相の型T1が付くのなら，型環境Gの下で一般化できる範囲でT1を一般化した多相型を，束縛される変数に付けて良い」
といった規則が採用されています．

型推論器の検証をするだけならその定義でも別に困らないのですが，型安全性を示す際に少々厄介です．ここでは，
「多相的な型T1の型パラメーターをfreshな名前の型変数で具体化して得られる，どのような型もletで変数を束縛する項t1が取りうるのなら，letで束縛される変数に多相的な型T1を付けても良い」
といった宣言的な定義を採用しています*7．ここでのfreshじゃない型変数のリストがLですね*8．気持ちとしてはfreshな名前の型変数どころかどんな型に具体化しても型が付いて欲しいところですが，それはそれで帰納法を回すのが大変になってしまいます…

型推論器の拡張

仕様にあたる型付け規則を多相型も扱うように拡張したので，実装に相当する型推論器もそれに対応するように修正していきましょう．

以前の型推論器の実装は

Fixpoint typing n G t :=
  match t with
  | trm_var x => nth None (map Some G) x
  | trm_abs t =>
      match typing n.+1 (typ_fvar n :: G) t with
      | None => None
      | Some (m, s, T2) => Some (m, s, typ_arrow (s n) T2)
      end
  | 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) =>
              option_map
                (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_let t1 t2 =>
      match typing n G t1 with
      | None => None
      | Some (n1, s1, T1) =>
          match typing n1 (T1 :: env_subst s1 G) t2 with
          | None => None
          | Some (n2, s2, T2) => Some (n2, typ_subst s2 \o s1, T2)
          end
      end
  end.

のようなものでした．このtyping n G tという関数は，n以上の型変数が全てfreshだと仮定して型環境Gの下で項tの型推論を行い，型推論が成功すれば，tの型とどのように型変数を具体化したかを表す型代入，およびいくつ以上の型変数が依然としてfreshなのかを返します．Coqは変数への破壊的代入を許さないので，いわゆるgensymの持つ状態nを引き回していることに注意してください．

これを，次のように変更します．

Fixpoint typing n G t :=
  match t with
  | trm_var x =>
      match nth None (map Some G) x with
      | None => None
      | Some T => Some ((n + maximum (typ_bv T)).+1, typ_fvar, typ_open (typ_fvar \o addn n) T)
      end
  | trm_abs t =>
      match typing n.+1 (typ_fvar n :: G) t with
      | None => None
      | Some (m, s, T2) => Some (m, s, typ_arrow (s n) T2)
      end
  | 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) =>
              option_map
                (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_let t1 t2 =>
      match typing n G t1 with
      | None => None
      | Some (n1, s1, T1) =>
          match typing 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) t2 with
          | None => None
          | Some (n2, s2, T2) => Some (n2, typ_subst s2 \o s1, T2)
          end
      end
  end.

変更したのは変数の型を推論する処理と，let式の型を推論する処理ですね．

まず，変数trm_var xの型を型環境Gから取り出す時に，型パラメーターをfreshな名前の型変数で置き換えています． 型パラメーターをどのような型で具体化するかは型推論が進行するまで分からないので，とりあえず型変数で置いている感じです*9．

次に，let式trm_let t1 t2に型を付ける際，変数を束縛する項t1の（単相的な）型T1を求めた後，T1に現れる型変数のうち，型環境Gに現れない型変数は全て型パラメーターに一般化しています．Gの下でt1に型T1が付く（G\vdash t_1 : T_1）のなら，適当な型代入sに基づいてGとT1の型変数を置き換えてやったところでt1に型が付くのには変わりない（s G \vdash t_1 : s T_1）性質がありますから，sがGを変えない（s G = G）のなら，Gの下で項t1は型 s T_1を取れる（G \vdash t_1 : s T_1）はずです．つまりGの下でt1は，Gに現れないT1の型変数を適当に置き換えて得られるどのような型も取りうる訳ですから，Gに現れないT1の型変数は型パラメーターにしても型安全性を損なわない訳です．

正当性の証明の修正

型推論の実装を修正したので，それにあわせて型推論の正当性の証明を修正していきましょう．

まず型推論の健全性，型環境Gの下で項tの型推論が成功して型代入sと型Tが帰ってきたならば，Gの型変数をsに従って置き換えた型環境s Gの下でtには型Tといった性質の証明を修正しましょう． 単相の型推論器についてこの性質を検証した際，次のようなステートメントに対して帰納法を回していました．

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.

そのまんまですね．これを，次のようなステートメントに対して帰納法を回すように変更します．

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) = [::].

多相型の型変数を多相型で置き換えてしまうと冠頭標準形でない型を作れてしまいますから，sが代入するのは単相型のみであることを保証する訳ですね．

長くなってしまうので具体的な証明の修正内容については割愛しますが，後で述べる完全性と比較するとstraightforwardな修正だけで済みました．

次に型推論の完全性，型環境s Gの下で項tに型Tが付くのなら，Gの下でのtの型推論は成功し，sより一般的な型代入とTより一般的な型を返すといった性質の証明を修正します． 単相の型推論器についてこの性質を証明した際，以下のようなステートメントに対して帰納法を回していました．

Theorem typing_complete : forall t n G s T,
  (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'
    /\ (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)).

gensymの返す変数名がfreshであることを保証しないといけないつらみをひしひしと感じますね… これを，以下のようなステートメントに対して帰納法を回すように修正します．

Theorem typing_complete : forall t n G s T,
  {in env_fv G, forall x, typ_bv (s x) = [::]} ->
  (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' = [::]
    /\ (forall x, typ_bv (s' x) = [::])
    /\ (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)).

健全性の証明で述べた理由によりsやs'が単相型しか代入しないことも追加で保証する必要があって酷いことになっています．

健全性の証明に比べて，完全性の証明を修正するのは一筋縄にはいきません． 型推論の完全性は，どのような型が付くとしても型推論器はそれよりも一般的な型を返すといった性質ですが，let式の型付け規則typed_letを振り返ってみましょう．letで束縛する項t1にはありとあらゆるsで多相型T1の型パラメーターを具体化した型が付くかどうか確かめてから，束縛変数の型を決めていました．t1に付く型は下手すると無限個与えられる訳ですが，これはどれを選んで帰納法を回したものでしょう？*10

結局のところ，T1の型パラメーターをお互い被らないような型変数で具体化するようにsを選んで得られるのが，型付け規則から得られるt1の最も一般的な型なので，そのような型付けに対して帰納法の仮定を適用すれば何とかなります．どんな型付け関係を用意しても型推論の結果はその上をいくって言いたいわけですからね．

まとめ

以前Coqで実装した型推論器を拡張し，let多相も扱えるようにしました． それにあわせて，以前Coqで書いていた型推論の正当性の証明も修正しました．

正当性の証明の修正箇所についてはあまりにも多岐にわたるので具体的なコードで示すことはしませんでしたが，知りたい人はリポジトリのdiffなどを確認頂ければと思います．

今後の方針としては，やはり対象言語を参照も扱えるように拡張して，緩い値制約を入れると型安全になることも検証していきたいですね．OCaml使いとしては．

*1:と言っても今年の1月ぐらいですが．本当はAdvent Calendarに間に合わせたかったんですが，間に合わなかったんですよね．

*2:健全性の検証についての記事を書いたのが2015年ですから，随分間が空いてしまいました．いくつになってもこんなことばかりやってるな…

*3:プログラミング言語と言っても良いかもしれない

*4:値制限と言います．OCamlやSML#では値制限をもっと上手くしたもの実装されています

*5:なぜならletではなくfunで導入された変数なので

*6:量化子が全部一番前に来るやつ

*7:要するにlocally namelessで良く見るあれです

*8:locally namelessで言うところのcofinite quantificationってやつです

*9:型推論って終始そんなノリですよね?

*10:型安全性の証明でサボったツケを払わされている…