Singleton types in Haskell

Question

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.

Answer 1

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.