Haskell单身汉:我们用SNat得到什么？

Question

我在试着格洛克·哈斯克尔单身。

在论文带单子的依赖型程序设计和他的博客文章中，Richard定义了数据类型Nat，它用peano公理来定义自然数：

data Nat = Zero | Succ Nat

通过使用语言扩展DataKinds，将此数据类型提升到类型级别。将数据结构函数Zero和Succ提升为类型构造函数'Zero‘和'Succ’，对每个自然数在类型级别上得到一个唯一的对应类型，例如，对于3，我们得到'Succ ( 'Succ‘Zero)，所以现在我们把自然数作为类型。

然后，他在值级别定义函数加号，在类型级别定义类型族加号，以使加法操作可用。通过使用单例库的促进函数/准数量，我们可以从加号函数自动创建加号类型家族。这样我们就可以避免编写类型的家族自助式。

到目前一切尚好!

使用GADT语法，他还定义了数据类型SNat。

data SNat :: Nat -> * where
  SZero :: SNat Zero
  SSucc :: SNat n -> SNat (Succ n)

基本上，他只将Nat类型封装到一个SNat构造函数中。为什么有这个必要？我们能得到什么？数据类型Nat和SNat不是同构的吗？为什么SNat是独生子女，为什么Nat不是单身？在这两种情况下，每种类型都有一个单独的值，对应的自然数。

Answer 1

我们能得到什么？嗯。单身人士的地位是尴尬的，但目前是必要的解决办法，我们越早能够消除他们，越好。

让我看看能不能弄清楚这幅画。我们有一个数据类型Nat

data Nat = Zero | Suc Nat

(战争的起因甚至比Suc中的c‘s数量还要小)

类型Nat具有在类型级别上难以区分的运行时值。Haskell类型系统当前具有替换属性，这意味着在任何类型良好的程序中，您可以使用具有相同范围和类型的可选子表达式替换任何类型良好的子表达式，并且程序将继续是良好类型的。例如，您可以重写

if <b> then <t> else <e>

至

if <b> then <e> else <t>

而且，您可以肯定，没有什么会wrong...with的结果，检查您的程序的类型。

替换财产令人尴尬。这清楚地证明，在意义开始重要的时刻，你的类型系统就放弃了。

现在，通过成为运行时值的数据类型，Nat也成为了类型级别值'Zero和'Suc的类型。后者只使用Haskell的类型语言，根本没有运行时存在。请注意，虽然'Zero和'Suc存在于类型级别，但是将它们称为“类型”是没有帮助的，而目前这样做的人应该停止使用。它们没有*类型，因此不能对值进行分类，这就是值得命名的类型。

在运行时和类型级别的Nat之间没有直接的交换手段，这可能会带来麻烦。范例示例涉及向量上的一个关键操作。

data Vec :: Nat -> * -> * where
  VNil   :: Vec 'Zero x
  VCons  :: x -> Vec n x -> Vec ('Suc n) x

我们可能希望计算给定元素的副本的向量(可能作为Applicative实例的一部分)。也许给出这种类型的

vec :: forall (n :: Nat) (x :: *). x -> Vec n x

但这有可能奏效吗？为了复制某些东西的n副本，我们需要在运行时了解n：程序必须决定是部署VNil和停止，还是部署VCons并继续运行，它需要一些数据来完成。一个很好的线索是forall量化器，它是参数化的:它表明量化的信息只对类型可用，并且被运行时擦除。

Haskell目前在依赖量化( forall所做的)和运行时擦除之间强制执行一个完全虚假的巧合。它不支持依赖的但不擦除的量词，我们通常称之为pi。vec的类型和实现应该类似于

vec :: pi (n :: Nat) -> forall (x :: *). Vec n x
vec 'Zero    x = VNil
vec ('Suc n) x = VCons x (vec n x)

其中，pi-positions中的参数是用类型语言编写的，但是在运行时数据是可用的。

那我们该怎么办呢？我们使用单例间接捕获类型级别数据的运行时副本意味着什么。

data SNat :: Nat -> * where
  SZero :: SNat Zero
  SSuc  :: SNat n -> SNat (Suc n)

现在，SZero和SSuc创建了运行时数据。SNat与Nat不是同构的:前者是Nat -> *型，后者是*型，因此试图使它们同构是一种类型错误。在Nat中有许多运行时值，类型系统没有区分它们；在每个不同的SNat n中都有一个运行时值(值得一说)，所以类型系统无法区分它们这一事实是无关紧要的。要点是，每个SNat n对于每个不同的n都是不同的类型，而GADT模式匹配(其中一个模式可以是一个更具体的GADT类型的实例，它已知是匹配的)可以改进我们对n的了解。

我们现在可以写

vec :: forall (n :: Nat). SNat n -> forall (x :: *). x -> Vec n x
vec SZero    x = VNil
vec (SSuc n) x = VCons x (vec n x)

单例允许我们通过利用允许细化类型信息的运行时分析的唯一形式来弥合运行时和类型级数据之间的差距。想知道它们是否真的有必要是非常明智的，而现在正是如此，只是因为这一差距还没有被消除。