\chapter{ラムダ計算と型システム}
\label{chapter:type}

\ref{chapter:akasha} 章では CbC のモデル検査的検証アプローチとして、akasha を用いた有限の要素数の挿入時の仕様の検証を行なった。
しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは断言しづらい。

そこで、 CbC の性質をより厳密に定義し、その上で証明を行なうことを考えた。
CbC のプログラムを証明できる形に変換し、任意の回数の挿入に対しても性質が保証できるよう証明するのである。
証明を行なう機構として注目したのが型システムである。

\ref{chapter:type}章では型システムの概要とCbCの型システムを提案する。
また、依存型を用いた実際の証明手法については~\ref{chapter:agda}章で解説する。

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

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

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

        文字列演算を行なう関数に整数を渡してしまったり、複雑な場合分けで境界条件を見落すなど、プログラマの不注意が型の不整合として表れる。

    \item 抽象化

        型は大規模プログラムの抽象化の単位にもなる。
        例えば特定のデータ構造に対する処理をモジュール化し、パッケージングすることができる。

    \item ドキュメント化

        関数やモジュールの型を確認することにより、プログラムの理解の助けになる。
        また、型はコンパイラが実行されるたびに検査されるため、常に最新の正しい情報を提供する。

    \item 言語の安全性

        例えばポインタを直接扱わないようメモリアクセスを抽象化し、データを破壊する可能性をプログラマに提供しないようにできる。

    \item 効率性

        そもそも、科学計算機における最初の型システムは Fortran~\cite{Backus:1978:HFI:960118.808380} などにおける整数と実数の算術式の区別だった。
        型の導入により、ソースからコンパイラがより最適化されたコードを生成できる。

\end{itemize}

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

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

% }}}

% {{{ 単純型
\section{単純型}
単純型とは値の型と関数型のみで構成される型システムのことである。
とある値はとある型に属する。
例えばリテラル \verb/true/ は \verb/bool/ 型に属するし、\verb/10/ は \verb/int/ 型に属する。

また、関数は値を取って値を返す処理と考えることで「型を取って型を返す型」 $ \rightarrow $ を持つ。
例を上げると \verb/int/ を取って \verb/int/ を返す関数fは $ \text{int} \rightarrow \text{int} $ 型に属する。
型システムにおいて項が型付けされるのならば、関数が所望の型を持つ値以外に適用されることは無い。
例を上げると、関数f が \verb/f(true)/ のように \verb/bool/ 型の値へと適用されることは無い。

関数型で複数の引数を表現することは「関数型を返す関数型」を考えることで実現できる。
例えば \verb/int/ と \verb/bool/ を取って \verb/string/ を返す型は $ \text{int} \rightarrow \text{bool} \rightarrow \text{string} $型に属する。
$ \rightarrow $ は右結合的であり、$ \text{int} \rightarrow \text{bool} \rightarrow \text{string} $ は $ \text{int} \rightarrow (\text{bool} \rightarrow \text{string}) $ と読む。

% }}}

% {{{ レコード型
\section{レコード型}
データ型には多くの種類が存在する。
ユーザが定義可能な型と区別するために言語が用意している型をプリミティブ型を呼ぶことにする。
C 言語におけるプリミティブ型には \verb/int/ や \verb/char/ といった型がある。

C 言語にはプリミティブ型以外にも、ユーザが定義可能な型が存在する。
例えば構造体は複数の値を持つような値を取り扱うような型である。
ここで構造体に対して「構造体型」という一つの型を用意した場合、複数の構造体の区別ができなくなる。
よって、構造体に型を付けるなら「何を内部に持っているのか」を覚えているような型でなくてはならない。

ここでレコード型という型を導入する。
レコード型は複数の型を持ちえる型であり、内部に持っている値にはユニークな名前がラベルとして付いている。
例えば「Intの変数x とIntの変数yを持つレコード型」は$ \{ x : Int , y : Bool\}$のように記述する。
C における構造体ではリスト~\ref{src:struct}にのソースコードに対応する。

\lstinputlisting[label=src:struct, caption=C におけるレコード型である構造体の定義] {src/struct.c}

レコード型の値を構成する際には、内部に格納する値を全て与えることで構成できる。
C 言語ならばフィールドの値を \verb/{}/ 内部に \verb/,/ 区切りで与えることで構造体を構成できる(リスト~\ref{src:struct-init})。
\lstinputlisting[label=src:struct-init, caption=C 言語の構造体の初期化] {src/struct-init.c}

レコード型から値を取り出す際にはラベル名を用いた射影を利用する。
C 言語では構造体の後に \verb/./ キーワードを付けた後にラベル名を指定する。

これで構造体に対する型付けができた。
% }}}

% {{{ 部分型付け

\section{部分型付け}
レコードを用いることで複数の値を一つの値としてまとめて扱うことができる。
しかし、関数が引数にレコードを取る場合、その型と完全に一致させる必要がある。
例えば $ \{ x : Int \} $ を引数に取る関数に対して $ \{ x : Int , y : Bool\}$ といった値を適用することができない。
しかし、直感的には関数の要求はフィールド $x $ が型 $Int$を持つことのみであり、その部分にのみ注目すると$ \{ x : Nat , y : Bool\}$ も要求に沿っている。

ここで、部分型という型を導入する。
部分型は上記のような場合の項を許すように型付けを緩めることである。
つまり型 $ S $ を持つ値が、型 $ T $ の値が期待される文脈において安全に利用できることを示す。
この時、$ S $ を $ T $ の部分型と呼び、 $ S <: T $ と書く。
これは型 $ S $ が型 $ T $よりも情報を多く持っていることを示しており、$S$は$T$の部分型である、と読む。
$ S <: T $ の別の読み方として、型 $ T $ は型 $ S $ の上位型である、という読み方も存在する。

値に関する部分型は「とあるデータ型$T$よりも$S$の方が持っている情報が多いなら、$S$は$T$として振る舞っても良い」と定義できる。
フィールドの多い方が部分型となるのは名前に反するように思える。
しかし、フィールドが多いほど制約が多くなり、表すことのできる集合の範囲は小さくなる。
集合の大きさで見ると明かにフィールドの多い方が小さいのである。

また、任意の型$T$に対して $ T <: T $ である。
これは「$T$ は $ T$ として振る舞っても良い」ことを示しているので自明である。

関数の部分型は以下のように定義できる。

\begin{prooftree}
    \AxiomC{$ T_1 <: S_1$}
    \AxiomC{$ S_2 <: T_2$}
    \BinaryInfC{$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $}
\end{prooftree}

これは「仮定$ T_1 <: S_1$ と$ S_2 <: T_2$ が成り立つ時、$ S_1 \rightarrow S_2 <: T_1 \rightarrow T_2 $ が成り立つ」と読む。
この部分型は引数の型と返り値の部分型について述べているために少々複雑である。

まず、引数部分に注目する。
上位型の関数の引数は $ T_1 $ である。
引数に対する仮定は部分型関係$ T_1 <: S_1$である。
これは上位型関数の引数が部分型となっており、大きい。
そして導かれる部分型の引数の型は $ S_1$ である。
つまり、「小さい型 $S_1$を要求する関数は大きな型 $S_1$ を受けつける」と言える。
具体的には $ T_1 $ のレコードをいくつか削って $S_1$まで小さくすれば良いのである(図~\ref{fig:subtype-arg})。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[width=450pt]{fig/subtype-arg.pdf}
        \caption{部分型の関数型と引数の型}
        \label{fig:subtype-arg}
    \end{center}
\end{figure}

次に返り値部分に注目する。
上位型の関数の返り値は $T_2$ である。
返り値に対する仮定は部分型関係$ S_2 <: T_2$であり、引数と逆になっている。
これは上位型関数の方が上位型となっており、小さい。
つまり、「大きい型 $ S_2 $ を返す関数は、小さい型 $T_2$ を返す関数として使っても良い」ということである。
具体的にはこちらも $ S_2 $ のレコードを削って $T_2$ と同じになるまで小さくなるようにすれば良い(図~\ref{fig:subtype-return})。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[width=450pt]{fig/subtype-return.pdf}
        \caption{部分型の関数型と返り値の型}
        \label{fig:subtype-return}
    \end{center}
\end{figure}

% }}}

% {{{ 部分型と Continuation based C

\section{部分型と Continuation based C}
部分型を用いて Conituation based C の型システムを定義していく。

まず、DataSegment の型を定義する。
DataSegment 自体はCの構造体によって定義されているため、レコード型として考えることができる。
例えばリスト~\ref{src:akasha-context}に示していた DataSegment の一つに注目する(リスト~\ref{src:type-ds})。

\lstinputlisting[label=src:type-ds, caption=akashaContext の DataSegment である AkashaInfo] {src/type-ds.h}
この AkashaInfo は $ \{ minHeight : unsigned\; int , maxHeight : unsigned \; int, akashaNode : AkashaNode*\}$ 型を持つ。
CodeSegment は DataSegment を引数に取るため、DataSegment の型は CodeSegment が要求する最低限の制約をまとめたものと言える。

次に Meta DataSegment について考える。
Meta DataSegment はプログラムに出現する DataSegment の共用体であった。
これを DataSegment の構造体に変更する。
こうすることにより、 Meta DataSegment はプログラム中に出現する DataSegment を必ず持つため、Meta DataSegment は任意の DataSegment の部分型となる。
もしくは各 DataSegment の全てのフィールドを含むような1つの構造体でも良い。
第~\ref{chapter:cbc-type}章における Meta DataSegment はそのように定義している。
なお、GearsOSでは DataSegment の共用体をプログラムで必要な数だけ持つ実装になっている。

具体的な CbC における Meta DataSegment であるContext (リスト~\ref{src:type-mds})は、 DataSegment の集合を値として持っているために明らかに DataSegment よりも多くの情報を持っている。
\lstinputlisting[label=src:type-mds, caption=CbC の Meta DataSegment である Context] {src/type-mds.h}

部分型として定義するなら以下のような定義となる。

\begin{definition}
    Meta DataSegment の定義

    \begin{align*}
        \text{Meta DataSegment} <: \text{プログラム中の任意のDataSegment}
    \end{align*}
\end{definition}

次に CodeSegment の型について考える。
CodeSegment は DataSegment を DataSegment へと移す関数型とする。

\begin{definition}
    CodeSegment の定義

    \begin{align*}
        \text{DataSegment} \rightarrow \text{DataSegment}
    \end{align*}
\end{definition}

そして Meta CodeSegmentは Meta DataSegment を Meta DataSegment へと移す関数となる。

\begin{definition}
    Meta CodeSegment の定義

    \begin{align*}
        \text{Meta DataSegment} \rightarrow \text{Meta DataSegment}
    \end{align*}
\end{definition}

ここで具体的なコード(リスト~\ref{src:type-cs})と比較してみる。

\lstinputlisting[label=src:type-cs, caption=具体的なCbCにおける CodeSegment] {src/type-cs.c}

CodeSegment \verb/getMinHeight/ は DataSegment \verb/Allocate/ と \verb/AkashaInfo/ を引数に取っている。
現状は \verb/Context/ も軽量継続のために渡しているが、本来ノーマルレベルからはアクセスできないために隠れているとする。
その場合、引数の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\}  $ となる。
また、返り値は構文的には存在していないが、軽量継続で渡す値は $ Context $ である。
よって \verb/getMinHeight/ の型は $ \{ allocate : Allocate , akashaInfo : AkahsaInfo\} \rightarrow Context $ となる。
$ Context $ の型は Meta DataSegment なので、部分型の定義より $Context $の上位型への変更ができる(図~\ref{fig:cbc-subtype})。

\begin{figure}[htbp]
    \begin{center}
        \includegraphics[width=450pt]{fig/cbc-subtype.pdf}
        \caption{CodeSegment の部分型付け}
        \label{fig:cbc-subtype}
    \end{center}
\end{figure}

返り値部分を部分型として定義することにより、軽量継続先が上位型であればどの CodeSegment へと遷移しても良い。
プログラムによっては遷移先は確定しているために部分型にせず具体的なものでも良い。
しかし、メタ計算やライブラリなどの遷移先が不定の場合は一度部分型として確定し、その後コンパイル時やランタイム時に具体的な型を導けば良い。

また、stub のみに注目すると、stub は Context から具体的な DataSegment X を取り出す操作に相当し、部分型の関数の引数の仮定のような振舞いをする。
加えて、軽量継続する際に X の計算結果を Context に格納してから goto する部分を別の Meta CodeSegment として分離すると、部分型の返り値の仮定のような振舞いを行なう。
このようにノーマルレベルの CodeSegment の先頭と末尾にメタ計算を接続することによってノーマルレベルの CodeSegment が型付けできる。
型付けを行なう際には DataSegment の集合としての Meta DataSegment が必須になるが、構造体としてコンパイル時に生成することで CbC に組み込むことができる。

なお、メタ計算に利用する Meta DataSegment と Meta DataSegment も同様に型付けできる。
Meta DataSegment の部分型に相当する Meta Meta DataSegment を定義してやれば良い。
ここで興味深いのはあるレベルの CodeSegment は同レベルの DataSegment において型付けされるが、一つ上の階層から見ると、下の階層のDataSegmentとして一貫して扱えることにある。
このようにメタ計算を階層化することにより、メタ計算で拡張された計算に対しても他のメタ計算が容易に適用できる。

% }}}