Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/type.tex @ 88:2be864ed3a79

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add figure
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 17:50:50 +0900
parents f3ea67a23cf6
children 54cf3b3153fe
comparison
equal deleted inserted replaced
87:21cc0181b4cc 88:2be864ed3a79
129 \AxiomC{$ T_1 <: S_1$} 129 \AxiomC{$ T_1 <: S_1$}
130 \AxiomC{$ S_2 <: T_2$} 130 \AxiomC{$ S_2 <: T_2$}
131 \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $} 131 \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $}
132 \end{prooftree} 132 \end{prooftree}
133 133
134 これは「仮定{$ T_1 <: S_1$ と$ S_2 <: T_2$ が成り立つ時、$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $ が成り立つ」と読む。 134 これは「仮定$ T_1 <: S_1$ と$ S_2 <: T_2$ が成り立つ時、$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $ が成り立つ」と読む。
135 この部分型は引数の型と返り値の部分型について述べているために少々複雑である。 135 この部分型は引数の型と返り値の部分型について述べているために少々複雑である。
136 136
137 まず、引数部分に注目する。 137 まず、引数部分に注目する。
138 上位型の関数の引数は $ T_1 $ である。 138 上位型の関数の引数は $ T_1 $ である。
139 引数に対する仮定は部分型関係$ T_1 <: S_1$である。 139 引数に対する仮定は部分型関係$ T_1 <: S_1$である。
140 これは上位型関数の方が部分型となっており、大きい。 140 これは上位型関数の引数が部分型となっており、大きい。
141 そして導かれる部分型の引数の型は $ S_1$ である。 141 そして導かれる部分型の引数の型は $ S_1$ である。
142 つまり、「大きい型 $T_1$を要求する関数は小さい型 $S_1$ を要求する関数として使って良い」ということである。 142 つまり、「小さい型 $S_1$を要求する関数は大きな型 $S_1$ を受けつける」と言える。
143 具体的には $ T_1 $ のレコードをいくつか削って $S_1$まで小さくすれば良い。 143 具体的には $ T_1 $ のレコードをいくつか削って $S_1$まで小さくすれば良いのである(図~\ref{fig:subtype-arg})。
144
145 \begin{figure}[htbp]
146 \begin{center}
147 \includegraphics[width=450pt]{fig/subtype-arg.pdf}
148 \caption{部分型の関数型と引数の型}
149 \label{fig:subtype-arg}
150 \end{center}
151 \end{figure}
144 152
145 次に返り値部分に注目する。 153 次に返り値部分に注目する。
146 上位型の関数の返り値は $T_2$ である。 154 上位型の関数の返り値は $T_2$ である。
147 返り値に対する仮定は部分型関係$ S_2 <: T_2$であり、引数と逆になっている。 155 返り値に対する仮定は部分型関係$ S_2 <: T_2$であり、引数と逆になっている。
148 これは上位型関数の方が上位型となっており、小さい。 156 これは上位型関数の方が上位型となっており、小さい。
149 つまり、「小さい型 $ T_2 $ を返す関数は、大きい型 $S_2$ を返す関数として使っても良い」ということである。 157 つまり、「大きい型 $ S_2 $ を返す関数は、小さい型 $T_2$ を返す関数として使っても良い」ということである。
150 具体的には $ T_2 $ のレコードが $S_2$ に全て格納できることを意味する。 158 具体的にはこちらも $ S_2 $ のレコードを削って $T_2$ と同じになるまで小さくなるようにすれば良い(図~\ref{fig:subtype-return})。
159
160 \begin{figure}[htbp]
161 \begin{center}
162 \includegraphics[width=450pt]{fig/subtype-return.pdf}
163 \caption{部分型の関数型と返り値の型}
164 \label{fig:subtype-return}
165 \end{center}
166 \end{figure}
151 167
152 % }}} 168 % }}}
153 169
154 % {{{ 部分型と Continuation based C 170 % {{{ 部分型と Continuation based C
155 171
179 195
180 \begin{definition} 196 \begin{definition}
181 Meta DataSegment の定義 197 Meta DataSegment の定義
182 198
183 \begin{align*} 199 \begin{align*}
184 Meta \; DataSegment <: プログラム中の任意のDataSegment 200 \text{Meta DataSegment} <: \text{プログラム中の任意のDataSegment}
185 \end{align*} 201 \end{align*}
186 \end{definition} 202 \end{definition}
187 203
188 次に CodeSegment の型について考える。 204 次に CodeSegment の型について考える。
189 CodeSegment は DataSegment を DataSegment へと移す関数型とする。 205 CodeSegment は DataSegment を DataSegment へと移す関数型とする。
190 206
191 \begin{definition} 207 \begin{definition}
192 CodeSegment の定義 208 CodeSegment の定義
193 209
194 \begin{align*} 210 \begin{align*}
195 DataSegment \rightarrow DataSegment 211 \text{DataSegment} \rightarrow \text{DataSegment}
196 \end{align*} 212 \end{align*}
197 \end{definition} 213 \end{definition}
198 214
199 そして Meta CodeSegmentは Meta DataSegment を Meta DataSegment へと移す関数となる。 215 そして Meta CodeSegmentは Meta DataSegment を Meta DataSegment へと移す関数となる。
200 216
201 \begin{definition} 217 \begin{definition}
202 Meta CodeSegment の定義 218 Meta CodeSegment の定義
203 219
204 \begin{align*} 220 \begin{align*}
205 Meta \; DataSegment \rightarrow Meta \; DataSegment 221 \text{Meta DataSegment} \rightarrow \text{Meta DataSegment}
206 \end{align*} 222 \end{align*}
207 \end{definition} 223 \end{definition}
208 224
209 ここで具体的なコード(リスト~\ref{src:type-cs})と比較してみる。 225 ここで具体的なコード(リスト~\ref{src:type-cs})と比較してみる。
210 226
213 CodeSegment \verb/getMinHeight/ は DataSegment \verb/Allocate/ と \verb/AkashaInfo/ を引数に取っている。 229 CodeSegment \verb/getMinHeight/ は DataSegment \verb/Allocate/ と \verb/AkashaInfo/ を引数に取っている。
214 現状は \verb/Context/ も軽量継続のために渡しているが、本来ノーマルレベルからはアクセスできないために隠れているとする。 230 現状は \verb/Context/ も軽量継続のために渡しているが、本来ノーマルレベルからはアクセスできないために隠れているとする。
215 その場合、引数の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} $ となる。 231 その場合、引数の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} $ となる。
216 また、返り値は構文的には存在していないが、軽量継続で渡す値は $ Context $ である。 232 また、返り値は構文的には存在していないが、軽量継続で渡す値は $ Context $ である。
217 よって \verb/getMinHeight/ の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} \rightarrow Context $ となる。 233 よって \verb/getMinHeight/ の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} \rightarrow Context $ となる。
218 $ Context $ の型は Meta DataSegment なので、部分型の定義より $Context $の上位型への変更ができる。 234 $ Context $ の型は Meta DataSegment なので、部分型の定義より $Context $の上位型への変更ができる(図~\ref{fig:cbc-subtype})。
219 235
220 % TODO: 図 236 \begin{figure}[htbp]
237 \begin{center}
238 \includegraphics[width=450pt]{fig/cbc-subtype.pdf}
239 \caption{CodeSegment の部分型付け}
240 \label{fig:cbc-subtype}
241 \end{center}
242 \end{figure}
221 243
222 返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。 244 返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。
223 プログラムによっては遷移先は確定しているために部分型にせず具体的なものでも良い。 245 プログラムによっては遷移先は確定しているために部分型にせず具体的なものでも良い。
224 しかし、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に具体的な型を導けば良い。 246 しかし、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に具体的な型を導けば良い。
225 247