Mercurial > hg > Papers > 2018 > nozomi-master
annotate paper/type.tex @ 88:2be864ed3a79
Add figure
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 Feb 2017 17:50:50 +0900 |
| parents | f3ea67a23cf6 |
| children | 54cf3b3153fe |
| rev | line source |
|---|---|
| 28 | 1 \chapter{ラムダ計算と型システム} |
| 2 \label{chapter:type} | |
| 77 | 3 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
4 \ref{chapter:akasha} 章では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
5 しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは断言しづらい。 |
| 34 | 6 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
7 そこで、 CbC の性質をより厳密に定義し、その上で証明を行なうことを考えた。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
8 CbC のプログラムを証明できる形に変換し、任意の回数の挿入に対しても性質が保証できるよう証明するのである。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
9 証明を行なう機構として注目したのが型システムである。 |
| 34 | 10 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
11 \ref{chapter:type}章では型システムの概要とCbCの型システムを提案する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
12 また、依存型を用いた実際の証明手法については~\ref{chapter:agda}章で解説する。 |
| 36 | 13 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
14 % {{{ 型システムとは |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
15 \section{型システムとは} |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
16 型システムとは、計算する値を分類することにでプログラムがある種の振舞いを行なわないことを保証する機構の事である\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
17 ある種の振舞いとはプログラム中の評価不可能な式や、言語として未定義な式などが当て嵌まる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
18 例えば、gcc や clang といったコンパイラは関数定義時に指定された引数の型と呼び出し時の値の型が異なる時に警告を出す。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
19 この警告は関数が受けつける範囲以外の値をプログラマが渡してしまった場合などに有効に働く。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
20 加えて、関数を定義する側も受け付ける値の範囲を限定できるため関数内部の処理を記述しやすい。 |
| 36 | 21 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
22 型システムで行なえることには以下のようなものが存在する。 |
| 36 | 23 |
| 37 | 24 \begin{itemize} |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
25 \item エラーの検出 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
26 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
27 文字列演算を行なう関数に整数を渡してしまったり、複雑な場合分けで境界条件を見落すなど、プログラマの不注意が型の不整合として表れる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
28 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
29 \item 抽象化 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
30 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
31 型は大規模プログラムの抽象化の単位にもなる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
32 例えば特定のデータ構造に対する処理をモジュール化し、パッケージングすることができる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
33 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
34 \item ドキュメント化 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
35 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
36 関数やモジュールの型を確認することにより、プログラムの理解の助けになる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
37 また、型はコンパイラが実行されるたびに検査されるため、常に最新の正しい情報を提供する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
38 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
39 \item 言語の安全性 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
40 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
41 例えばポインタを直接扱わないようメモリアクセスを抽象化し、データを破壊する可能性をプログラマに提供しないようにできる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
42 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
43 \item 効率性 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
44 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
45 そもそも、科学計算機における最初の型システムは Fortran~\ref{Backus:1978:HFI:960118.808380} などにおける整数と実数の算術式の区別だった。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
46 型の導入により、ソースからコンパイラがより最適化されたコードを生成できる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
47 |
| 37 | 48 \end{itemize} |
| 49 | |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
50 型システムには多くの定義が存在する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
51 型の表現能力には単純型や総称型、部分型などが存在する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
52 型付けにも動的型付けや静的型付けが存在し、どの型システムを採用するかは言語の設計に依存する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
53 例えば C言語では数値と文字を二項演算子 \verb/+/ で加算できるが、Haskell では加算することができない。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
54 これは Haskell が C言語よりも厳密な型システムを採用しているからである。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
55 具体的には Haskell は暗黙的な型変換を許さず、 C 言語は言語仕様として暗黙の型変換を持っている。 |
| 38 | 56 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
57 型システムを定義することはプログラミング言語がどのような特徴を持つかを決めることにも繋がる。 |
| 38 | 58 |
| 59 % }}} | |
| 34 | 60 |
| 41 | 61 % {{{ 単純型 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
62 \section{単純型} |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
63 単純型とは値の型と関数型のみで構成される型システムのことである。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
64 とある値はとある型に属する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
65 例えばリテラル \verb/true/ は \verb/bool/ 型に属するし、\verb/10/ は \verb/int/ 型に属する。 |
| 41 | 66 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
67 また、関数は値を取って値を返す処理と考えることで「型を取って型を返す型」 $ \rightarrow $ を持つ。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
68 例を上げると \verb/int/ を取って \verb/int/ を返す関数fは $ \text{int} \rightarrow \text{int} $ 型に属する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
69 型システムにおいて項が型付けされるのならば、関数が所望の型を持つ値以外に適用されることは無い。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
70 例を上げると、関数f が \verb/f(true)/ のように \verb/bool/ 型の値へと適用されることは無い。 |
| 40 | 71 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
72 関数型で複数の引数を表現することは「関数型を返す関数型」を考えることで実現できる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
73 例えば \verb/int/ と \verb/bool/ を取って \verb/string/ を返す型は $ \text{int} \rightarrow \text{bool} \rightarrow \text{string} $型に属する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
74 $ \rightarrow $ は右結合的であり、$ \text{int} \rightarrow \text{bool} \rightarrow \text{string} $ は $ \text{int} \rightarrow (\text{bool} \rightarrow \text{string}) $ と読む。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
75 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
76 % }}} |
| 40 | 77 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
78 % {{{ レコード型 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
79 \section{レコード型} |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
80 データ型には多くの種類が存在する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
81 ユーザが定義可能な型と区別するために言語が用意している型をプリミティブ型を呼ぶことにする。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
82 C 言語におけるプリミティブ型には \verb/int/ や \verb/char/ といった型がある。 |
| 40 | 83 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
84 C 言語にはプリミティブ型以外にも、ユーザが定義可能な型が存在する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
85 例えば構造体は複数の値を持つような値を取り扱うような型である。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
86 ここで構造体に対して「構造体型」という一つの型を用意した場合、複数の構造体の区別ができなくなる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
87 よって、構造体に型を付けるなら「何を内部に持っているのか」を覚えているような型でなくてはならない。 |
| 40 | 88 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
89 ここでレコード型という型を導入する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
90 レコード型は複数の型を持ちえる型であり、内部に持っている値にはユニークな名前がラベルとして付いている。 |
| 84 | 91 例えば「Intの変数x とIntの変数yを持つレコード型」は$ \{ x : Int , y : Bool\}$のように記述する。 |
| 92 C における構造体ではリストに対応する。 | |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
93 % TODO C の構造体 |
| 84 | 94 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
95 レコード型の値を構成する際には、内部に格納する値を全て与えることで構成できる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
96 % TODO C の構造体の初期化 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
97 レコード型から値を取り出す際にはラベル名を用いた射影を利用する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
98 C 言語では構造体の後に \verb/./ キーワードを付けた後にラベル名を指定する。 |
| 40 | 99 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
100 これで構造体に対する型付けができた。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
101 % }}} |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
102 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
103 % {{{ 部分型付け |
| 40 | 104 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
105 \section{部分型付け} |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
106 レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
107 しかし、関数が引数にレコードを取る場合、その型と完全に一致させる必要がある。 |
| 84 | 108 例えば $ \{ x : Int \} $ を引数に取る関数に対して $ \{ x : Int , y : Bool\}$ といった値を適用することができない。 |
| 109 しかし、直感的には関数の要求はフィールド $x $ が型 $Int$を持つことのみであり、その部分にのみ注目すると$ \{ x : Nat , y : Bool\}$ も要求に沿っている。 | |
| 41 | 110 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
111 ここで、部分型という型を導入する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
112 部分型は上記のような場合の項を許すように型付けを緩めることである。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
113 つまり型 $ S $ を持つ値が、型 $ T $ の値が期待される文脈において安全に利用できることを示す。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
114 この時、$ S $ を $ T $ の部分型と呼び、 $ S <: T $ と書く。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
115 これは型 $ S $ が型 $ T $よりも情報を多く持っていることを示しており、$S$は$T$の部分型である、と読む。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
116 $ S <: T $ の別の読み方として、型 $ T $ は型 $ S $ の上位型である、という読み方も存在する。 |
| 41 | 117 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
118 値に関する部分型は「とあるデータ型$T$よりも$S$の方が持っている情報が多いなら、$S$は$T$として振る舞っても良い」と定義できる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
119 フィールドの多い方が部分型となるのは名前に反するように思える。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
120 しかし、フィールドが多いほど制約が多くなり、表すことのできる集合の範囲は小さくなる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
121 集合の大きさで見ると明かにフィールドの多い方が小さいのである。 |
| 41 | 122 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
123 また、任意の型$T$に対して $ T <: T $ である。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
124 これは「$T$ は $ T$ として振る舞っても良い」ことを示しているので自明である。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
125 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
126 関数の部分型は以下のように定義できる。 |
| 40 | 127 |
| 128 \begin{prooftree} | |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
129 \AxiomC{$ T_1 <: S_1$} |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
130 \AxiomC{$ S_2 <: T_2$} |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
131 \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $} |
| 40 | 132 \end{prooftree} |
| 133 | |
| 88 | 134 これは「仮定$ T_1 <: S_1$ と$ S_2 <: T_2$ が成り立つ時、$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $ が成り立つ」と読む。 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
135 この部分型は引数の型と返り値の部分型について述べているために少々複雑である。 |
| 41 | 136 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
137 まず、引数部分に注目する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
138 上位型の関数の引数は $ T_1 $ である。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
139 引数に対する仮定は部分型関係$ T_1 <: S_1$である。 |
| 88 | 140 これは上位型関数の引数が部分型となっており、大きい。 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
141 そして導かれる部分型の引数の型は $ S_1$ である。 |
| 88 | 142 つまり、「小さい型 $S_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} | |
| 41 | 152 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
153 次に返り値部分に注目する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
154 上位型の関数の返り値は $T_2$ である。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
155 返り値に対する仮定は部分型関係$ S_2 <: T_2$であり、引数と逆になっている。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
156 これは上位型関数の方が上位型となっており、小さい。 |
| 88 | 157 つまり、「大きい型 $ S_2 $ を返す関数は、小さい型 $T_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} | |
| 41 | 167 |
| 168 % }}} | |
| 40 | 169 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
170 % {{{ 部分型と Continuation based C |
| 31 | 171 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
172 \section{部分型と Continuation based C} |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
173 部分型を用いて Conituation based C の型システムを定義していく。 |
| 31 | 174 |
| 84 | 175 まず、DataSegment の型を定義する。 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
176 DataSegment 自体はCの構造体によって定義されているため、レコード型として考えることができる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
177 例えばリスト~\ref{src:akasha-context}に示していた DataSegment の一つに注目する(リスト~\ref{src:type-ds})。 |
| 31 | 178 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
179 \lstinputlisting[label=src:type-ds, caption=akashaContext の DataSegment である AkashaInfo] {src/type-ds.h} |
| 84 | 180 この AkashaInfo は $ \{ minHeight : unsigned\; int , maxHeight : unsigned \; int, akashaNode : AkashaNode*\}$ 型を持つ。 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
181 CodeSegment は DataSegment を引数に取るため、DataSegment の型は CodeSegment が要求する最低限の制約をまとめたものと言える。 |
| 31 | 182 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
183 次に Meta DataSegment について考える。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
184 Meta DataSegment はプログラムに出現する DataSegment の共用体であった。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
185 これを DataSegment の構造体に変更する。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
186 こうすることにより、 Meta DataSegment はプログラム中に出現する DataSegment を必ず持つため、Meta DataSegment は任意の DataSegment の部分型となる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
187 もしくは各 DataSegment の全てのフィールドを含むような1つの構造体でも良い。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
188 第~\ref{chapter:cbc-type}章における Meta DataSegment はそのように定義している。 |
| 84 | 189 なお、GearsOSでは DataSegment の共用体をプログラムで必要な数だけ持つ実装になっている。 |
| 32 | 190 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
191 具体的な CbC における Meta DataSegment であるContext (リスト~\ref{src:type-mds})は、 DataSegment の集合を値として持っているために明らかに DataSegment よりも多くの情報を持っている。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
192 \lstinputlisting[label=src:type-mds, caption=CbC の Meta DataSegment である Context] {src/type-mds.h} |
| 39 | 193 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
194 部分型として定義するなら以下のような定義となる。 |
| 39 | 195 |
| 196 \begin{definition} | |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
197 Meta DataSegment の定義 |
| 39 | 198 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
199 \begin{align*} |
| 88 | 200 \text{Meta DataSegment} <: \text{プログラム中の任意のDataSegment} |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
201 \end{align*} |
| 39 | 202 \end{definition} |
| 203 | |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
204 次に CodeSegment の型について考える。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
205 CodeSegment は DataSegment を DataSegment へと移す関数型とする。 |
| 39 | 206 |
| 207 \begin{definition} | |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
208 CodeSegment の定義 |
| 39 | 209 |
| 210 \begin{align*} | |
| 88 | 211 \text{DataSegment} \rightarrow \text{DataSegment} |
| 39 | 212 \end{align*} |
| 213 \end{definition} | |
| 32 | 214 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
215 そして Meta CodeSegmentは Meta DataSegment を Meta DataSegment へと移す関数となる。 |
| 42 | 216 |
| 217 \begin{definition} | |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
218 Meta CodeSegment の定義 |
| 42 | 219 |
| 220 \begin{align*} | |
| 88 | 221 \text{Meta DataSegment} \rightarrow \text{Meta DataSegment} |
| 42 | 222 \end{align*} |
| 223 \end{definition} | |
| 224 | |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
225 ここで具体的なコード(リスト~\ref{src:type-cs})と比較してみる。 |
| 42 | 226 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
227 \lstinputlisting[label=src:type-cs, caption=具体的なCbCにおける CodeSegment] {src/type-cs.c} |
| 42 | 228 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
229 CodeSegment \verb/getMinHeight/ は DataSegment \verb/Allocate/ と \verb/AkashaInfo/ を引数に取っている。 |
| 84 | 230 現状は \verb/Context/ も軽量継続のために渡しているが、本来ノーマルレベルからはアクセスできないために隠れているとする。 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
231 その場合、引数の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} $ となる。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
232 また、返り値は構文的には存在していないが、軽量継続で渡す値は $ Context $ である。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
233 よって \verb/getMinHeight/ の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} \rightarrow Context $ となる。 |
| 88 | 234 $ Context $ の型は Meta DataSegment なので、部分型の定義より $Context $の上位型への変更ができる(図~\ref{fig:cbc-subtype})。 |
| 43 | 235 |
| 88 | 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} | |
| 43 | 243 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
244 返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。 |
| 84 | 245 プログラムによっては遷移先は確定しているために部分型にせず具体的なものでも良い。 |
| 246 しかし、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に具体的な型を導けば良い。 | |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
247 |
| 84 | 248 また、stub のみに注目すると、stub は Context から具体的な DataSegment X を取り出す操作に相当し、部分型の関数の引数の仮定のような振舞いをする。 |
| 249 加えて、軽量継続する際に X の計算結果を Context に格納してから goto する部分を別の Meta CodeSegment として分離すると、部分型の返り値の仮定のような振舞いを行なう。 | |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
250 このようにノーマルレベルの CodeSegment の先頭と末尾にメタ計算を接続することによってノーマルレベルの CodeSegment が型付けできる。 |
| 84 | 251 型付けを行なう際には DataSegment の集合としての Meta DataSegment が必須になるが、構造体としてコンパイル時に生成することで CbC に組み込むことができる。 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
252 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
253 なお、メタ計算に利用する Meta DataSegment と Meta DataSegment も同様に型付けできる。 |
| 84 | 254 Meta DataSegment の部分型に相当する Meta Meta DataSegment を定義してやれば良い。 |
|
83
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
255 ここで興味深いのはあるレベルの CodeSegment は同レベルの DataSegment において型付けされるが、一つ上の階層から見ると、下の階層のDataSegmentとして一貫して扱えることにある。 |
|
c0199291c58e
Add simple/sub type description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
78
diff
changeset
|
256 このようにメタ計算を階層化することにより、メタ計算で拡張された計算に対しても他のメタ計算が容易に適用できる。 |
| 43 | 257 |
| 258 % }}} |