この記事は言語実装 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.31で動作を確認していますが,動かなかったらPRでも投げて下さい.
型推論の検証ですが,実は僕は2年前にも言語実装 Advent Calendar 2015でやったことがあります. もっともその時は型推論の健全性—型推論のアルゴリズムが正常に終了して型代入と型が帰ってきた場合,項は型環境の下で型を持つこと2—しか証明していませんでしたから,リベンジマッチとして完全性—項が型環境の下で型を持つような型代入が存在する場合,型推論のアルゴリズムは正常に終了してより一般的な解を返すこと—も証明しようと思います.
型についての諸々の定義
それでは始めにCoq上で単純型付きλ計算の型を定義していきましょう.
Inductive typ : Set := | typ_fvar (x : nat) | typ_arrow (T1 T2 : typ).
型変数は型で3,関数型も型(かつ,それ以外型でない).簡単ですね.
型に対する型代入の適用はこんな感じ.
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かどうかを延々と議論していく訳ですから,型に含まれる型変数の集合を定義します.
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—型の中に型変数が現れるかの判定—はこう書けます.
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.
タクティックでプログラムを書いているので少し分かりづらいですが,型変数からなる型に型変数が現れるか調べる際は,とが等しいか調べて,型に型変数が現れるか調べる際は,まず型に現れるか調べて,含まれていなければ型に現れるか調べて…と自然な定義になっています.
以上を踏まえて,制約を解く単一化のアルゴリズムを実装するならば以下のような感じでしょうか.
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.
制約はリスト[(T11, T21); ... ; (T1n, T2n)]
で表現しています.
typ_eq_dec T1 T2
は型T1
とT2
が等しいかの判定ですね.
この単一化の実装は正直愚直ってレベルではない4のですが,今回検証する型推論のアルゴリズムではそこまで複雑な入力を与えられないと思うので,そのままにしておきます.
この単一化の手続きは健全—が正常に停止して代入を返した場合,は制約の解になっている—かつ完全—制約に解が存在する場合,は正常に停止してより一般的な代入を返す—ですが,それらの証明の大筋は2年前と同様なので省略します.
項についての諸々の定義
次に,Coq上で単純型付きλ計算の項を定義していきましょう.
Inductive trm : Set := | trm_var (n : nat) | trm_abs (T : typ) (t : trm) | trm_app (t1 t2 : trm).
変数があり,λ抽象があり,関数適用がある.自然ですね. ここで,変数束縛をde Bruijn indicesで表現している5ことと,関数引数に型注釈が付いていることに注意して下さい. 型注釈があるのに型推論の手続きを考えるのか?と思われるかもしれませんが,型注釈のところをfreshな型変数で補えば型注釈の無い項についての型推論の手続きも実装できます.
項に関連する定義で注意すべきはそれぐらいで,その他の定義は自明です. 項に対する型代入の適用の定義は以下の通りになり,
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.
項に現れる型変数の集合の定義は以下の通りになります.
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.
型判断についての諸々の定義
続いて,単純型付きλ計算の型判断に必要な定義を準備していきましょう. 変数束縛をde Bruijn indicesで表現したので,型環境は型の有限列,つまり型のリストで十分です.
Definition env := list typ.
型環境に含まれる型変数の集合はfold_right
で記述でき,
Definition env_ftv (G : env) := fold_right (fun T s => Union _ (typ_fv T) s) (Empty_set _) G.
型環境に対する型代入の適用はmap
で記述できます.
Definition env_subst_typ s G := map (typ_subst s) G.
この型環境の定義を用いると,型判断は以下のように定義できます.
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.
ここで,型推論の健全性を証明する上で重要となる型代入補題を紹介しておきます. これはが成り立つ場合,も成り立つという補題で, 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).
型推論の実装
まず,型推論の実装について考えてみましょう.一般的な教科書6では型推論を解説する際,型についての方程式を立て,それを解くのだといった喩えが良く用いられています.説明のためにfreshな型変数の生成(gensym)をlet x := fresh in ...
と書くことにすると,方程式(制約)を抽出する(と共に単一化前の型を返す)アルゴリズムは以下のような疑似コードで表現できます.
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多相に拡張する際に問題があります7.と言うのも,let多相では項を型環境の下で型付けする際の型はに含まれない型変数で量化しても良い訳ですが,の再帰呼び出しをしただけではの型が確定しないため,どの型変数を量化して良いか分からないのです.
そこで,いちいちプログラム全体に型を付けるための制約ができるのを待ってから単一化をするのではなく,必要になった制約をその場で単一化する(つまり,局所的な解を確定させる)ようなアルゴリズムを考えましょう.こうすればを型付けしてが得られた時点で,どの型変数がに含まれないのか分かりますね.疑似コードにすると以下の通りでしょうか.
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.
実際の型推論器8も,(参照を用いているために型代入の適用が隠れているものの)このように制約が必要になった段階で単一化を行う実装になっています. もっとも,この疑似コードは構造的再帰になっていないため,(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.
このはの下でのの型を推論するアルゴリズムです.
そういえば,説明のために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.
このはをgensymの持っている状態としての下でのの型を推論し,変更されたgensymの状態と共に結果を返すアルゴリズムです. 今回はこの型推論の実装を採用し,検証を行います.
型推論の検証
それでは準備も済んだことですし,型推論の正当性を検証していきましょう.始めに型推論の健全性—が正常に終了して型代入と型が帰ってきた場合,項は型環境の下で型を持つこと—から証明します.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.
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.
示すのが大変なのは型推論の完全性—項が型環境の下で型を持つような型代入が存在し,状態の下でgensymがやに含まれる型変数を返さない場合,型推論のアルゴリズムは正常に終了して,より一般的な解ととに含まれる型変数をgensymが返さないような状態を返すこと—です.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.
これら健全性と完全性の系として,型環境と項が与えられたとき,型付けできるならば主要型9とその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
以下の型変数しか持たない型を表すようにすると良さそうです.
-
古くないか?↩
-
型推論によって型変数の中身が確定したら,中身を代入してやる必要があるのでが必要になります.型変数を参照として扱うと,この代入が暗黙のうちに行われるので必要性が分かりづらいかもしれませんが…↩
-
ここでの型変数とは自由な型変数です.let多相に対応する場合,ここに束縛された型変数を表す
typ_bvar
なるコンストラクタが増えることでしょう… 型変数のシンボルを自然数で表すのはde Bruijn indexと紛らわしいですが,参照を使わずにgensymを書く都合上(Gallinaに参照は無いので)こうなっています.↩ -
型代入]が得られた瞬間に,その場で残りの制約への代入を行っています.おまけに経路圧縮も行っていません.↩
-
型変数の束縛はlocally nameless representationで扱うつもりなのに変数束縛はde Bruijn indicesで扱うのか!?と思うかもしれませんが,これは単に僕がde Bruijn indices好きだからです.型変数の束縛をlocally nameless representationで扱おうと考えているのは,型推論の都合上そちらの方が向いている(自由な型変数は名前として扱いたい)と考えたからにすぎません.↩
-
まぁまだ拡張してないんですけどね.↩