13

GHC ユーザー ガイドのセクション 7.9.2 で説明されているデータ型昇格の制限の背後にある動機を説明または推測できる人はいますか?

プロモーションには次の制限が適用されます。

  • 種類が の形式のデータ型のみを昇格させ* -> ... -> * -> *ます。data Fix f = In (f (Fix f))特に、 のような高種類のデータ型や、 のような種類が昇格した型を含むデータ型は昇格しませんVec :: * -> Nat -> *。

特に、 などの昇格型に関する最後の部分に興味がありますVec :: * -> Nat -> *。そのようないくつかのタイプを宣伝することは自然に思えます。*より良いドキュメントなどを提供するために、すべての種類を使用するのではなく、さまざまなファントム型に対して特定の昇格された種類を使用するようにライブラリの 1 つを変換しようとしているときに、すぐにそれに遭遇しました。

このようなコンパイラの制限の理由は、少し考えただけですぐに思いつくことがよくありますが、私はこれを見ていません。ということで、「まだ必要ないので作っていない」か「それは無理・決められない・推論をぶち壊す」の範疇に入るのかなと思っています。

4

2 に答える 2

21

昇格された型によってインデックス付けされた型を昇格すると、興味深いことが起こります。想像してみてください

data Nat = Ze | Su Nat

その後

data Vec :: Nat -> * -> * where
  VNil   :: Vec Ze x
  VCons  :: x -> Vec n x -> Vec (Su n) x

舞台裏では、コンストラクターの内部型は、制約によってインスタンス化された戻りインデックスを表します。

data Vec (n :: Nat) (a :: *)
  =            n ~ Ze    => VNil
  | forall k.  n ~ Su k  => VCons a (Vec k a)

今、次のようなものが許可された場合

data Elem :: forall n a. a -> Vec n a -> * where
  Top :: Elem x (VCons x xs)
  Pop :: Elem x xs -> Elem x (VCons y xs)

内部形式への変換は次のようにする必要があります

data Elem (x :: a) (zs :: Vec n a)
  = forall (k :: Nat), (xs :: Vec k a).            (n ~ Su k, zs ~ VCons x xs) =>
      Top
  | forall (k :: Nat), (xs :: Vec k s), (y :: a).  (n ~ Su k, zs ~ VCons y xs) =>
      Pop (Elem x xs)

ただし、それぞれの場合の 2 番目の制約を見てください。我々は持っています

zs :: Vec n a

しかし

VCons x xs, VCons y xs :: Vec (Su k) a

しかし、当時定義されていたシステム FC では、等式制約は両側で同じ種類の型を持たなければならないため、この例はそれほど問題ではありません。

修正の 1 つは、最初の制約の証拠を使用して 2 番目の制約を修正することですが、従属制約が必要になります。

(q1 :: n ~ Su k, zs |> q1 ~ VCons x xs)

もう 1 つの修正方法は、15 年前に従属型理論で行ったように、異種方程式を許可することです。必然的に、構文的に明らかではない方法で種類が等しいものの間に方程式が存在します。

現在支持されているのは後者の計画です。私が理解している限りでは、あなたが言及したポリシーは、(Weirich と同僚によって提案された) 異種の平等を備えたコア言語の設計が成熟して実装されるまで、保留中の立場として採用されていました。私たちは興味深い時代に生きています。

于 2014-01-18T17:31:11.580 に答える
4

これはおそらく、GHC が特に豊富な「並べ替え」の概念を持っていないという事実に由来します。並べ替えは種類の型です。

  values : type : kind : sort : ...

データの種類を含む種類のかなり複雑なシステムがありますが、すべての種類は依然として非常に単純な並べ替えに昇格していることに注意してください。種類を昇格するNatには、複数の並べ替えタイプ/コンストラクターが必要であり、昇格Fixするには、より高度に並べ替えられた種類が必要ですが、これも基本的な並べ替えシステムではカバーされていません。

これは技術的な障壁ではありません。Coq や Agda (依存型付け言語) などの言語には、これらの完全なスタックが無限にありますが、GHC は最近、親切なシステムを成長させたばかりです。洗練された並べ替えシステムはまだ実装されていませんが、おそらく将来的に実装されるでしょう。

于 2014-01-18T16:29:24.457 に答える