Haskellの型プログラミング 1.型と代数
読書メモ Thinking with Types
この記事は，「Thinking with Types」を読んで自分なりに作成したメモです。プログラミングは趣味でやっているので，数学や情報工学上の適切な訳語ではない可能性があります。誤りがありましたら，お知らせいただければ幸いです。
第1部 基礎
第1章 型と代数
1.1 同型と濃度
関数プログラミングの切り札の一つは，代数データ型に裏付けられたパターンマッチングである。型に関する代数を活用すれば，型を解析してさらに便利な型に変換できることや，型クラスのような便利な操作が実装可能かがわかる。
濃度 とは，型がとりうる要素の数を表す。
data Void -- 濃度 0
data () = () -- 濃度 1
data Bool = False | True -- 濃度 2
型 a の濃度は |a| で表す。
\begin{align} |Void|&=&0 \\ |()|&=& 1\\ |Bool|&=&2 \end{align}濃度が等しい，要素数が有限の型同士は，互いに同型 という。 型 s と型 t が同型であるとき，s≅t と表記する。
1.2 濃度の和・積および冪乗
要素の濃度を加算して濃度を計算する型を直和型，積算して計算する型を直積型という。
直和型の例
|Either\ a\ b| = |a| + |b|
直積型の例
|(a,b)| = |a| \times |b|
濃度計算の例1
data Mixed a = Mixed Bool aこの時，濃度は以下のようになる。
|Mixed\ a| = |Bool| \times |a| = 2 \times |a|
また，関数で濃度は冪乗となる。
濃度計算の例2
func :: a → bこの時，濃度は以下のようになる。
|a → b| = \underbrace{|b| \times |b| \times\dots\times |b|}_{|a|回の繰り返し} = |b|^{|a|}
これらの知識を使えば，ある問題を解くときに設定した型や型と関数の組み合わせを，より簡便な表現に変換することができる。
1.3 例：Tic-Tac-Toe
略
1.4 カリー・ハワード同型
代数と論理，型は，互いに同じことを別の視点で見ている。例えば，代数でいうa^1=a は，型の世界では () → a = a を表している。これにより，型を正しく設計することは論理を正しく設定することになり，型の正しさを代数や論理を使って証明することが可能となる。
| 代数 | 論理 | 型 |
| a+b | a\vee{}b | Either a b |
| a\times{}b | a\wedge{}b | (a,b) |
| b^a | a\Rightarrow{}b | a→b |
| a=b | a\Leftrightarrow{}b | 同型 |
| 0 | \bot | Void |
| 1 | \top | () |
1.5 カノニカル表現
t=\sum_{m}\prod_{n} t_{m,n}\sumは総和を，\prodは総積を表す。
- カノニカル表現に合致する型
--()
--Either a b
--a → b - カノニカル表現に合致しない型
--(a, Bool)
--(a, Either b c)
ところで，Maybe aのカノニカルな表現はEither a ()だが，だからと言ってMaybe aの代わりにEither a ()を使えというわけではない。カノニカル表現について，詳しくは第13章参照。
