Tipos de Singleton en Haskell

dependent-type type-theory

Question

Como parte de una encuesta sobre varias técnicas de formalización tipificadas de manera dependiente, encontré un artículo que aboga por el uso de tipos singleton (tipos con un habitante) como una forma de apoyar la programación tipificada de manera dependiente.

De acuerdo con esta fuente, en Haskell, hay una separación entre los valores de tiempo de ejecución y los tipos de tiempo de compilación que se pueden difuminar cuando se usan tipos singleton, debido al isomorfismo de tipo / valor inducido.

Mi pregunta es: ¿en qué se diferencian los tipos singleton de las clases de tipo o de las estructuras citadas / reificadas a este respecto?

También apreciaría particularmente alguna explicación intuitiva con respecto a la importancia / ventajas teóricas del tipo al usar tipos singleton y en la medida en que pueden emular tipos dependientes en general.

Answer 1

Como usted describe, los tipos singleton son aquellos que tienen un solo valor (ignoremos ⊥ por el momento). Por lo tanto, el valor de un tipo singleton tiene un tipo único que representa el valor. El quid de la teoría de los tipos dependientes (DTT) es que los tipos pueden depender de los valores (o, dicho de otra manera, los valores pueden parametrizar tipos). Una teoría de tipos que permite que los tipos dependan de tipos puede usar tipos singleton para permitir que los tipos dependan de valores singleton. En contraste, las clases de tipos proporcionan un polimorfismo ad hoc , donde los valores pueden depender de los tipos (al revés de la TDT donde los tipos dependen de los valores).

Una técnica útil en Haskell es definir una clase de tipos singleton relacionados. El ejemplo clásico es de números naturales:

data S n = Succ n 
data Z = Zero

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

Siempre que no se agreguen más instancias a Nat , la clase Nat describe tipos singleton cuyos valores / tipos son números naturales definidos inductivamente. Tenga en cuenta que, Zero es el único habitante de Z pero el tipo S Int , por ejemplo, tiene muchos habitantes (no es un singleton); La clase Nat restringe el parámetro de S a tipos singleton. Intuitivamente, cualquier tipo de datos con más de un constructor de datos no es un tipo singleton.

Dando lo anterior, podemos escribir la función de sucesor de tipo dependiente:

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

En la firma de tipo, la variable de tipo n puede verse como un valor, ya que la restricción Nat n restringe n a la clase de tipos singleton que representan números naturales. El tipo de retorno de succ depende de este valor, donde S está parametrizado por el valor n .

Cualquier valor que se pueda definir de forma inductiva puede recibir una representación única de tipo singleton.

Una técnica útil es utilizar GADT para parametrizar tipos no singleton con tipos singleton (es decir, con valores). Esto se puede usar, por ejemplo, para dar una representación a nivel de tipo de la forma de un tipo de datos definido inductivamente. El ejemplo clásico es una lista clasificada:

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

Aquí los tipos singleton de número natural parametrizan el tipo de lista por su longitud.

Pensando en términos del cálculo lambda polimórfico, succ anterior toma dos argumentos, el tipo n y luego un parámetro de valor del tipo n . Por lo tanto, los tipos singleton aquí proporcionan un tipo de tipo Π-type , donde succ :: Πn:Nat . n -> S(n) succ :: Πn:Nat . n -> S(n) donde el argumento a succ en Haskell proporciona tanto el parámetro de producto dependiente n:Nat (pasado como el parámetro de tipo) y luego el valor del argumento.