Haskell中的单身类型 [英] Singleton types in Haskell

问题描述

作为对各种依赖类型形式化技术进行调查的一部分，我曾经发表过一篇文章，提倡使用单身人士类型（与一个居民一起使用的类型）作为支持依赖类型编程的一种方式。 $ b $根据这个源代码，在Haskell中，运行时值和编译时类型之间存在分离，由于类型/值同构的原因，在使用单例类型时可能会模糊。

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

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

解决方案

正如你所描述的，单身类型是那些只有一个值的类型（让我们忽略⊥暂时）。因此，单例类型的值具有表示该值的唯一类型。依赖型理论（DTT）的关键是类型可以依赖于值（或者，换言之，值可以参数化类型）。允许类型依赖于类型的类型理论可以使用单例类型来让类型依赖于单例值。相反，type类提供了特别的多态，其中值可以依赖于类型（DTT的类型依赖于值的其他方式）。

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

  data S n = Succ n 
 data Z = Zero 
 
类Nat n 
实例Nat Z 
实例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 。

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

一个有用的技术是使用GADT来参数化具有单例类型的非单例类型（即带有值）。例如，这可以用来给出感应定义数据类型形状的类型级别表示。经典的例子是大小清单：

 数据列出其中
无::列表Z a 
 Cons :: Nat n => a  - >列表n a  - > List（S n）a 
  

这里自然数singleton类型通过它的长度参数化列表类型。

根据多态lambda演算的思想，上面的 succ 有两个参数，类型为 n ，然后是 n 类型的值参数。因此，这里的单身人士类型提供了一种Π型，其中 succ ::Πn：Nat。 n - > S（n）其中Haskell中 succ 的参数提供了相关产品参数 n：Nat （作为类型参数传递），然后是参数值。

As part of doing a survey on various dependently typed formalization techniques, I have ran across a paper advocating the use of singleton types (types with one inhabitant) as a way of supporting dependently typed programming.

Acording to this source, in Haskell, there is a separation betwen runtime values and compile-time types that can be blurred when using singleton types, due to the induced type/value isomorphism.

My question is: How do singleton types differ from type-classes or from quoted/reified structures in this respect?

I would also particularly appreciate some intuitive explaination with respect to the type-theoretical importance/advantages to using singleton types and to the extent to which they can emulate dependent types in general.

解决方案

As you describe, singleton types are those which have only one value (let's ignore ⊥ for the moment). Thus, the value of a singleton type has a unique type representing the value. The crux of dependent-type theory (DTT) is that types can depend on values (or, said another way, values can parameterise types). A type theory that allows types to depend on types can use singleton types to let types depend on singleton values. In contrast, type classes provide ad hoc polymorphism, where values can depend on types (the other way round to DTT where types depend on values).

A useful technique in Haskell is to define a class of related singleton types. The classic example is of natural numbers:

data S n = Succ n 
data Z = Zero

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

Provided further instances aren't added to Nat, the Nat class describes singleton types whose values/types are inductively defined natural numbers. Note that, Zero is the only inhabitant of Z but the type S Int, for example, has many inhabitants (it is not a singleton); the Nat class restricts the parameter of S to singleton types. Intuitively, any data type with more than one data constructor is not a singleton type.

Give the above, we can write the dependently-typed successor function:

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

In the type signature, the type variable n can be seen as a value since the Nat n constraint restricts n to the class of singleton types representing natural numbers. The return type of the succ then depends on this value, where S is parameterised by the value n.

Any value that can be inductively defined can be given a unique singleton type representation.

A useful technique is to use GADTs to parameterise non-singleton types with singleton types (i.e. with values). This can be used, for example, to give a type-level representation of the shape of an inductively defined data type. The classic example is a sized-list:

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

Here the natural number singleton types parameterise the list-type by its length.

Thinking in terms of the polymorphic lambda calculus, succ above takes two arguments, the type n and then a value parameter of type n. Thus, singleton types here provides a kind of Π-type, where succ :: Πn:Nat . n -> S(n) where the argument to succ in Haskell provides both the dependent product parameter n:Nat (passed as the type parameter) and then the argument value.

这篇关于Haskell中的单身类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！