Chapter 09

2.3 型とは何か?

さのたけと
さのたけと
2021.05.04に更新

最も単純な型の解釈は,それを値の集合と考えることだ.Bool 型は(Haskell では具体型は大文字で始まることを思い出そう)TrueFalse からなる 2元集合だ.Char 型は aą などの全ての Unicode 文字の集合だ.

集合は有限でも無限でも良い.String 型は,Char のリストであり,無限集合の例である.

xInteger 型だと宣言するということは,

x :: Integer

x は整数全体の集合の要素だということだ.Haskell で Integer は無限集合であり,任意精度の演算を行うことができる.マシンが用いる整数に対応する有限集合としての Int 型もある,これは C++ の int に対応する.

型と集合の同一視が上手くいかなくなる微妙な点もある.循環的な定義を伴う多相関数を考えると,「集合全体の集合」を考えることはできないことから問題に当たってしまうのだが,約束通り私は,数学的な厳密さにこだわる気はない.素晴らしいことに「集合の圏」\mathbf{Set} というものはあって,我々はそれを扱う.\mathbf{Set} においては,対象は集合で,射は関数である.

\mathbf{Set} は非常に特別な圏だ:なぜならその対象の中身を覗き込んで,多くの直観的な理解を得ることができるから.例えば,我々は空集合は要素を持たないことを知っている.一元集合が存在することも知っている.関数は一つの集合の要素を他の集合の要素に対応させる.二つの要素が同じ要素に対応することはあるが,一つの要素が二つの要素に対応することはない.恒等関数は,集合の要素をそれ自身に対応させる,などなど.この先のプランは,徐々にこれらの情報を忘れていって,上に述べたことを全て圏の言葉で表現し直すことだ.つまり要素を使わず,対象と射だけで.

理想的な世界では,Haskell の型は数学の集合で,Haskell の関数は数学の関数だと言えば良い.ただ一つ小さな問題がある:数学の関数はコードを実行しない,結果を予め知っている.Haskell の関数は答えを計算しなければいけない.この答えが有限個のステップで終わるなら問題にならない,それがどれほど大きなものでも.問題は,再帰を伴う計算があり,それは永遠に終わらないかも知れないことだ.単純に非停止関数を禁止するということはできない,なぜならそれは決定不可能だからだ.これが有名な停止性問題である.そこでコンピュータ科学者は素晴らしいアイディア(または大きなハック,どちらかはあなたの価値観による)を思いついた.それは全ての型に ボトム (bottom) と呼ばれる特別な値を追加したことだ.ボトムは \bot と書かれる.この "値" は停止しない計算に対応する.

したがって,次のように宣言される関数:

f :: Bool -> Bool

が返す値は,True, False, _|_ のいずれかで,最後の場合は永遠に終わらないことを意味する.

興味深いことに,一度ボトムを型システムの一部として受け入れると,全ての実行時エラーをボトムとして扱うのが便利で,さらには関数が明示的にボトムを返すことを許しても良くなる.後者は undefined を用いて,次のようにする:

f :: Bool -> Bool
f x = undefined

この定義は有効である,なぜなら undefined はボトムとして評価され,ボトムは Bool を含む全ての方のメンバーだから.こんな書き方も許される:

f :: Bool -> Bool
f = undefined

(つまりパラメータ x なしで),なぜならボトムは型 Bool -> Bool のメンバーでもあるから.

ボトムを返す可能性のある関数は 部分的 (partial) と呼ばれ,全域的 (total) と対立するものである.

ボトムがあることで,Haskell における型と関数のなす圏は \mathbf{Set} ではなく \mathbf{Hask} と書かれる.理論的な観点では,これは永遠に終わらないコンパイルの原因となるものだが,この話はここで止めておく.実用的な観点では,終わらない関数やボトムのことは無視してよく,\mathbf{Hask}\mathbf{Set} そのものだと思って良い[1]

(和訳:@taketo1024

脚注
  1. Nils Anders Danielsson,
    John Hughes, Patrik Jansson, Jeremy Gibbons, "Fast and Loose Reasoning is Morally Correct".この論文で,ほとんどの状況でボトムを無視していいことの正当性が説明されている. ↩︎