Types: 型システム
次に取り組む内容は型システムです。
型システムは、式をその評価結果の「かたち」で分類する静的解析手法です。
まずは、非常に簡単に把握できる言語から始め、型に関する基本的な考え方や型付け規則、型保存(type preservation)や進行(progress)といった型システムに関する基礎的な定理を導入します。
Stlc章では、単純型付きラムダ計算(simply typed lambda-calculus)に移ります。
単純型付きラムダ計算は（Coq を含む）近代的な関数型プログラミング言語すべての中心概念になっています。
Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Arith.Arith.
From PLF Require Import Maps.
From PLF Require Import Imp.
From PLF Require Import Smallstep.
Hint Constructors multi.
型システムについての議論を始めるために、例のごとく、ごく単純な言語から始めましょう。
この言語は、実行時の型エラーでまずいことが起きる可能性のあるものであってほしいので、 Smallstep 章で使った、定数と足し算だけの言語よりはもう少し複雑なものでなければなりません。
データが一種類だけ（数のみ）では単純すぎますが、二種類（数とブール値）なら、実験のための材料はもう揃っています。
言語の定義はいつも通り、お決まりの作業です。
非形式的な構文は以下の通りです。
t ::= tru
| fls
| test t then t else t
| zro
| scc t
| prd t
| iszro t
そして形式的には以下の通りです。
Inductive tm : Type :=
| tru : tm
| fls : tm
| test : tm -> tm -> tm -> tm
| zro : tm
| scc : tm -> tm
| prd : tm -> tm
| iszro : tm -> tm.
Inductive bvalue : tm -> Prop :=
| bv_tru : bvalue tru
| bv_fls : bvalue fls.
Inductive nvalue : tm -> Prop :=
| nv_zro : nvalue zro
| nv_scc : forall t, nvalue t -> nvalue (scc t).
Definition value (t : tm) := bvalue t \/ nvalue t.
Hint Constructors bvalue nvalue.
Hint Unfold value.
Hint Unfold update.
1ステップ関係について、まず非形式的なものを見ます。
------------------------------- (ST_TestTru)
test tru then t1 else t2 --> t1
------------------------------- (ST_TestFls)
test fls then t1 else t2 --> t2
t1 --> t1'
---------------------------------------------------- (ST_Test)
test t1 then t2 else t3 --> test t1' then t2 else t3
t1 --> t1'
------------------ (ST_Scc)
scc t1 --> scc t1'
--------------- (ST_PrdZro)
prd zro --> zro
numeric value v1
------------------- (ST_PrdScc)
prd (scc v1) --> v1
t1 --> t1'
------------------ (ST_Prd)
prd t1 --> prd t1'
----------------- (ST_IszroZro)
iszro zro --> tru
numeric value v1
---------------------- (ST_IszroScc)
iszro (scc v1) --> fls
t1 --> t1'
---------------------- (ST_Iszro)
iszro t1 --> iszro t1'
そして形式的なものです。
Reserved Notation "t1 '-->' t2" (at level 40).
Inductive step : tm -> tm -> Prop :=
| ST_TestTru : forall t1 t2,
(test tru t1 t2) --> t1
| ST_TestFls : forall t1 t2,
(test fls t1 t2) --> t2
| ST_Test : forall t1 t1' t2 t3,
t1 --> t1' ->
(test t1 t2 t3) --> (test t1' t2 t3)
| ST_Scc : forall t1 t1',
t1 --> t1' ->
(scc t1) --> (scc t1')
| ST_PrdZro :
(prd zro) --> zro
| ST_PrdScc : forall t1,
nvalue t1 ->
(prd (scc t1)) --> t1
| ST_Prd : forall t1 t1',
t1 --> t1' ->
(prd t1) --> (prd t1')
| ST_IszroZro :
(iszro zro) --> tru
| ST_IszroScc : forall t1,
nvalue t1 ->
(iszro (scc t1)) --> fls
| ST_Iszro : forall t1 t1',
t1 --> t1' ->
(iszro t1) --> (iszro t1')
where "t1 '-->' t2" := (step t1 t2).
Hint Constructors step.
step 関係は元の式が大域的に意味を持つかは考慮せず、「次の」簡約操作が適切な種類の対象へ適用されることだけを確認していることに注意してください。
例えば、 scc tru は先に進むことはできませんが、明らかに同程度に無意味な項
scc (test tru then tru else tru)
は（行き詰まるまでに1ステップ）進めることができます。
scc (test tru then tru else tru)
この言語の step 関係について、まず注目に値するのは、 Smallstep 章の強進行性定理(strong progress theorem)が成り立たないということです。
すなわち、正規形ではあるのに（これ以上簡約できないのに）、値ではない項があるのです（これは、そのような項を想定する「簡約結果」と定義しなかったからです）。
そのような項は「行き詰まる(stuck)」ことになります。
Notation step_normal_form := (normal_form step).
Definition stuck (t : tm) : Prop :=
step_normal_form t /\ ~ value t.
Hint Unfold stuck.
☐
ただし、この言語では値の集合と正規形の集合は同一ではありませんが、値の集合は正規形の集合の部分集合になっています。
これは重要なことで、さらに簡約できる値を定義してしまうことはないことを表しています。
（ヒント: 証明中で、数値であることがわかっている項に対して帰納的推論をしなければならないことになります。
この帰納法は、その項自体にして適用することもできますし、その項が数値であるという事実に対して適用することもできます。
どちらでも証明は進められますが、片方はもう片方よりもかなり短くなります。
練習として、ふたつの方法両方で証明を完成させなさい。）
☐
☐
次にこの言語から見て取れる非常に重要なことは、行き詰まる項があったとしても、そのような項は、我々としても意味を持つことすらやめてほしいようなブール値と数の取り混ぜ方をしたもので、すべて無価値なものであるということです。
項とその評価結果の型（数かブール値）を関係づける型付け関係を定義することで、そのような、型の付かない項を除くことができます。
非形式的な記法では、型付け関係を |- t \in T と書き、「t の型は T である」と読みます。
記号 |- は「ターンスタイル（turnstile）」と呼びます。
後の章ではより複雑になり、ターンスタイルの左側に追加の「コンテキスト」引数を付ける型付け関係もあります。
ここでは、コンテキストは常に空です。
--------------- (T_Tru)
|- tru \in Bool
--------------- (T_Fls)
|- fls \in Bool
|- t1 \in Bool |- t2 \in T |- t3 \in T
-------------------------------------------- (T_Test)
|- test t1 then t2 else t3 \in T
-------------- (T_Zro)
|- zro \in Nat
|- t1 \in Nat
----------------- (T_Scc)
|- scc t1 \in Nat
|- t1 \in Nat
----------------- (T_Prd)
|- prd t1 \in Nat
|- t1 \in Nat
-------------------- (T_IsZro)
|- iszro t1 \in Bool
Reserved Notation "'|-' t '\in' T" (at level 40).
Inductive has_type : tm -> ty -> Prop :=
| T_Tru :
|- tru \in Bool
| T_Fls :
|- fls \in Bool
| T_Test : forall t1 t2 t3 T,
|- t1 \in Bool ->
|- t2 \in T ->
|- t3 \in T ->
|- test t1 t2 t3 \in T
| T_Zro :
|- zro \in Nat
| T_Scc : forall t1,
|- t1 \in Nat ->
|- scc t1 \in Nat
| T_Prd : forall t1,
|- t1 \in Nat ->
|- prd t1 \in Nat
| T_Iszro : forall t1,
|- t1 \in Nat ->
|- iszro t1 \in Bool
where "'|-' t '\in' T" := (has_type t T).
Hint Constructors has_type.
Example has_type_1 :
|- test fls zro (scc zro) \in Nat.
Proof.
apply T_Test.
- apply T_Fls.
- apply T_Zro.
- apply T_Scc.
+ apply T_Zro.
Qed.
（型付け関係のすべての構成子をヒントデータベースに登録してあるので、実際には auto で証明を自動的に構築することができます。）
型付け関係というのは保守的な（または静的な）近似です。
型付け関係では、簡約で何が起こるかを考慮しませんし、また特に項の正規形の型を計算しているわけでもありません。
Example has_type_not :
~ ( |- test fls zro tru \in Bool ).
Proof.
intros Contra. solve_by_inverts 2. Qed.
☐
Canonical forms
Lemma bool_canonical : forall t,
|- t \in Bool -> value t -> bvalue t.
Proof.
intros t HT [Hb | Hn].
- assumption.
- induction Hn; inversion HT; auto.
Qed.
Lemma nat_canonical : forall t,
|- t \in Nat -> value t -> nvalue t.
Proof.
intros t HT [Hb | Hn].
- inversion Hb; subst; inversion HT.
- assumption.
Qed.
型付け関係には重要な性質がふたつあります。
最初のものは、型のついた(well-typed)正規形は行き詰まっていない、というものです。
別の言い方をすれば、もし項に型がつくなら、項は値であるか、または1ステップは進めるということです。
この性質を「進行性(progress)」と言います。
Complete the formal proof of the progress property. (Make sure
you understand the parts we've given of the informal proof in the
following exercise before starting -- this will save you a lot of
time.)
Proof with auto.
intros t T HT.
induction HT...
-
right. inversion IHHT1; clear IHHT1.
+
apply (bool_canonical t1 HT1) in H.
inversion H; subst; clear H.
exists t2...
exists t3...
+
inversion H as [t1' H1].
exists (test t1' t2 t3)...
Admitted.
intros t T HT.
induction HT...
-
right. inversion IHHT1; clear IHHT1.
+
apply (bool_canonical t1 HT1) in H.
inversion H; subst; clear H.
exists t2...
exists t3...
+
inversion H as [t1' H1].
exists (test t1' t2 t3)...
Admitted.
☐
証明: |- t \in T の導出に関する帰納法で証明する。
☐
この定理は Smallstep の章の強進行性定理よりも興味深いものです。
Smallstep の章では、正規形はすべて値でした。
本章では項が行き詰まることもありますが、行き詰まるようなものは型のつかないものだけです。
型付けの第二の重要な性質は、型のついた項を一段階簡約すると、簡約結果もまた型のつく項である、ということです。
Complete the formal proof of the preservation property. (Again,
make sure you understand the informal proof fragment in the
following exercise first.)
Proof with auto.
intros t t' T HT HE.
generalize dependent t'.
induction HT;
intros t' HE;
try solve_by_invert.
- inversion HE; subst; clear HE.
+ assumption.
+ assumption.
+ apply T_Test; try assumption.
apply IHHT1; assumption.
Admitted.
☐
証明: |- t \in T の導出に関する帰納法で証明する。
- 導出で直前に使った規則が T_Test の場合、 t = test t1 then t2 else t3、かつ |- t1 \in Bool、 |- t2 \in T かつ |- t3 \in T である。
t が test ... の形式であることとスモールステップ簡約関係を見ると、 t --> t' を示すために使えるのは ST_TestTru、 ST_TestFls または ST_Test のみである。
- 直前の規則が ST_TestTru の場合、 t' = t2 である。
|- t2 \in T であるのでこれは求める結果である。
- 直前の規則が ST_TestFls の場合、 t' = t3 である。
|- t3 \in T であるのでこれは求める結果である。
- 直前の規則が ST_Test の場合、 t' = test t1' then t2 else t3' である。
ここで、 t1 --> t1' である。 |- t1 \in Bool であるので、帰納法の仮定から |- t1' \in Bool である。
また、 T_Test 規則から |- test t1' then t2 else t3 \in T であり、これは求める結果である。
- 直前の規則が ST_TestTru の場合、 t' = t2 である。
|- t2 \in T であるのでこれは求める結果である。
☐
練習問題: ★★★, standard (preservation_alternate_proof)
Theorem preservation' : forall t t' T,
|- t \in T ->
t --> t' ->
|- t' \in T.
Proof with eauto.
Admitted.
☐
型保存定理は「主部簡約（subject reduction）」性と呼ばれることが多々あります。
これは、この定理が型付け関係の主部が簡約されるときに起こることについて言っているからです。
この用語は型付けを文として見たことによるもので、項が主部（subject）、型が述部（predicate）に当たります。
進行と型保存を合わせると、型のついた項は決して行き詰まらないことを示せます。
Definition multistep := (multi step).
Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).
Corollary soundness : forall t t' T,
|- t \in T ->
t -->* t' ->
~(stuck t').
Proof.
intros t t' T HT P. induction P; intros [R S].
destruct (progress x T HT); auto.
apply IHP. apply (preservation x y T HT H).
unfold stuck. split; auto. Qed.
練習問題: ★★, standard, recommended (subject_expansion)
☐
練習問題: ★★, standard (variation1)
| T_SccBool : forall t,
|- t \in Bool ->
|- scc t \in Bool
- step の決定性
- 進行
- 型保存
☐
Suppose, instead, that we add this new rule to the step relation:
| ST_Funny1 : forall t2 t3,
(test tru t2 t3) --> t3
Which of the above properties become false in the presence of
this rule? For each one that does, give a counter-example.
Exercise: 2 stars, standard (variation2)
練習問題: ★★, standard (variation2)
| ST_Funny1 : forall t2 t3,
(test tru t2 t3) --> t3
☐
練習問題: ★★, standard, optional (variation3)
| ST_Funny2 : forall t1 t2 t2' t3,
t2 --> t2' ->
(test t1 t2 t3) --> (test t1 t2' t3)
練習問題: ★★, standard, optional (variation4)
| ST_Funny3 :
(prd fls) --> (prd (prd fls))
練習問題: ★★, standard, optional (variation5)
| T_Funny4 :
|- zro \in Bool
練習問題: ★★, standard, optional (variation6)
| T_Funny5 :
|- prd zro \in Bool
練習問題: ★★★, standard, optional (more_variations)
練習問題: ★, standard (remove_predzero)
☐
練習問題: ★★★★, advanced (prog_pres_bigstep)
☐