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

diff -r 3b2446944d11 -r 2c42cfe593e6 paper/type.tex
--- a/paper/type.tex	Sun Jan 29 21:58:35 2017 +0900
+++ b/paper/type.tex	Sun Jan 29 22:13:47 2017 +0900
@@ -1024,5 +1024,26 @@
 \end{definition}
 
 レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。
+しかし、引数にレコードを取る場合、その型と完全に一致させる必要がある。
+例えば $ \{ x : Nat \} $ を引数に取る関数に対して $ \{ x : Nat , y : Bool\}$ といった値を適用することができない。
+しかし、直感的には関数の要求はフィールド $x $ が型 $Nat$を持つことのみであり、その部分にのみ注目すると$ \{ x : Nat , y : Bool\}$ も要求に沿っている。
+
+部分型付けの目標は上記のような場合の項を許すように型付けを改良することにある。
+つまり型 $ S $ の任意の項が、型 $ T $ の項が期待される文脈において安全に利用できることを示す。
+この時、$ S $ を $ T $ の部分型と呼び、 $ S <: T $ と書く。
+これは型 $ S $ が型 $ T $よりも情報を多く持っていることを示しており、$S$は$T$の部分型である、と読む。
+$ S <: T $ の別の読み方として、型 $ T $ は型 $ S $ の上位型である、という読み方も存在する。
+
+型付け関係と部分型関係をつなぐための新しい型付け規則を考える。
+
+\begin{align*}
+    \AxiomC{$\Gamma \vdash t : S $}
+    \AxiomC{$ S <: T $}
+    \BinaryInfC{$ \Gamma \vdash t : T$}
+    \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 \}$ を導ける。
 
 \section{部分型と Continuation based C}