52

私は種類の概念に慣れ始めたばかりなので、質問をうまくまとめられていない場合はご容赦ください...

値には型があります:

3 :: Int
[1,2,3] :: [Int]
('c',True) :: (Char,Bool)

型には種類があります:

the type 'Int' has kind *
the type '[Int]' also has kind *
   but the type constructor [] has kind * -> *
similarly, the type (Char,Bool) has kind  *
   but the type constructor (,) has kind * -> * -> *

Kindsには何がありますか？

それらの種類には、同類、ジャンル、品種、または品種がありますか?

この一連の抽象化はどこまで進んでいますか? 言葉が足りなくなったからやめるのか、それとも遠くへ行くことに価値がないからやめるのか。それとも、人間の認識の限界にすぐに達し、より高いジャンルの種類に頭を包むことができないためでしょうか?

関連する質問: 言語は、値を作成するための値コンストラクター (cons 演算子など) を提供します。言語は、型を作成するための (,) や [] などの型コンストラクターも提供します。kind-constructor を公開して kind を作成する言語はありますか?

私が興味を持っているもう 1 つのエッジ ケース: どうやら「底の型」と呼ばれる、⊥ として示される値を持たない型があるようです。型のない種類、下の種類はありますか？

4

2 に答える 2

30

用語typeとkindはうまくスケーリングしません。バートランド・ラッセル以来、型理論家は「型」の階層を使用してきました。これの 1 つのバージョンは、Integer : Type 0, Type 0 : Type 1, Type 1 : Type 2, ..., Type n : Type (n+1), .... Coq や Agda などの依存型付き言語では、これらの「より高い並べ替え」が頻繁に必要になるというものです。

このようなレベルは、ラッセルのパラドックスを回避するのに役立ちます。使用Type : Typeすると矛盾が生じる傾向があります (別のデザインについてはQuineを参照してください)。

この数字の使用は、必要な場合の標準表記です。t : Type n型理論の中には、「もしそうなら」という「累積的な種類」、「累積的なレベル」、または「累積的な並べ替え」という概念がありますt : Type (n+1)。

累積レベル + 「レベル ポリモーフィズム」は、 とほぼ同じくらい柔軟な理論を提供しますType : Typeが、パラドックスを回避します。Coq はレベルをほとんど暗黙的にしますが、 sortSetとPropは両方とも型付けされていますType, Type {1} : Type {2}. つまり、通常は数字を目にすることはなく、ほとんどの場合は機能します。

Agda には、レベル ポリモーフィズムを提供する言語プラグマがあり、物事を非常に柔軟にしますが、やや官僚的になります (ただし、Agda は通常、他の分野では Coq よりも「官僚的」ではありません)。

もう一つの良い言葉は「宇宙」です。

于 2013-01-18T19:45:15.063 に答える
6

おそらく、タイプ/種類/種類の無限の塔があるが、本格的な依存型がないHaskellの方言であるOmegaに関するTimSheardの論文を読む必要があります。これが必要な理由を説明し、「ソート」より上のレベルは実際には（少なくともこれまでのところ）直接使用されていないことを示しています。

于 2013-01-25T20:05:04.377 に答える