haskell - Haskell单例:SNat有什么好处

Question

我想让Haskell单例感到沮丧。

在纸上Dependently Typed Programming with Singletons
在他的博客文章singletons v0.9 Released!中
Richard Eisenberg定义了数据类型Nat，该数据类型使用peano公理定义了自然数:

data Nat = Zero | Succ Nat

通过使用语言扩展DataKinds，此数据类型被提升为类型级别。
数据构造器Zero和Succ被提升为类型构造器'Zero和'Succ。
这样，我们就可以为每个自然数在类型级别上获得一个唯一的对应类型。例如，对于3，我们得到'Succ('Succ('Succ'零))。
因此，我们现在将自然数作为类型。

然后，他在值级别定义函数plus，在类型级别定义type family Plus
使附加操作可用。
借助单例库的提升功能/准四方，我们可以自动
从plus函数创建Plus类型族。因此，我们可以避免自己编写类型家族。

到现在为止还挺好!

使用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'数量更多的琐碎问题引发了 war )
Nat类型的运行时值在类型级别上是无法区分的。 Haskell类型系统当前具有替换属性，这意味着在任何类型良好的程序中，您都可以用具有相同范围和类型的替代子表达式替换任何类型良好的子表达式，并且程序将继续进行类型良好。例如，您可以重写每次出现的

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

至

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

而且您可以确定不会出错...检查程序类型的结果。

替换属性(property)是一个尴尬。明确的证据表明您的类型系统在意义开始重要的那一刻就放弃了。

现在，Nat通过成为运行时值的数据类型，也成为类型级别值'Zero和'Suc的类型。后者仅使用Haskell的类型语言生活，根本没有运行时状态。请注意，尽管'Zero和'Suc存在于类型级别，但是将它们称为“类型”是无济于事的，并且目前这样做的人应该停止使用。它们没有*类型，因此无法对值进行分类，这是值得命名的类型。

在运行时和类型级别的Nat之间没有直接的交换方式，这很麻烦。范式示例涉及对 vector 的关键操作:

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

我们可能想计算给定元素的副本 vector (可能作为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)

Singleton通过利用唯一一种可以优化类型信息的运行时分析形式，使我们能够弥合运行时与类型级别数据之间的鸿沟。怀疑它们是否真的必要，并且目前是否有必要，只是因为这一差距尚未消除，这是非常明智的。