类型理论：型种

我读过很多关于种类型，-kinded较高的类型等有趣的东西。默认情况下，哈斯克尔支持两类种：类型理论：型种

简单类型：*
类型的构造函数：* → *

最新GHC的语言扩展ConstraintKinds增加了一个新的种类：

类型参数约束：Constraint

读取this mailing list后也变得清楚的是另一种类型的种可能存在，但它不被支持GHC（但这种支持在.NET实现）：

无盒装类型：#

我已经了解了polymorphic kinds，我想我理解了这个想法。 Haskell也支持明确的量化。

所以我的问题是：

是否有任何其他类型的种类的存在？
是否还有其他种类相关的语言特征？
是什么subkinding意思？它在哪里实施/有用？
有上kinds顶部的类型系统，如kinds上的types顶部类型的系统？（只是感兴趣的）

来源

2011-10-13 ControlFlow

是演示文稿，存在其他类型。页面Intermediate Types描述了GHC中使用的其他类型（包括非盒装类型和一些更复杂的类型）。 Ωmega语言将最高逻辑扩展的类型更高，允许用户可定义的类型（以及更高的排序）。 This page提出了一种GHC的系统扩展，它允许用户在Haskell中定义种类，以及它们为什么会有用的一个很好的例子。

作为一个简短的摘录，假设你想其中有列表的长度类型的注解列表类型，像这样：

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两种类型。然后List数据类型可以表达的是，最后一个参数是不是一个*，但Nat，像

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

这将使类型检查，以更加辨别什么它接受，以及制造型级别编程更具表现力。

来源

2011-10-13 12:23:48

就像种类被种类分类一样，种类也被分类。

Ωmega programming language与用户自定义类型的任何级别的一种制度。（所以它的维基说，我觉得它是指种类和水平以上，但我不知道。）

来源

2011-10-13 10:39:39 missingfaktor

Ω很好：3 – raichoo

已经有解除类型分为样的水平和值代入式水平的建议。但我不知道这是否是已经实现的（或者，如果它曾经将达到“黄金时间”）

考虑下面的代码：

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类型，如果我们已经很不方便定义的自然数，像这样：如果需要

data Nat = Z | S Nat 

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

这将解除纳特到那种水平和S和Z为类型级别：

data Nat = Z | S Nat

搭配建议你可以写这样的事情。所以纳特是另一种类型，并且与*相同。

下面是布伦特Yorgey

Typed type-level functional programming in GHC

来源

2011-10-13 11:32:41 raichoo

更新：ghc 7.4.1通过PolyKinds和DataKinds扩展支持这一点。 – raichoo

类型理论：型种

回答

相关问题