Mercurial > hg > Papers > 2018 > nozomi-master

annotate paper/type.tex @ 30:55f67e448dcc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add type system description
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 26 Jan 2017 11:03:51 +0900
parents 36ce493604fb
children 9dc9c50a28bd
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
28
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \chapter{ラムダ計算と型システム}
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 \label{chapter:type}
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 \ref{chapter:cbc} では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 しかし、さらに多くの要素を検証したり無限回の挿入を検証するには状態の抽象化や CbC 側に記号実行の機構を組み込んだり証明を行なう必要がある。
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 CbC は直接自身を証明する機構が存在しない。
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 プログラムの性質を証明するには CbC の形式的な定義が必須となる。
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 \ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment が定義できることを示していく。
30
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
8 また、型システムの別の利用方法として命題が型で表現できる Curry-Howard 対応を利用した証明が存在するが、その利用方法については\ref{chapter:agda}章で述べる。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
9
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
10 % {{{ 型システムとは
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
11 \section{型システムとは}
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
12 型システムとは、計算する値を分類することにでプログラムがある種の振舞いを行なわないことを保証する機構の事である\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
13 ある種の振舞いとはプログラム中の評価不可能な式や、言語として未定義な式などが当て嵌まる。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
14 例えば、gcc や clang といったコンパイラは関数定義時に指定された引数の型と呼び出し時の値の型が異なる時に警告を出す。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
15 % TODO: C の warning?
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
16 この警告は関数が受けつける範囲以外の値をプログラマが渡してしまった場合などに有効に働く。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
17 加えて、関数を定義する側も受け付ける値の範囲を限定できるため関数内部の処理を記述しやすい。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
18
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
19 型システムで行なえることには以下のようなものが存在する。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
20
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
21 \begin{itemize}
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
22 \item エラーの検出
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
23
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
24 文字列演算を行なう関数に整数を渡してしまったり、データの単位を間違えてしまったり、複雑な場合分けで境界条件を見落すなど、プログラマの不注意が型の不整合となって早期に指摘できる。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
25 この指摘できる詳細さは、型システムの表現力とプログラムの内容に依存する。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
26 多用なデータ構造を扱うプログラム(コンパイラのような記号処理アプリケーションなど)は数値計算のような数種類の単純な型しか使わないプログラムよりも型検査器から受けられる恩恵が大きい。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
27 他にも、ある種のプログラムにとっては型は保守のためのツールともなる。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
28 複雑なデータ構造を変更する時、その構造に関連するソースコードを型検査器は明らかにしてくれる。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
29
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
30 \itemize 抽象化
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
31
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
32 型は大規模プログラムの抽象化の単位にもなる。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
33 例えば特定のデータ構造に対する処理をモジュール化し、パッケージングすることができる。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
34 モジュール化されたデータ構造は厳格に定義されたインターフェースを経由して呼び出すことになる。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
35 このインターフェースは利用する側に取っては呼び出しの規約となり、実装する側にとってはモジュールの要約となる。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
36
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
37 \itemize ドキュメント化
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
38
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
39 型はプログラムを理解する際にも有用である。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
40 関数やモジュールの型を確認することにより、どのデータを対象としているのかといった情報が手に入る。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
41 また、型はコンパイラが実行されるために検査されるため、コメントに埋め込まれた情報と異なり常に正しい情報を提供する。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
42
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
43 \itemize 言語の安全性
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
44
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
45 安全性のの定義は言語によって異なるが、型はデータの抽象化によってある種の安全性を確保できる。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
46 例えば、プログラマは配列をソートする関数があった場合、与えられた配列のみがソートされ、他のデータには影響が無いことを期待するだろう。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
47 しかし、低水準言語ではメモリを直接扱えるため、予想された処理の範囲を越えてデータを破壊する可能性がある。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
48 より安全な言語ではメモリアクセスが抽象化し、データを破壊する可能性をプログラマに提供しないという選択肢がある。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
49
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
50 \itemize 効率性
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
51
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
52 そもそも、科学計算機における最初の型システムは Fortran などにおける式の区別であった。% TODO ref fortran
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
53 整数の算術式と実数の算術式を区別し、数値計算の効率化を測るために導入されたのである。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
54 型の導入により、コンパイラはプリミティブな演算とは異なる表現を用い、実行コードを生成する時に適切な機械語表現を行なえるようになった。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
55 昨今の高性能コンパイラでは最適化とコード生成のフェーズにおいて型検査器が収集する情報を多く利用している。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
56
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
57 \end{itemize}
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
58
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
59 型システムの定義には多くの定義が存在する。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
60 型の表現能力には単純型や総称型、部分型などが存在し、動的型付けや静的型付けなど、言語によってどの型システムを採用するかは言語の設計に依存する。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
61 例えば C言語では数値と文字を二項演算子 \verb/+/ で加算できるが、Haskell では加算することができない。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
62 これは Haskell が C言語よりも厳密な型システムを採用しているからである。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
63 具体的には Haskell は暗黙的な型変換を許さず、 C 言語は言語仕様として暗黙の型変換を持っている。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
64
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
65 型システムを定義することはプログラミング言語がどのような特徴を持つか決めることにも繋がる。
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
66
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
67 % }}}
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
68
55f67e448dcc Add type system description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
69 \section{型なしラムダ計算}
28
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
71
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 \section{単純型付きラムダ計算}
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 \section{部分型付け}
36ce493604fb Add akasha result
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 \section{部分型と Continuation based C}