Haskell 中的单例类型

Question

作为对各种依赖类型形式化技术进行调查的一部分，我看到一篇论文提倡使用单例类型（有一个居民的类型）作为支持依赖类型编程的一种方式。

根据这个来源，在 Haskell 中，由于引入的类型/值同构，在使用单例类型时，运行时值和编译时类型之间存在分离。

我的问题是：在这方面，单例类型与类型类或引用/具体化结构有何不同？

我还特别感谢一些关于使用单例类型的类型理论重要性/优势以及它们可以在多大程度上模拟一般依赖类型的直观解释。

Answer 1

正如您所描述的，单例类型是只有一个值的类型（我们暂时忽略⊥）。因此，单例类型的值具有表示该值的唯一类型。依赖类型理论 (DTT) 的关键在于类型可以依赖于值（或者，换句话说，值可以参数化类型）。允许类型依赖于类型的类型理论可以使用单例类型来让类型依赖于单例值。相比之下，类型类提供 ad hoc 多态性，其中值可以依赖于类型（与 DTT 相反，其中类型依赖于值）。

Haskell 中一个有用的技术是定义一类相关的单例类型。经典的例子是自然数：

data S n = Succ n 
data Z = Zero

class Nat n 
instance Nat Z
instance Nat n => Nat (S n)

如果没有向Nat 添加更多实例，Nat 类描述了其值/类型是归纳定义的自然数的单例类型。请注意，Zero 是 Z 的唯一居民，但例如 S Int 类型有很多居民（它不是单例）； Nat 类将 S 的参数限制为单例类型。直观地说，任何具有多个数据构造函数的数据类型都不是单例类型。

给定上面，我们可以写出依赖类型的后继函数：

succ :: Nat n => n -> (S n)
succ n = Succ n 

在类型签名中，类型变量n 可以被视为一个值，因为Nat n 约束将n 限制为表示自然数的单例类型类。 succ 的返回类型取决于这个值，其中S 由值n 参数化。

任何可以归纳定义的值都可以被赋予唯一的单例类型表示。

一种有用的技术是使用 GADT 将非单例类型参数化为单例类型（即使用值）。例如，这可以用于给出归纳定义的数据类型的形状的类型级表示。经典的例子是一个大小列表：

data List n a where
   Nil :: List Z a 
   Cons :: Nat n => a -> List n a -> List (S n) a

这里的自然数单例类型通过其长度参数化列表类型。

考虑到多态 lambda 演算，上面的 succ 有两个参数，n 类型，然后是 n 类型的值参数。因此，这里的单例类型提供了一种Π-type，其中succ :: Πn:Nat . n -> S(n)，其中Haskell 中succ 的参数提供了依赖产品参数n:Nat（作为类型参数传递）和参数值。