haskell - Haskell 中的单例类型

Question

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

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

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

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

Answer 1

正如您所描述的，单例类型是只有一个值的类型(暂时忽略⊥)。因此，单例类型的值具有表示该值的唯一类型。依赖类型理论 (DTT) 的关键在于类型可以依赖于值(或者，换句话说，值可以参数化类型)。允许类型依赖于类型的类型理论可以使用单例类型来让类型依赖于单例值。相反，类型类提供临时多态性，其中值可以依赖于类型(与 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) succ 的参数在哪里在 Haskell 中提供了依赖产品参数 n:Nat (作为类型参数传递)，然后是参数值。