読書メモ　Thinking with Types

この記事は，「Thinking with Types」を読んで自分なりに作成したメモです。プログラミングは趣味でやっているので，数学や情報工学上の適切な訳語ではない可能性があります。誤りがありましたら，お知らせいただければ幸いです。

第1部　基礎

第1章　型と代数

第2章 式term，型typeおよび種kind

2.1　種カインドシステム

日常的な Haskell プログラムは，式termと型typeで構成されている。比喩的に言えば，型レベルのプログラミングでは，型と種カインドで構成される。種システムとは，型の型システムのことと思えば良い。つまり，種カインドとは型の型のようなものである。

魚野： GHCでは，種カインドは（型の種カインド, アロー種カインド, 制約種カインド,データ種カインド）の四種類？

2.1.1 型の種カインド

型という言葉には複数の意味がある。

広義には，型レベルで存在するもののこと。式termでもなければ種カインドでもない。

狭義には，TYPEと書かれるもの，即ち，型の種カインドのことである。歴史的に，TYPEは*と表現されていた。TYPE は，IntやMaybe Boolのようなものの種カインドのことで，実行時に存在するものの種類を区分する役割がある。TYPEでない種カインドとしては，例えばパラメタなしのMaybeやShowがある。

以降，TYPE（魚野注：原著ではSMALLCAPSで表現） と大文字斜体で表現した場合，TYPEという種カインドを表すことにする。

2.1.2 Arrow 種カインド(Arrow Kinds)

後で調べる： HKTとArrow（→）を使って作られた種カインドの関係は？HKTは高階型とでも訳す？

HKT(Higher-kinded types)とは，型変数を持つものをいう。型変数に具体的なものが詰められたとき，HKTは，単なる TYPE となる。逆にいうと，HKTの型コンストラクタは，TYPE ではない。

HKTの例

Maybe

TYPE パラメタを一つとるので，TYPE → TYPE という種カインドを持つ。

MaybeT

TYPE パラメタを二つとるが，同様にパラメタをふたつとるEitherのパラメタが二つとも TYPE であるのと異なり，一つのパラメタはMonadでなければならない。Monadは常にTYPE → TYPEという種カインドを持つので，MaybeTが持つ種カインドは，(TYPE → TYPE ) → TYPE → TYPEとなる。

2.1.3 制約種カインド(Constraint Kinds)

種カインドは，単に型にだけではなく，全ての型レベルのものに適用される。

例えば，Showの型は，型署名シグネチャとしてShow a ⇒ a → Stringと表現されるが，これは明らかに TYPE ではない。実はShowの種カインドは TYPE ではなく，CONSTRAINT である。

CONSTRAINT は，制約constraint種カインド，即ち，型クラスのうち全ての型変数に具体的な型の詰め込みが終わったsaturatedものの種カインドである。

2.2 データ種カインド(Data Kinds)

GHC拡張の-XDataKindsを使うと，TYPE や CONSTRAINT 及びアロー（→)を使ったそれらの派生型とはまた別の種カインドを使うことができる。

-XDataKindsは，データコンストラクタを型コンストラクタにする。

例

data Bool = True | False

-XDataXindsが有効になっていれば，上記の宣言は，Boolという新しい種カインドと，Boolという種カインドを持つ'Trueと'Boolという二つの新しい型を宣言したことにもなる。

このような'Trueと'Falseを，昇格プロモートしたデータコンストラクタ という。

コンストラクタ名の前についているアポストロフィ（'）はティックtickと呼ばれ，通常の型コンストラクタと昇格プロモートしたデータコンストラクタを区別するために用いられる。

例

data Unit = Unit

ティックを使っていれば，上記のような宣言をされたときでも，TYPEという種カインドを持つ型コンストラクタUnitと，UNITという種カインドを持つプロモートされたデータコンストラクタ'Unitが，型レベルで混在していても明確に区別できる。Maybe Unit型の値を扱うことは正当だが，Maybe 'Unitの値を扱おうとすると，種カインドの誤りとして検出される。

データ種カインドの重要性

Haskellの型レベルプログラミングでのデータ種カインドの位置付けは，通常のHaskellプログラミングの型の位置付けと同じであり，仮に型レベルプログラミングでデータ種カインドを欠いていれば，それは通常のプログラミングで動的型付けをしているとの同じことになり，種カインドを明示するほど，型の制約について豊富なヒントが得られるようになる。

昇格プロモートしたデータコンストラクタは，実行時に，種カインドの誤りとして不具合につながる型の情報を教えてくれる。

例

ここでは，予め組み込まれた管理者の権限がないと扱えない機能の管理をすることを考えよう。万が一にも非管理者が当該機能を使えるようになってしまうことを避けるため，この制約をビジネスロジックの誤りではなく，型の誤りとして扱うことにし，型システムの力を借りて誤り無きようにしよう。

以下のように，UserType型を定義し，これによって昇格プロモートしたデータコンストラクタを扱うことにする。また，User型を以下のように宣言し，各ユーザが権限トークンを保持できるようにする。加えて，厳密に管理しなければならない機能を実行する際には，管理者権限トークンを必要とする旨を以下のように記述する。

data UserType = User | Admin

data User = User { userAdminToken ::  Maybe (Proxy 'Admin) , ... }

doSensitiveThings :: Proxy 'Admin -> IO()
doSensitiveThings = ...

こうすれば，何か誤って管理者権限トークンなしでdoSensitiveThingsを呼び出すプログラムを記述してしまったとしても，型エラーでコンパイルできないことになる。更に改善した手法（後述のSTトリック等）もある。

2.3 組込みbuilt-in型の昇格プロモート

注：本節では，ライブラリの読み込みが必要である。

import GHC.TypeLits

-XDataKindsを使うと，組込み型（文字列，数，リスト及びタプル）などほとんど全ての型が自動的に種カインドに昇格プロモートされる（GADTsやその他の普通でない型は昇格プロモートは自動ではできない）。

2.3.1 Symbol

Stringが昇格プロモートすると， SYMBOL という種カインドとなる。 SYMBOLに属するものは，文字列ではないが，GHC.TypeLitsで定義されているAppendSymbolプリミティブを使って結合可能である。

> :set -XDataKinds

> :kind "hello"
"hello" :: Symbol

> :kind AppendSymbol
AppendSymbol :: Symbol -> Symbol -> Symbol

> :kind! AppendSymbol "thinking" " with types"
AppendSymbol "thinking" " with types" :: Symbol
= "thinking with types"

SYMBOL の比較も，CompSymbolプリミティブで可能。ただし，Ordering が得られることに注意。この Ordering は，標準ライブラリ Prelude の Ordering が -XDataKinds によって昇格プロモートされたものである。

> :kind CmpSymbol
CmpSymbol :: Symbol -> Symbol -> Ordering

> :kind! CmpSymbol "sandy" "sandy"
CompSymbol "sandy" "sandy" :: Ordering
= 'EQ

> :kind! CmpSymbol "sandy" "batman"
CompSymbol "sandy" "batman" :: Ordering
= 'GT

2.3.2 自然数

昇格プロモートした数は更に変則的だ。自然数のみが昇格プロモートする（つまり，負の数や分数型，不動小数点型の昇格プロモートはない）。自然数が昇格プロモートしたとき，種カインドは NAT となる。

文字列の時と同様，GHC.TypeLitsには，NAT リテラルの演算を行うことができる演算子が定義されており，-XTypeOperatorsを使えば利用できる。

> :set -XTypeOperators

> :kind! (1 + 17) * 3
(1 + 17) * 3 :: Nat
= 54

> kind! (128 `Div` 8) ^ 2
(128 `Div` 8) ^ 2 :: Nat
= 256

2.3.3 リスト

リストのデータコンストラクタが昇格プロモートした場合，元のリストの定義とよく似た構造をしている。

data [a] = [] | a: [a]

リストのデータコンストラクタ昇格プロモートすると得られるのは，

• '[] の種カインドは[A]
• '(:)の種カインドはA → [A] → [A]　　；中置演算子として使う場合， x ': xs

種カインドレベルでの多相性については後述するが，概ね，類推できるような多相性を持つ。

リストのデータコンストラクタは記号なので，-XTypeOperatorsが必要である。

また，[Bool]の種カインドはTYPEであり，式レベルのことを差しているが，'[Bool]の種カインドは[TYPE]であり，型レベルの，BOOL型の要素のリストである。

2.3.4 タプル

タプルについても，'(,)というコンストラクタとなる。

2.4 型レベルの関数 閉じた型族？closed type familliy

-XDataKindsが本当に有用となるのは，閉じた型族？closed type familliyと組み合わせて使う時である。閉じた型族？closed type familliesとは，型レベルの関数と思えば良い。既に，CmpSymbolやDivなどを紹介した。

GHCで自分の好きな閉じた型族？closed type familliyを定義することができるが，まずは標準的な関数と，その閉じた型族？closed type famillies版を見比べていこう。

or :: Bool → Bool → Bool
or True  _ = True
or False y = y

type family Or (x :: Bool) (y :: Bool) :: Bool where
  Or 'True  y = 'True
  Or 'False y = y

Mapもmapにそっくりの構造である。

map :: (a → b) → [a] → [b]
map _ []       = []
map f (a : as) = f a : map f as

type family Map (x :: a → b) (i :: [a]) :: [b] where
  Map f '[]       = '[]
  Map f (x ': xs) = f x ': Map f xs

もっとも，閉じた型族？closed type familliyは部分適用ができないので，Mapはそれほど有用でははい。

なお，Orの定義の際，その種カインドシグネチャをOR x y :: BOOL → BOOL → BOOLではなく，Or (x :: BOOL) (Y :: BOOL) :: BOOLとした。型族？type familliyの種カインドは曲者で，::の後に書いた種カインドは，型族？type familliyが返す型の種カインドであり，型族？type famillyそのものの種カインドではないからである。