# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1485753914 -32400
# Node ID 3aeabd46d72b2a88e1621ff43faf0446bf8ceffd
# Parent  2c42cfe593e66d79d5caf146d7c8a63a5983e245
Wrote subtype

diff -r 2c42cfe593e6 -r 3aeabd46d72b paper/type.tex
--- a/paper/type.tex	Sun Jan 29 22:13:47 2017 +0900
+++ b/paper/type.tex	Mon Jan 30 14:25:14 2017 +0900
@@ -960,6 +960,8 @@
 
 % }}}
 
+% {{{ 部分型付け
+
 \section{部分型付け}
 単純型付きラムダ計算では、ラムダ計算の項が型付けされることを確認した。
 ここで、 単純型の拡張として、レコードを導入する。
@@ -1040,10 +1042,100 @@
     \AxiomC{$\Gamma \vdash t : S $}
     \AxiomC{$ S <: T $}
     \BinaryInfC{$ \Gamma \vdash t : T$}
-    \DisplayProof && \text { T-SUB}
+    \DisplayProof && \text {T-SUB}
 \end{align*}
 
 この規則は $ S <: T $ ならば $ S $ 型の要素 $ t$はすべて $ T $の要素であると言っている。
 例えば、先程の $ \{ x : Nat \} $ と $ \{ x : Nat , y : Bool\}$ が $ \{ x : Nat , y : Bool\} <: \{ x : Nat \}$ となるように部分型関係を定義した時に $ \Gamma \vdash \{x=0, y=1\} : \{ x : Nat \}$ を導ける。
 
+部分型関係は $ S <: T $ という形式の部分型付け式を導入するための推論規則の集まりとして定式化される。
+始めに、部分型付けの一般的な規定から考える。
+部分型は反射的であり、推移的である。
+
+\begin{align*}
+    S <: S && \text{S-REFL} \\
+    \AxiomC{$S <: U$}
+    \AxiomC{$U <: T$}
+    \BinaryInfC{$ S <: T $}
+    \DisplayProof && \text{S-TRANS}
+\end{align*}
+
+これらの規則は安全代入に対する直感より正しい。
+次に、基本型や関数型、レコード型などの型それぞれに対して、その形の型の要素が期待される部分に対して上位型の要素を利用しても安全である、という規則を導入していく。
+
+レコード型については型 $ T = \{ l_i : T_1 ... l_n : T_n\} $が持つフィールドが型 $ S = \{ k_1 : S_1 ... k_n : T_n\} $のものよりも少なければ $S$ を $T$の部分型とする。
+つまりレコードの終端フィールドのいくつかを忘れてしまっても安全である、ということを意味する。
+この直感は幅部分型付け規則となる。
+
+\begin{align*}
+    \{l_i : T_i^{\; i \in 1..n+k} \} <: \{l_i : T_i^{\; i \in 1..n}\}
+    && \text{S-RCDWIDTH}
+\end{align*}
+
+フィールドの多い方が部分型となるのは名前に反するように思える。
+しかし、フィールドが多いレコードほど制約が多くなり表すことのできる集合の範囲は小さくなる。
+集合の大きさで見ると明かにフィールドの多い方が小さいのである。
+
+幅部分型付け規則が適用可能なのは、共通のフィールドの型が全く同じな場合のみである。
+しかし、その場合フィールドの型に部分型を導入できず、フィールドの型の扱いで同じ問題を抱えることとなる。
+そのために導入するのが深さ部分型付けである。
+二つのレコードの中で対応するフィールドの型が部分型付け関係にある時に個々のフィールドの型が異なることを許す。
+これは具体的には以下の規則となる。
+
+\begin{align*}
+    \AxiomC{各iに対して $S_i <: T_i$}
+    \UnaryInfC{$\{ l_i : S_i^{\; i \in 1..n}\} <: \{l_i : T_i^{\; i \in 1..n}\}$}
+    \DisplayProof && \text{S-RCDDEPTH}
+\end{align*}
+
+これらを用いて $ \{ x : \{a : Nat , b : Nat\}, y : \{m : Nat\}\}$ が $ \{x : \{ a : Nat\}, y : \{\}\}$の部分型であることは以下のように導出できる。
+
+\begin{prooftree}
+    \AxiomC{}
+    \RightLabel{S-RCDWIDTH}
+    \UnaryInfC{$ \{a : Nat, b : Nat\} <: \{a : Nat\}$}
+    \AxiomC{}
+    \RightLabel{S-RCDWIDTH}
+    \UnaryInfC{$ \{m : Nat\} <: \{\}$}
+    \RightLabel{S-RCDDEPTH}
+    \BinaryInfC{$ \{ x : \{a : Nat , b : Nat\}, y : \{m : Nat\}\} <:  \{x : \{ a : Nat\}, y : \{\}\}$}
+\end{prooftree}
+
+最後に、レコードを利用する際はフィールドさえ揃っていれば順序は異なっても良いという規則を示す。
+
+\begin{align*}
+    \AxiomC{$ \{ k_j : S_j^{\; i \in 1 .. n} \}$ は $ \{ l_i : T_i^{\; i \in 1 ..n}\} $ の並べ替えである}
+    \UnaryInfC{$ \{k_j : S_j^{\; j \in 1..n} \} <: \{l_i : T_i^{\; i \in 1..n }\}$}
+    \DisplayProof && \text{S-RCDPERM}
+\end{align*}
+
+S-RCDPERM を用いることで、終端フィールドだけではなく任意の位置のフィールドを削ることができる。
+
+レコードの部分型は定義できたので、次は関数の部分型を定義していく。
+関数の部分型は以下 S-ARROW として定義できる。
+
+\begin{align*}
+    \AxiomC{$ T_1 <: S_1$}
+    \AxiomC{$ S_2 <: T_2$}
+    \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $}
+    \DisplayProof && \text{S-ARROW}
+\end{align*}
+
+前提の条件二つを見ると部分型の関係が逆転している。
+左側の条件は関数型自身の型と逆になっているため反変と言い、返り値の型は同じ向きであるため共変と言う。
+引数について考えた時、求める型よりも大きい型であれば明らかに安全に呼ぶことができるために関数の引数の型の方が上位型になる。
+返り値については関数が返す型が部分型であれば上位型を返すことができるため、関数の返り値の方が部分型になる。
+
+別の見方をすると、型 $ S_1 \rightarrow S_2 $ の関数を別の型 $ T_1 \rightarrow T_2 $が期待される文脈で用いることが安全な時とは
+
+\begin{itemize}
+    \item 関数に渡される引数がその関数にとって想定外でない($ T_1 <: S_1$)
+    \item 関数が返す値も文脈にとって想定外でない($ S_2 <: T_2 $)
+\end{itemize}
+
+という場合に限る。
+
+% }}}
+
+
 \section{部分型と Continuation based C}