実体のある型レベル自然数をHaskellで実装してみた - 非現実的非日常的非常識的、非日記。

2014-09-19 実体のある型レベル自然数をHaskellで実装してみた Haskell IT GHC では型システムが急速に進化していて、ついに型レベル自然数 (type-level natural number) も組み込まれました。この型レベル自然数は、0, 1, 2, ... というリテラルによって型レベル自然数を得られ、足し算・掛け算・冪乗・引き算・比較が可能です。考えられる使い道としては、配列の要素外アクセスを制限したり、バージョン管理をしたりといったことを、コンパイル時に静的に行うことでしょう。しかしこの型レベル自然数の類 (kind) は Nat であり、真の型（proper type, 実際に値を持つ類 * の型）ではありません。これはもったいない気がします。型に属する値が何種類あるか、という観点から、ヴォイド型 Void は 0、ユニット型 () は 1、ブール型

[nfunato]

[haskell][math]