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