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为表示自然数的单例类型.succthen 的返回类型取决于此值,其中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.因此,这里的单例类型提供了一种Π类型,其中Haskell succ :: ?n:Nat . n -> S(n)中的参数succ提供依赖的产品参数n:Nat(作为类型参数传递)然后提供参数值.