类型理论:类型种类

Question

我已经阅读了很多有关类型,高级类型等等的有趣内容.默认情况下,Haskell支持两种类型:

• 简单类型: *
• 类型构造函数: * ? *

最新的GHC语言扩展ConstraintKinds增加了一种新的:

• 类型参数约束: Constraint

在阅读这个邮件列表后,很明显可能存在另一种类型,但GHC不支持它(但这种支持是在.NET中实现的):

• 未装箱类型: #

我已经了解了多态种类,我想我理解这个想法.Haskell也支持明确的kinded量化.

所以我的问题是:

• 是否存在其他类型的种类？
• 还有其他类似的语言功能吗？
• 什么subkinding意思？它在哪里实施/有用？
• 是否有一个类型系统kinds,就像kinds一个类型系统在上面types？(只是感兴趣)

Answer 1

是的,存在其他种类.中间类型页面描述了GHC中使用的其他类型(包括未装箱类型和一些更复杂的类型).Ωmega语言将更高级的类型转换为最大逻辑扩展,允许用户可定义的类型(和排序,以及更高). 这个页面为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数据类型可以表示最后一个参数不是a *,而是a Nat,就像

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

这将允许类型检查器在它接受的内容中更具辨别力,以及使类型级编程更具表现力.

Answer 2

正如类型按类别分类一样,种类也按类别分类.

Ωmega编程语言在任何级别都有一个用户可定义种类的系统.(所以说它的wiki.我认为它指的是上面的种类和级别,但我不确定.)

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 

这是一个Vector,它的维度在类型中编码.我们使用Z和S来生成自然数.这很好但是如果我们在生成Vec时使用正确的类型(我们可能会意外地切换内容类型的长度),我们就不能"打字检查",我们还需要生成一个S和Z类型,如果我们已经很不方便定义了这样的自然数:

data Nat = Z | S 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

如果需要,这会将Nat提升到类型级别,将S和Z提升到类型级别.所以Nat是另一种,与*一样生活在同一水平.

以下是Brent Yorgey的演讲

在GHC中键入类型级函数编程