☰

Haskell シングルトン: SNat で得られるものは何ですか? 質問する

tag-icon • tag-icon haskell dependent-type type-level-computation singleton-type
Haskell シングルトン: SNat で得られるものは何ですか? 質問する

Haskell シングルトンを grook しようとしています。

論文ではシングルトンを使用した依存型プログラミングそして彼のブログ記事ではシングルトンv0.9がリリースされました！リチャード・アイゼンバーグはデータ型を定義しているナットこれはペアノ​​公理を用いて自然数を定義する:

data Nat = Zero | Succ Nat

言語拡張機能を使用することでデータの種類このデータ型は型レベルに昇格されます。データコンストラクタゼロそしてサック型コンストラクタに昇格される'ゼロそして'サックこれにより、すべての自然数に対して、型レベルで対応する唯一の型が得られます。例えば、3我々が得る'サック（ 'サック（ 'サック 'ゼロ））. これで、自然数が型として存在するようになりました。

次に彼は価値レベルで関数を定義するプラスそしてタイプレベルではタイプファミリープラス加算演算が利用可能になります。推進するシングルトンライブラリのfunction/quasiqoterを使用すると、自動的にプラスタイプファミリーからプラス関数です。そのため、型ファミリを自分で記述する必要がなくなります。

ここまでは順調ですね！

GADT構文ではデータ型も定義するスナット:

data SNat :: Nat -> * where
  SZero :: SNat Zero
  SSucc :: SNat n -> SNat (Succ n)

基本的に彼はナット入力するスナットコンストラクタ。なぜこれが必要なのか？何が得られるのか？データ型はナットそしてスナット同型ではないのはなぜですか？スナットシングルトン、そしてなぜナットシングルトンではないですか? どちらの場合も、すべての型には 1 つの値、つまり対応する自然数が含まれます。

ベストアンサー1

何を得られるのか？うーん。シングルトンのステータスは厄介だが現在必要な回避策、そしてそれらを早く排除できればできるほど良いのです。

図を明確にしてみましょう。データ型がありますNat:

data Nat = Zero | Suc Nat

（「c」の数よりもさらに些細な問題で戦争が始まったこともあるSuc）

型にはNat実行時の値があり、型レベルでは区別できません。Haskellの型システムは現在、交換プロパティは、型付けが正しいプログラムであれば、型付けが正しい部分式を同じスコープと型を持つ別の部分式に置き換えても、プログラムは型付けが正しいままであることを意味します。たとえば、

if <b> then <t> else <e>

に

if <b> then <e> else <t>

プログラムの型をチェックした結果、何も問題が起きないことが保証されます。

置換プロパティは恥ずかしいものです。これは、意味が重要になり始めた瞬間に型システムが諦めてしまうことの明確な証拠です。

実行時の値のデータ型である は、Nat型レベルの値と の型にもなります'Zero。'Suc後者は Haskell の型言語でのみ存在し、実行時にはまったく存在しません。 と は'Zero型'Sucレベルで存在しますが、これらを「型」と呼ぶのは役に立たないので、現在そうしている人はやめるべきであることに注意してください。これらには型がないので*、値を分類するそれは、その名にふさわしいタイプの機能です。

実行時と型レベルの間で直接交換する手段がないのでNat、面倒なことになる。典型的な例は、ベクトル:

data Vec :: Nat -> * -> * where
  VNil   :: Vec 'Zero x
  VCons  :: x -> Vec n x -> Vec ('Suc n) x

与えられた要素（おそらくインスタンスの一部Applicative）のコピーのベクトルを計算したいとします。その場合、次のような型を与えるのが良いかもしれません。

vec :: forall (n :: Nat) (x :: *). x -> Vec n x

nしかし、それは本当に機能するのでしょうか？何かのコピーを作成するには、実行時に知る必要があります。プログラムは、展開して停止するか、展開して続行するnかを決定する必要があり、そのためには何らかのデータが必要です。良い手がかりとなるのは、量指定子です。VNilVConsforallパラメトリック: 定量化された情報は型に対してのみ使用可能であり、実行時に消去されることを示します。

forallHaskellは現在、実行時に依存量化（何をするか）と消去の間にまったく偽りの一致を強制している。ないは、依存しているが消去されていない量指定子をサポートします。これは、よく と呼ばれますpi。 の型と実装はvec次のようになります。

vec :: pi (n :: Nat) -> forall (x :: *). Vec n x
vec 'Zero    x = VNil
vec ('Suc n) x = VCons x (vec n x)

- 位置の引数はpi型言語で記述されますが、データは実行時に使用できます。

では、代わりに何をするのでしょうか？シングルトンを使って、間接的に型レベルデータの実行時コピー。

data SNat :: Nat -> * where
  SZero :: SNat Zero
  SSuc  :: SNat n -> SNat (Suc n)

ここで、SZeroと はSSuc実行時データを作成します。SNatは と同型ではありませんNat。前者の型は でNat -> *、後者の型は である*ため、これらを同型にしようとすると型エラーになります。 には多くの実行時値がありますNatが、型システムはそれらを区別しません。異なる にはそれぞれ 1 つの実行時値 (言及する価値がある) があるSNat nため、型システムがそれらを区別できないという事実は重要ではありません。重要なのは、それぞれがSNat n異なる に対して異なる型でありn、GADT パターン マッチング (パターンは、一致することがわかっている GADT 型のより具体的なインスタンスである可能性がある) によって に関する知識を洗練できるということですn。

我々は今こう書くことができる

vec :: forall (n :: Nat). SNat n -> forall (x :: *). x -> Vec n x
vec SZero    x = VNil
vec (SSuc n) x = VCons x (vec n x)

シングルトンを使用すると、型情報の改良を可能にする唯一の実行時分析形式を利用して、実行時と型レベルのデータ間のギャップを埋めることができます。シングルトンが本当に必要かどうか疑問に思うのは当然ですが、現時点では、そのギャップがまだ解消されていないため、シングルトンは必要です。

おすすめ記事