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

技術書典マーケット：Haskellでの型レベルプログラミング：だめぽラボ

概要

Haskellでの型レベルプログラミングの解説書です。型とカインドの基本から入って、現行のHaskellで依存型を模倣するやり方であるシングルトンパターンを目指します。Haskellによる定理証明も扱います。

この本はZennで公開している同名の本に加筆修正を加えたものです。主な加筆内容は「型レベルリスト」「定理証明の代償」「Dependent Haskellへの展望」です。サンプルコードをGitHubで公開しています。

はじめに……ii
第1章型とカインド……1
第2章幽霊型とProxy……3
- 2.1 幽霊型……3
- 2.2 Proxy型……5
第3章発展：カインド多相……7
- 3.1 カインド推論とカインド多相……7
- 3.2 カインド変数の量化……9
- 3.3 依存カインド……11
- 3.4 Type :: Type……11
第4章データ型の昇格（DataKinds拡張）……13
第5章型レベル関数と型族、型演算子……15
- 5.1 型レベル関数と型族（TypeFamilies拡張）……15
- 5.2 寄り道：型演算子（TypeOperators拡張）……18
- 5.3 部分適用と引数の個数……19
第6章型レベル計算の結果を実行時に利用する：型クラス……21
第7章一般化された代数的データ型 (GADT)……23
- 7.1 一般化された代数的データ型……23
- 7.2 型の等価性……24
- 7.3 存在型……26
- 7.4 寄り道：GADTを解体する……27
第8章復習・小まとめ……28
- 8.1 自然数……28
- 8.2 長さの決まったリスト型……31
- 8.3 次章予告……35
第9章シングルトン型と依存型の模倣……37
- 9.1 シングルトン型……37
- 9.2 型クラス……39
- 9.3 値から型への持ち上げ……40
- 9.4 引数への依存性……41
- 9.5 singletonsライブラリー……42
- 9.6 参考文献……45
第10章定理証明……46
第11章応用：Constraintカインド……51
第12章応用：GHCの型レベル自然数（Natカインド）……53
- 12.1 型レベル自然数の使い所……53
- 12.2 ペアノ自然数の欠点……54
- 12.3 GHC組み込みの型レベル自然数……55
- 12.4 基本的な使い方……55
- 12.5 実行時の自然数を型レベルに持ち上げる……56
- 12.6 四則演算ほか……57
- 12.7 等価性……58
- 12.8 大小比較……59
- 12.9 GHC組み込みの限界……60
第13章応用：GHCの型レベル文字列（Symbolカインド）……70
- 13.1 型レベル文字列……70
- 13.2 型レベル文字……71
- 13.3 関連：オーバーロードされたラベル……72
第14章応用：GHC.Generics……75
- 14.1 ジェネリックプログラミングの考え方……75
- 14.2 GHC.Generics……76
- 14.3 例：データ構築子の名前を取得する……78
- 14.4 もっと知りたい方へ……81
第15章応用：型レベルリスト……83
- 15.1 型レベルリスト……83
- 15.2 型レベルリストの操作……84
- 15.3 ヘテロジニアスリスト……86
- 15.4 型レベルリストに関する定理証明……86
第16章応用：実行時型情報（Typeable）……96
第17章定理証明の代償……101
第18章 Dependent Haskellへの展望……104
- 18.1 量化子……104
- 18.2 型と項の名前空間……106
- 18.3 可視なforall……107
あとがき……111

「だめぽラボ」のページトップへ

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

概要

目次