Haskellでの型レベルプログラミング

TL;DR

• Haskell での型レベルプログラミングの解説書である。型とカインドの基本から入り、依存型を模倣するシングルトンパターンを目指す。定理証明も扱う。
• Zenn で公開している同名の本に加筆したもので、「型レベルリスト」「定理証明の代償」「Dependent Haskellへの展望」の章が加わっている。

目次

1. はじめに
2. 型とカインド
3. 幽霊型とProxy
4. 発展：カインド多相
5. データ型の昇格（DataKinds拡張）
6. 型レベル関数と型族、型演算子
7. 型レベル計算の結果を実行時に利用する：型クラス
8. 一般化された代数的データ型 (GADT)
9. 復習・小まとめ
10. シングルトン型と依存型の模倣
11. 定理証明
12. 応用：Constraintカインド
13. 応用：GHCの型レベル自然数（Natカインド）
14. 応用：GHCの型レベル文字列（Symbolカインド）
15. 応用：GHC.Generics
16. 応用：型レベルリスト
17. 応用：実行時型情報（Typeable）
18. 定理証明の代償
19. Dependent Haskellへの展望
20. あとがき

関連

• Haskell
• Web 版
• 技術書典の販売ページ