19
私はハスケルシングルトンを突き詰めようとしています。言語拡張にDataKindsこれを使用することによりハスケルシングルトン：私たちはSNatで何を得ますか
data Nat = Zero | Succ Nat
：紙Dependently Typed Programming with Singletons で、彼のブログ記事singletons v0.9 Released! リチャード・アイゼンバーグで
はペアノの公理と自然数を定義するデータ型 ナットを定義しますデータ型は型レベルに昇格されます。 データconstuctors ゼロと Succとしては型コンストラクタ 'ゼロと ' 成功回数に昇格されています。 これにより、すべてのNaturalナンバーに対して、タイプレベルで対応する単一の固有タイプが取得されます。例： 'Succ（' Succ '' Succ 'Zero））を取得します。 これで、タイプとして自然数が得られました。彼はその後、値レベルで機能プラスを定義し、タイプレベルでタイプファミリープラス は、加算演算が利用できる持っています。 で はシングルトンライブラリの機能/ quasiqoterを促進し、我々は自動的に プラス機能からプラスタイプファミリを作成することができます。だから私たちは型のファミリーを書くのを避けることができます。
これまでのところとても良い！ GADTの構文で
彼はまた、SNATデータ型を定義しています
data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
基本的に、彼は唯一のSNATコンストラクタにナット型をラップします。 これはなぜ必要なのですか？私たちは何を得ますか？ データ型はナットおよびSNatは同形ではありませんか？なぜSNatシングルトンですか、なぜですかナットではない シングルトン？どちらの場合も、すべての型には1つの単一値、つまり対応する自然数が存在します。