Haskell单例：SNat有什么好处

Question

Haskell单例：SNat有什么好处

haskelldependent-typetype-level-computationsingleton-type

22

我正在尝试理解Haskell的单例模式。

在论文《使用单例的依赖类型编程》和他的博客文章《发布0.9版的单例模式！》中， Richard Eisenberg定义了数据类型Nat，它使用Peano公理定义了自然数：

data Nat = Zero | Succ Nat

通过使用语言扩展，这种数据类型被提升到类型层。数据构造器和被提升为类型构造器<'Zero>和<'Succ>。因此，对于每个自然数，在类型层上都有一个单一且唯一的对应类型。例如，对于<3>，我们得到<'Succ ( 'Succ ( 'Succ 'Zero))>。现在我们把自然数作为类型。

然后他在值级别上定义了函数，在类型级别上定义了类型族，以便使用加法操作。借助单例库的函数/宏，我们可以自动创建类型族，而无需手动编写类型族。

到目前为止还不错！

他还使用GADT语法定义了一个名为的数据类型：

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

基本上，他只是将Nat类型封装到一个SNat构造器中。为什么这是必要的？我们会得到什么？ Nat和SNat数据类型不是同构的吗？为什么SNat是单例而Nat不是单例？在两种情况下，每种类型都由一个单一值所占据，即相应的自然数。

- Jogger

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- pigworker · Accepted Answer

我们获得了什么？嗯。单例的状态是一个尴尬但目前必需的解决方法，我们越早摆脱它们，就越好。

让我看看能否澄清这个画面。我们有一个数据类型Nat：

data Nat = Zero | Suc Nat

(甚至有些战争是因为“Suc”里C的数量而爆发的)

Nat类型在运行时无法从类型层面上区分其值。Haskell类型系统目前具有“替换”性质，这意味着在任何良好类型化的程序中，您可以用一个具有相同作用域和类型的备用子表达式替换任何良好类型化的子表达式，并且程序仍然能够良好地类型化。例如，您可以重写每个出现的

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

到

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

你可以放心，检查程序类型的结果不会出错。

替换属性是一种尴尬的情况。这清楚地证明了你的类型系统在意义开始变得重要的时候就放弃了。

现在，通过成为运行时值的数据类型，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 实例的一部分）。为了达成这个目的，给出下面的类型定义可能是一个好主意：

```haskell ```

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位置的参数，但数据在运行时可用。

那么我们该怎么办呢？我们使用单例间接捕获“运行时类型级别数据的副本”的含义。

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

现在，SZero和SSuc生成运行时数据。 SNat与Nat不同构：前者具有类型Nat -> *，而后者具有类型*，因此尝试使它们同构是一种类型错误。在Nat中有许多运行时值，并且类型系统无法区分它们；对于每个不同的SNat n，恰好有一个（值得一提的）运行时值，因此，类型系统不能区分它们是无关紧要的。重点是每个不同的n都为每个SNat 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)

单例允许我们通过利用唯一一种运行时分析形式来细化类型信息，从而弥合运行时和类型级别数据之间的差距。人们很自然地会想知道它们是否真的必要，并且它们目前仍然是必需的，仅因为那个差距尚未被消除。