タイプ理論：タイプの種類

Question

タイプの種類、高級タイプなどについては興味深いことがたくさんあります。デフォルトでは、Haskellは一種の2種類をサポートしています。

• シンプルタイプ：*
• 型コンストラクタ：
  • Typeパラメータ：* → *

  最新のGHCの言語拡張ConstraintKindsは、新しい種類の追加制約：Constraint

またthis mailing listを読んだ後、それは一種の別のタイプが存在することが明らかになり、それはGHCでサポートされていない（そのようなサポートは、.NETに実装され）：

• 箱なしタイプ：#

私はpolymorphic kindsについて学びました。私はその考えを理解していると思います。また、Haskellは明示的に類別された数量化をサポートしています。

だから私の質問は以下のとおりです。

• 種類の任意の他のタイプを行いますが存在しますか？
• 他の種類関連言語機能はありますか？
• subkindingは何を意味しますか？それはどこに実装されていますか？
• kindsの上にタイプシステムがありますか？typesの上のタイプシステムはkindsですか？ （ちょうど興味がある）

Answer 1

の発表が存在しています。ページIntermediate Typesは、GHCで使用されている他の種類（ボックス化されていない種類とさらに複雑な種類の両方を含む）を記述します。 Ωmega言語は、より高級な型を最大の論理拡張にして、ユーザーが定義できる種類（および並べ替え、およびそれ以上）を可能にします。 This pageは、Haskellでユーザ定義可能な種類を可能にするGHC用のシステム拡張を提案し、なぜ有用であるかの良い例を提案しています。このような短い抜粋として

、あなたはリストの長さのタイプレベルの注釈を持っていたリストの種類を望んでいたと仮定し、：

data Zero 
data Succ n 

data List :: * -> * -> * where 
    Nil :: List a Zero 
    Cons :: a -> List a n -> List a (Succ n) 

意図が最後の型引数が唯一でなければならないことですZeroまたはSucc nであり、nは再びZeroまたはSucc nです。要するに、Natという新しい種類を導入する必要があります。これには、ZeroとSucc nの2種類だけが含まれています。その後Listデータ型は最後の引数は、型チェッカーは、はるかに弁別それが受け入れ何で、だけでなく、タイプレベルを作ることができるようになる

data List :: * -> Nat -> * where 
    Nil :: List a Zero 
    Cons :: a -> List a n -> List a (Succ n) 

このように、*が、Natではないことを表現できますはるかに表現力豊かなプログラミング。

Answer 2

種類が種類に分類されるように、種類は種類によって分類されます。

Ωmega programming languageは、任意のレベルでユーザー定義可能な種類の種類システムを備えています。 （そのウィキは、上記の種類とレベルを参照していると思いますが、わかりません）

Answer 3

種類を種類レベルに値上げし、型レベルに値を引き上げる提案がありました。これは、それがでエンコードされたディメンションの持つベクトルである

data Z 
data S a 

data Vec (a :: *) (b :: *) where 
    VNil :: Vec Z a 
    VCons :: a -> Vec l a -> Vec (S l) a 

：それがすでに実装されている場合（または、それは、これまで「プライムタイム」に達する場合）しかし、私は

は、次のコードを考えてみましょう知りませんタイプ。私たちはZとSを使って自然数を生成しています。これは素晴らしいことですが、Vecを生成する際に適切な型を使用している（コンテンツの長さを誤って切り替える可能性がある）場合は「型チェック」できず、タイプSとZも生成する必要があります。必要であれば、これはタイプレベルに親切レベルとSとZにNATを持ち上げてしまう

data Nat = Z | S Nat 

data Vec (a :: Nat) (b :: *) where            
    VNil :: Vec Z a 
    VCons :: a -> Vec l a -> Vec (S l) a 

：あなたはこのような何かを書くことができ、提案して

data Nat = Z | S Nat 

：そうのような自然数を定義しました。だからナットは別の種類で*と同じレベルで生きています。ここで

はい、他の種類は、ブレントYorgey

Typed type-level functional programming in GHC