Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/type.tex @ 84:f3ea67a23cf6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update type.tex
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 13:57:35 +0900
parents c0199291c58e
children 2be864ed3a79
comparison
equal deleted inserted replaced
83:c0199291c58e 84:f3ea67a23cf6
86 ここで構造体に対して「構造体型」という一つの型を用意した場合、複数の構造体の区別ができなくなる。 86 ここで構造体に対して「構造体型」という一つの型を用意した場合、複数の構造体の区別ができなくなる。
87 よって、構造体に型を付けるなら「何を内部に持っているのか」を覚えているような型でなくてはならない。 87 よって、構造体に型を付けるなら「何を内部に持っているのか」を覚えているような型でなくてはならない。
88 88
89 ここでレコード型という型を導入する。 89 ここでレコード型という型を導入する。
90 レコード型は複数の型を持ちえる型であり、内部に持っている値にはユニークな名前がラベルとして付いている。 90 レコード型は複数の型を持ちえる型であり、内部に持っている値にはユニークな名前がラベルとして付いている。
91 例えば「Intの変数x とIntの変数yを持つレコード型」は$ \{ x : Int , y : Bool\}$のように記述する。
92 C における構造体ではリストに対応する。
91 % TODO C の構造体 93 % TODO C の構造体
94
92 レコード型の値を構成する際には、内部に格納する値を全て与えることで構成できる。 95 レコード型の値を構成する際には、内部に格納する値を全て与えることで構成できる。
93 % TODO C の構造体の初期化 96 % TODO C の構造体の初期化
94 レコード型から値を取り出す際にはラベル名を用いた射影を利用する。 97 レコード型から値を取り出す際にはラベル名を用いた射影を利用する。
95 C 言語では構造体の後に \verb/./ キーワードを付けた後にラベル名を指定する。 98 C 言語では構造体の後に \verb/./ キーワードを付けた後にラベル名を指定する。
96 99
100 % {{{ 部分型付け 103 % {{{ 部分型付け
101 104
102 \section{部分型付け} 105 \section{部分型付け}
103 レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。 106 レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。
104 しかし、関数が引数にレコードを取る場合、その型と完全に一致させる必要がある。 107 しかし、関数が引数にレコードを取る場合、その型と完全に一致させる必要がある。
105 例えば $ \{ x : Nat \} $ を引数に取る関数に対して $ \{ x : Nat , y : Bool\}$ といった値を適用することができない。 108 例えば $ \{ x : Int \} $ を引数に取る関数に対して $ \{ x : Int , y : Bool\}$ といった値を適用することができない。
106 しかし、直感的には関数の要求はフィールド $x $ が型 $Nat$を持つことのみであり、その部分にのみ注目すると$ \{ x : Nat , y : Bool\}$ も要求に沿っている。 109 しかし、直感的には関数の要求はフィールド $x $ が型 $Int$を持つことのみであり、その部分にのみ注目すると$ \{ x : Nat , y : Bool\}$ も要求に沿っている。
107 110
108 ここで、部分型という型を導入する。 111 ここで、部分型という型を導入する。
109 部分型は上記のような場合の項を許すように型付けを緩めることである。 112 部分型は上記のような場合の項を許すように型付けを緩めることである。
110 つまり型 $ S $ を持つ値が、型 $ T $ の値が期待される文脈において安全に利用できることを示す。 113 つまり型 $ S $ を持つ値が、型 $ T $ の値が期待される文脈において安全に利用できることを示す。
111 この時、$ S $ を $ T $ の部分型と呼び、 $ S <: T $ と書く。 114 この時、$ S $ を $ T $ の部分型と呼び、 $ S <: T $ と書く。
149 % }}} 152 % }}}
150 153
151 % {{{ 部分型と Continuation based C 154 % {{{ 部分型と Continuation based C
152 155
153 \section{部分型と Continuation based C} 156 \section{部分型と Continuation based C}
154 TODO なおす
155 部分型を用いて Conituation based C の型システムを定義していく。 157 部分型を用いて Conituation based C の型システムを定義していく。
156 158
157 まず、DataSegment の型から定義してく。 159 まず、DataSegment の型を定義する。
158 DataSegment 自体はCの構造体によって定義されているため、レコード型として考えることができる。 160 DataSegment 自体はCの構造体によって定義されているため、レコード型として考えることができる。
159 例えばリスト~\ref{src:akasha-context}に示していた DataSegment の一つに注目する(リスト~\ref{src:type-ds})。 161 例えばリスト~\ref{src:akasha-context}に示していた DataSegment の一つに注目する(リスト~\ref{src:type-ds})。
160 162
161 \lstinputlisting[label=src:type-ds, caption=akashaContext の DataSegment である AkashaInfo] {src/type-ds.h} 163 \lstinputlisting[label=src:type-ds, caption=akashaContext の DataSegment である AkashaInfo] {src/type-ds.h}
162 この AkashaInfo は $ \{ minHeight : unsigned\; int , maxHeight : unsigned \; int, akashaNode : AkashaNode*\}$ であると見なせる。 164 この AkashaInfo は $ \{ minHeight : unsigned\; int , maxHeight : unsigned \; int, akashaNode : AkashaNode*\}$ 型を持つ。
163 CodeSegment は DataSegment を引数に取るため、DataSegment の型は CodeSegment が要求する最低限の制約をまとめたものと言える。 165 CodeSegment は DataSegment を引数に取るため、DataSegment の型は CodeSegment が要求する最低限の制約をまとめたものと言える。
164 166
165 次に Meta DataSegment について考える。 167 次に Meta DataSegment について考える。
166 Meta DataSegment はプログラムに出現する DataSegment の共用体であった。 168 Meta DataSegment はプログラムに出現する DataSegment の共用体であった。
167 これを DataSegment の構造体に変更する。 169 これを DataSegment の構造体に変更する。
168 こうすることにより、 Meta DataSegment はプログラム中に出現する DataSegment を必ず持つため、Meta DataSegment は任意の DataSegment の部分型となる。 170 こうすることにより、 Meta DataSegment はプログラム中に出現する DataSegment を必ず持つため、Meta DataSegment は任意の DataSegment の部分型となる。
169 もしくは各 DataSegment の全てのフィールドを含むような1つの構造体でも良い。 171 もしくは各 DataSegment の全てのフィールドを含むような1つの構造体でも良い。
170 第~\ref{chapter:cbc-type}章における Meta DataSegment はそのように定義している。 172 第~\ref{chapter:cbc-type}章における Meta DataSegment はそのように定義している。
171 なお、GearsOSでは DataSegment の共用体をプログラムで必要な数だか持つ実装になっている。 173 なお、GearsOSでは DataSegment の共用体をプログラムで必要な数だけ持つ実装になっている。
172 174
173 具体的な CbC における Meta DataSegment であるContext (リスト~\ref{src:type-mds})は、 DataSegment の集合を値として持っているために明らかに DataSegment よりも多くの情報を持っている。 175 具体的な CbC における Meta DataSegment であるContext (リスト~\ref{src:type-mds})は、 DataSegment の集合を値として持っているために明らかに DataSegment よりも多くの情報を持っている。
174 \lstinputlisting[label=src:type-mds, caption=CbC の Meta DataSegment である Context] {src/type-mds.h} 176 \lstinputlisting[label=src:type-mds, caption=CbC の Meta DataSegment である Context] {src/type-mds.h}
175 177
176 部分型として定義するなら以下のような定義となる。 178 部分型として定義するなら以下のような定義となる。
177 179
178 \begin{definition} 180 \begin{definition}
179 Meta DataSegment の定義 181 Meta DataSegment の定義
180 182
181 \begin{align*} 183 \begin{align*}
182 Meta \; DataSegment <: DataSegment_i^{i \in N} && \text{S-MDS} 184 Meta \; DataSegment <: プログラム中の任意のDataSegment
183 \end{align*} 185 \end{align*}
184 \end{definition} 186 \end{definition}
185 187
186 なお、$N$はあるプログラムに出現するデータセグメントの名前の集合であるとする。
187
188 次に CodeSegment の型について考える。 188 次に CodeSegment の型について考える。
189 CodeSegment は DataSegment を DataSegment へと移す関数型とする。 189 CodeSegment は DataSegment を DataSegment へと移す関数型とする。
190 190
191 \begin{definition} 191 \begin{definition}
192 CodeSegment の定義 192 CodeSegment の定義
193 193
194 \begin{align*} 194 \begin{align*}
195 DataSegment \rightarrow DataSegment && \text{T-CS} 195 DataSegment \rightarrow DataSegment
196 \end{align*} 196 \end{align*}
197 \end{definition} 197 \end{definition}
198 198
199 そして Meta CodeSegmentは Meta DataSegment を Meta DataSegment へと移す関数となる。 199 そして Meta CodeSegmentは Meta DataSegment を Meta DataSegment へと移す関数となる。
200 200
201 \begin{definition} 201 \begin{definition}
202 Meta CodeSegment の定義 202 Meta CodeSegment の定義
203 203
204 \begin{align*} 204 \begin{align*}
205 Meta \; DataSegment \rightarrow Meta \; DataSegment && \text{T-MCS} 205 Meta \; DataSegment \rightarrow Meta \; DataSegment
206 \end{align*} 206 \end{align*}
207 \end{definition} 207 \end{definition}
208 208
209 ここで具体的なコード(リスト~\ref{src:type-cs})と比較してみる。 209 ここで具体的なコード(リスト~\ref{src:type-cs})と比較してみる。
210 210
211 \lstinputlisting[label=src:type-cs, caption=具体的なCbCにおける CodeSegment] {src/type-cs.c} 211 \lstinputlisting[label=src:type-cs, caption=具体的なCbCにおける CodeSegment] {src/type-cs.c}
212 212
213 CodeSegment \verb/getMinHeight/ は DataSegment \verb/Allocate/ と \verb/AkashaInfo/ を引数に取っている。 213 CodeSegment \verb/getMinHeight/ は DataSegment \verb/Allocate/ と \verb/AkashaInfo/ を引数に取っている。
214 現状は \verb/Context/ も継続のために渡しているが、本来ノーマルレベルからはアクセスできないために隠れているとする。 214 現状は \verb/Context/ も軽量継続のために渡しているが、本来ノーマルレベルからはアクセスできないために隠れているとする。
215 その場合、引数の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} $ となる。 215 その場合、引数の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} $ となる。
216 また、返り値は構文的には存在していないが、軽量継続で渡す値は $ Context $ である。 216 また、返り値は構文的には存在していないが、軽量継続で渡す値は $ Context $ である。
217 よって \verb/getMinHeight/ の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} \rightarrow Context $ となる。 217 よって \verb/getMinHeight/ の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} \rightarrow Context $ となる。
218 $ Context $ の型は Meta DataSegment なので、 subtype の S-ARROW より $Context $の上位型への変更ができる。 218 $ Context $ の型は Meta DataSegment なので、部分型の定義より $Context $の上位型への変更ができる。
219 219
220 $ \{ allocat; : Allocate , akashaInfo : AkahsaInfo\} $ を $X$と置いて、\verb/getMinHeignt/ を $ X \rightarrow X $ とする際の導出木は以下である。 220 % TODO: 図
221
222 \begin{prooftree}
223 \AxiomC{}
224 \RightLabel{S-REFL}
225 \UnaryInfC{$ X <: X $}
226 \AxiomC{}
227 \RightLabel{S-MDS}
228 \UnaryInfC{$ Conttext <: X$}
229 \RightLabel{S-ARROW}
230 \BinaryInfC{$ X \rightarrow Context <: X \rightarrow X$}
231 \end{prooftree}
232 221
233 返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。 222 返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。
234 プログラムによっては遷移先は確定しているために部分型にする必要性は無いが、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に包摂関係から具体型を導けば良い。 223 プログラムによっては遷移先は確定しているために部分型にせず具体的なものでも良い。
235 例えばコンパイル時に解決すればライブラリの静的リンク時実行コード生成が行なえ、ランタイム時に解決すればネットワークを経由するプログラムとの接続初期化に利用できる。 224 しかし、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に具体的な型を導けば良い。
236 例えば、プロトコルがバージョンを持つ場合に接続先のプログラムが利用しているプロトコルと互換性があるかの判断を Context どうしの部分型関係で判断できる。 225
237 226 また、stub のみに注目すると、stub は Context から具体的な DataSegment X を取り出す操作に相当し、部分型の関数の引数の仮定のような振舞いをする。
238 また、stub のみに注目すると、stub は Context から具体的なDataSegment X を取り出す操作に相当し、S-ARROWの左側の前提のような振舞いをする。 227 加えて、軽量継続する際に X の計算結果を Context に格納してから goto する部分を別の Meta CodeSegment として分離すると、部分型の返り値の仮定のような振舞いを行なう。
239 加えて、軽量継続する際に X の計算結果を Context に格納してから goto する部分を別の Meta CodeSegment として分離すると、S-ARROWの右側の前提のような振舞いを行なう。
240 このようにノーマルレベルの CodeSegment の先頭と末尾にメタ計算を接続することによってノーマルレベルの CodeSegment が型付けできる。 228 このようにノーマルレベルの CodeSegment の先頭と末尾にメタ計算を接続することによってノーマルレベルの CodeSegment が型付けできる。
241 型付けにDataSegment の集合としての Meta DataSegment が必須になるが、これは構造体として定義可能なためコンパイル時に生成することで CbC に組み込むことができる。 229 型付けを行なう際には DataSegment の集合としての Meta DataSegment が必須になるが、構造体としてコンパイル時に生成することで CbC に組み込むことができる。
242 230
243 なお、メタ計算に利用する Meta DataSegment と Meta DataSegment も同様に型付けできる。 231 なお、メタ計算に利用する Meta DataSegment と Meta DataSegment も同様に型付けできる。
232 Meta DataSegment の部分型に相当する Meta Meta DataSegment を定義してやれば良い。
244 ここで興味深いのはあるレベルの CodeSegment は同レベルの DataSegment において型付けされるが、一つ上の階層から見ると、下の階層のDataSegmentとして一貫して扱えることにある。 233 ここで興味深いのはあるレベルの CodeSegment は同レベルの DataSegment において型付けされるが、一つ上の階層から見ると、下の階層のDataSegmentとして一貫して扱えることにある。
245 このようにメタ計算を階層化することにより、メタ計算で拡張された計算に対しても他のメタ計算が容易に適用できる。 234 このようにメタ計算を階層化することにより、メタ計算で拡張された計算に対しても他のメタ計算が容易に適用できる。
246 235
247 % }}} 236 % }}}