scala – 类型理论：类型

发布时间：2020-12-16 09:48:13 所属栏目：安全来源：网络整理

导读：我读了很多有关类型，更高类型的有趣的东西等等。默认情况下Haskell支持两种类型：简单类型：* 类型构造函数：*→* 最新GHC的语言扩展ConstraintKinds增加了新的类型：类型参数约束：约束此外，阅读this mailing list后，变得清楚，另一种类型可能存在，

我读了很多有关类型，更高类型的有趣的东西等等。默认情况下Haskell支持两种类型：

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

最新GHC的语言扩展ConstraintKinds增加了新的类型：

>类型参数约束：约束

此外，阅读this mailing list后，变得清楚，另一种类型可能存在，但GHC不支持(但这种支持在.NET中实现)：

>取消装箱的类型：#

我学到了polymorphic kinds，我想我已经明白了这个想法。 Haskell也支持显式定量化。

所以我的问题是：

>有没有其他类型的种类存在？
>什么是其他类型相关的语言特性存在？
> subkinding是什么意思？它在哪里实现/有用？
>有没有类型系统的种类，类型是类型系统的类型？ (只是有趣)

解决方法

是的，存在其他种类。页面 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)

意图是最后一个类型参数应该只是零或Succ n，其中n再次只是零或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)

这将允许类型检查器在它接受什么更多的歧视，以及使类型级编程更加表达。

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!