最近、「Haskellでの型レベルプログラミング」という「本」を執筆している。まだ完成ではないが、以下のリンクから読める：
目次
なぜHaskellか
最近いろんな言語が出てきている中で、Haskellの強みとは何だろうか。人によって答えは色々あるだろうが、筆者にとってHaskellの魅力的な側面は強力な型システムである。どのくらい強力かというと、型レベルでプログラミングができ、依存型の模倣さえもできてしまう。
（依存型をやりたいなら最初から依存型のある言語を使えという意見は尤もだが、それはそれとして。）
Haskellでの型レベルプログラミングの解説記事というのは、英語圏ではちらほら見かけるが、日本語圏ではあまり見ない。2018年（原文は2017年）に公開された
が数少ない例である。が、「基本」と銘打っているからかシングルトンパターンにまでは触れていない。
まあ強い人は英語の記事をバリバリ読み込んで型レベル入門するのかもしれないが……門戸は広い方が良い。というわけで、型レベルプログラミングの入門記事を書くことにした。
対象読者はHaskellをある程度わかっている人である。
内容
予定している内容は以下の通りである：
- 型とカインド
- 通常のプログラミングで型を意識しなければならないように、型レベルプログラミングではカインドの意識が必要になる。まずはカインドについて軽く説明する。
- 幽霊型とProxy
- 型レベルプログラミングの最初の応用例は幽霊型だろう。型を関数に渡すときによく使うProxyについてもここで触れておく。
- カインド多相（未執筆）
- 最近のGHCではカインド多相に関連する機能にも手が入っている。その辺も含めて書きたい。
- データ型の昇格
- Typeカインドだけでも型レベルプログラミングはできないこともないが、それでは型のない動的言語と同じ轍を踏むことになる。型レベルのものに「型」をつけるためにDataKinds拡張を使う。…という風な説明にした方が良いか？
- 型レベル関数と型族、型演算子
- 最初の山場である。
- 型レベル計算の結果を実行時に利用する：型クラス
- 言語によっては型レベルプログラミングの結果を実行時に持ち越せないものがあるが、Haskellは違う。型クラスを使うと型に対してパターンマッチした結果を実行時に利用することができる。
- GADTと型の等価性
- シングルトンと定理証明の準備としてGADTが必要になるのでここで説明しておく。
- シングルトン型と依存型の模倣
- 本丸である。
- 定理証明
- GHCの型検査器をなだめる方法を扱う。
- 応用：Constraintカインド
- GHCでは制約も型として扱えるようになっている。
- 応用：GHCの型レベル自然数（Natカインド）（執筆中）
- Natカインドについては以前Qiitaに書いたが、その内容をこの本の流れに合わせて再構成する。比較すると説明が薄っぺらくなっていないか、という気がする……。
- 応用：GHCの型レベル文字列（Symbolカインド）（未執筆）
- GHC 9.2でCharカインドが使えるようになったのでその辺も併せて書きたい。
- 応用：GHC.Generics（未執筆）
- 応用：実行時型情報（Typeable）（未執筆）
媒体
今回はZennの「本」という形式にして、随時更新していくことにした。この方式について思うところを書いておく。
要件として、Haskellでの型レベルプログラミングのトピックは多岐にわたるので、章分けができると良い。単独の記事に詰め込むと上下に長くなってスクロールが大変になるだろう。
次に、先に全体を書き上げて一気に公開するというのは筆者のやる気的に厳しい。随時更新という形が望ましい。
章分けして随時更新という形では、以前「週刊 代数的実数を作る」でやったように、連載記事にするという手がある。しかし、先に公開した分を後から修正したり、先に置くべき内容を後から書いたりするのはやりにくい。計画性が必要となる。
Zennの「本」は、当然章分けができる。GitHub連携していれば更新履歴をGitHubで確認できる（という言い訳が立つ）ので本文中に更新履歴を残すことに神経質にならなくていい。そして、未完成な状態で公開することに心理的抵抗が少ない。
読者やZennの運営がどう思うかは別として、Zennの「本」はやる気の乏しい執筆者がまとまったボリュームの文章を書くのに優しすぎる媒体なのである。
気が向いたら表紙も作りたい。
