データ型昇進の制限の動機

Question

セクション7.9.2 of the GHC user guideで説明されているデータ型昇格の制限の背後にある動機を誰かが説明したり推測したりすることはできますか？

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

• 私たちは、その種類のフォーム* -> ... -> * -> *のあるデータ型を促進します。特に、data Fix f = In (f (Fix f))などの上位のデータ型や、Vec :: * -> Nat -> *などのプロモートされたデータ型を持つデータ型は宣伝しません。特に

、私はそのようなVec :: * -> Nat -> *として昇格の種類についての最後のビットに興味があります。そのようないくつかのタイプを宣伝するのは当然のようです。私はかなり速くそれに遭遇していましたが、私のライブラリの1つを、より良いドキュメントなどを提供するために、すべて種類の*を使用する代わりに、さまざまなファントムタイプに対して特定のプロモートされた種類を使用するように変換しようとしました。

これらのようなコンパイラの制限の理由は、しばしば少し考えて飛び出してしまいますが、私はこれを見ていません。だから私はそれが "まだ必要ではないので、私たちはそれを構築しなかった"または "それは不可能/決める/推論を破壊する"というカテゴリーに入るのだろうかと思っています。

Answer 1

プロモーションタイプでインデックス登録されたタイプを宣伝すると面白いことが起こります。私たちは舞台裏

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で

を持っているので、この例ではinconsiderably問題ではありません。

一つの修正は、第二を修正するために第1の制約のために証拠を使用しているが、私は依存の型で行ったように、我々は、別の修正が単に異種の方程式を可能にしている依存制約

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

を必要とするだろう15年前の理論。文法的に明白でない方法で同種のもの同士の間には必然的に等式が存在します。

現在、後者の方が有利です。私が理解する限り、あなたが言及した方針は、（Weirichとその同僚によって提案された）異質な平等を持つコア言語の設計が実現するまで保持位置に採択されました。私たちは面白い時代に住んでいる。

Answer 2

これはおそらく、ソートが

values : type : kind : sort : ... 

お知らせので、種類の一種であるGHCは、「種類」のいずれかの特に豊富な概念を持っていないという事実に由来我々はかなり複雑なシステムの持っていながら、そのデータ型を持つ種類は、すべての種類がまだ非常に単純な種類に昇格します。 Natのような種類を宣伝するには、複数のソートタイプ/コンストラクタが必要で、Fixのプロモートにはより高いソートされた種類が必要です。プリミティブソートシステムでは扱いません。

これは技術的な障壁ではありません。CoqやAgda（依存型言語）のような言語は無限にスタックしていますが、GHCは近年では種類システムを成長させました。洗練されたソートシステムはまだ実装されていないだけで、将来は取得する予定です。