Haskell Singletons：我们从SNat中得到了什么

Question

data Nat = Zero | Succ Nat

到目前为止还不错！

使用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'数更琐碎）

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

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

在运行时和类型级的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量词，它是参数的：它表示量化的信息只对类型可用，并且被运行时擦除。

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

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

现在，szero和ssuc生成运行时数据。SNAT与NAT不同构：前者具有NAT->*类型，而后者具有*类型，因此试图使它们同构是一种类型错误。NAT中有许多运行时值，类型系统不区分它们；在每个不同的snatn中正好有一个运行时值（值得一提），因此类型系统无法区分它们的事实是无关紧要的。关键是每个SNATn对于每个不同的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)

单例允许我们在运行时和类型级数据之间架起桥梁，它利用了运行时分析的唯一形式，可以细化类型信息。想知道它们是否真的有必要是相当明智的，而它们目前是必要的，只是因为这一差距尚未消除。