\chapter{ラムダ計算と型システム}
\label{chapter:type}
\ref{chapter:cbc} では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
しかし、さらに多くの要素を検証したり無限回の挿入を検証するには状態の抽象化や CbC 側に記号実行の機構を組み込んだり証明を行なう必要がある。
CbC は直接自身を証明する機構が存在しない。
プログラムの性質を証明するには CbC の形式的な定義が必須となる。
\ref{chapter:type} 章ではCbC の項の形式的な定義の一つとして、部分型を用いて CbC の CodeSegment と DataSegment が定義できることを示していく。
また、型システムの別の利用方法として命題が型で表現できる Curry-Howard 対応を利用した証明が存在するが、その利用方法については\ref{chapter:agda}章で述べる。

% {{{ 型システムとは
\section{型システムとは}
型システムとは、計算する値を分類することにでプログラムがある種の振舞いを行なわないことを保証する機構の事である\cite{Pierce:2002:TPL:509043}\cite{pierce2013型システム入門プログラミング言語と型の理論}。
ある種の振舞いとはプログラム中の評価不可能な式や、言語として未定義な式などが当て嵌まる。
例えば、gcc や clang といったコンパイラは関数定義時に指定された引数の型と呼び出し時の値の型が異なる時に警告を出す。
% TODO: C の warning?
この警告は関数が受けつける範囲以外の値をプログラマが渡してしまった場合などに有効に働く。
加えて、関数を定義する側も受け付ける値の範囲を限定できるため関数内部の処理を記述しやすい。

型システムで行なえることには以下のようなものが存在する。

\begin{itemize}
    \item エラーの検出

        文字列演算を行なう関数に整数を渡してしまったり、データの単位を間違えてしまったり、複雑な場合分けで境界条件を見落すなど、プログラマの不注意が型の不整合となって早期に指摘できる。
        この指摘できる詳細さは、型システムの表現力とプログラムの内容に依存する。
        多用なデータ構造を扱うプログラム(コンパイラのような記号処理アプリケーションなど)は数値計算のような数種類の単純な型しか使わないプログラムよりも型検査器から受けられる恩恵が大きい。
        他にも、ある種のプログラムにとっては型は保守のためのツールともなる。
        複雑なデータ構造を変更する時、その構造に関連するソースコードを型検査器は明らかにしてくれる。

    \itemize 抽象化

        型は大規模プログラムの抽象化の単位にもなる。
        例えば特定のデータ構造に対する処理をモジュール化し、パッケージングすることができる。
        モジュール化されたデータ構造は厳格に定義されたインターフェースを経由して呼び出すことになる。
        このインターフェースは利用する側に取っては呼び出しの規約となり、実装する側にとってはモジュールの要約となる。

    \itemize ドキュメント化

        型はプログラムを理解する際にも有用である。
        関数やモジュールの型を確認することにより、どのデータを対象としているのかといった情報が手に入る。
        また、型はコンパイラが実行されるために検査されるため、コメントに埋め込まれた情報と異なり常に正しい情報を提供する。

    \itemize 言語の安全性

        安全性のの定義は言語によって異なるが、型はデータの抽象化によってある種の安全性を確保できる。
        例えば、プログラマは配列をソートする関数があった場合、与えられた配列のみがソートされ、他のデータには影響が無いことを期待するだろう。
        しかし、低水準言語ではメモリを直接扱えるため、予想された処理の範囲を越えてデータを破壊する可能性がある。
        より安全な言語ではメモリアクセスが抽象化し、データを破壊する可能性をプログラマに提供しないという選択肢がある。

    \itemize 効率性

        そもそも、科学計算機における最初の型システムは Fortran などにおける式の区別であった。% TODO ref fortran
        整数の算術式と実数の算術式を区別し、数値計算の効率化を測るために導入されたのである。
        型の導入により、コンパイラはプリミティブな演算とは異なる表現を用い、実行コードを生成する時に適切な機械語表現を行なえるようになった。
        昨今の高性能コンパイラでは最適化とコード生成のフェーズにおいて型検査器が収集する情報を多く利用している。

\end{itemize}

型システムの定義には多くの定義が存在する。
型の表現能力には単純型や総称型、部分型などが存在し、動的型付けや静的型付けなど、言語によってどの型システムを採用するかは言語の設計に依存する。
例えば C言語では数値と文字を二項演算子 \verb/+/ で加算できるが、Haskell では加算することができない。
これは Haskell が C言語よりも厳密な型システムを採用しているからである。
具体的には Haskell は暗黙的な型変換を許さず、 C 言語は言語仕様として暗黙の型変換を持っている。

型システムを定義することはプログラミング言語がどのような特徴を持つか決めることにも繋がる。

% }}}

\section{型なしラムダ計算}


\section{単純型付きラムダ計算}
\section{部分型付け}
\section{部分型と Continuation based C}