Haskell singletons: ¿Qué ganamos con SNat?
dependent-type type-level-computation (1)
Estoy tratando de tragarme las cartas de Haskell.
¡En el periódico Dependently Typed Programming with Singletons y en su blog singletons v0.9 Released! Richard Eisenberg define el tipo de datos Nat que define números naturales con los axiomas peano:
data Nat = Zero | Succ Nat
Al utilizar la extensión de idioma DataKinds, este tipo de datos se promueve al nivel de tipo. Los constructores de datos Zero y Succ se promueven a los constructores de tipo ''Cero y '' Succ . Con esto obtenemos para cada Número natural un tipo correspondiente único y único en el nivel de tipo. Por ejemplo, para 3 obtenemos ''Succ ('' Succ (''Succ'' Zero)) . Así que ahora tenemos números naturales como tipos.
A continuación, define en el nivel de valor la función más y en el nivel de tipo la familia de tipos Más para tener disponible la operación de adición. Con la función de promoción / quasiqoter de la biblioteca de singletons podemos crear automáticamente la familia de tipos Plus a partir de la función más . Así que podemos evitar escribir el tipo familia nosotros mismos.
¡Hasta ahora tan bueno!
Con la sintaxis de GADT también define un tipo de datos SNat :
data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
Básicamente, solo envuelve el tipo Nat en un constructor SNat . ¿Por qué es esto necesario? ¿Qué ganamos? ¿Los tipos de datos Nat y SNat no son isomorfos? ¿Por qué es SNat un singleton, y por qué Nat no es un singleton? En ambos casos, cada tipo está habitado por un solo valor, el número natural correspondiente.
¿Qué ganamos? Hmm El estado de singletons es el de una solución torpe pero necesaria en la actualidad , y cuanto antes podamos eliminarlos, mejor.
Déjame ver si puedo aclarar la imagen. Tenemos un tipo de datos Nat :
data Nat = Zero | Suc Nat
(Las guerras se han iniciado con problemas aún más triviales que la cantidad de ''C'' en Suc ).
El tipo Nat tiene valores de tiempo de ejecución que no se pueden distinguir en el nivel de tipo. El sistema tipo Haskell actualmente tiene la propiedad de reemplazo , lo que significa que en cualquier programa bien escrito, puede reemplazar cualquier subexpresión bien tipeada por una subexpresión alternativa con el mismo alcance y tipo, y el programa continuará tipándose correctamente. Por ejemplo, puede volver a escribir cada aparición de
if <b> then <t> else <e>
a
if <b> then <e> else <t>
y puede estar seguro de que nada saldrá mal ... con el resultado de verificar el tipo de su programa.
La propiedad de reemplazo es una vergüenza. Es una clara prueba de que su sistema de tipos se rinde en el momento en que el significado comienza a importar.
Ahora, al ser un tipo de datos para los valores en tiempo de ejecución, Nat también se convierte en un tipo de valores de nivel de tipo ''Zero y ''Suc . Los últimos viven solo en el lenguaje tipográfico de Haskell y no tienen presencia en el tiempo de ejecución. Tenga en cuenta que aunque ''Zero y ''Suc existen en el nivel de tipo, no es útil referirse a ellos como "tipos" y las personas que actualmente lo hacen deben desistir. No tienen tipo * y, por lo tanto, no pueden clasificar valores, que es lo que hacen los tipos dignos de ese nombre.
No hay ningún medio de intercambio directo entre el tiempo de ejecución y el nivel de tipo Nat , lo que puede ser una molestia. El ejemplo paradigmático se refiere a una operación clave en vectores :
data Vec :: Nat -> * -> * where
VNil :: Vec ''Zero x
VCons :: x -> Vec n x -> Vec (''Suc n) x
Nos gustaría calcular un vector de copias de un elemento dado (tal vez como parte de una instancia del Applicative ). Podría parecer una buena idea dar el tipo
vec :: forall (n :: Nat) (x :: *). x -> Vec n x
¿Pero eso puede funcionar? Para hacer n copias de algo, necesitamos saber n en el tiempo de ejecución: un programa tiene que decidir si implementar VNil y detener o implementar VCons y seguir adelante, y necesita algunos datos para hacerlo. Una buena pista es el cuantificador forall , que es paramétrico : indica que la información cuantificada está disponible solo para los tipos y se borra por el tiempo de ejecución.
Haskell actualmente impone una coincidencia totalmente espuria entre la cuantificación dependiente (lo que hace todo) y el borrado del tiempo de ejecución. No admite un cuantificador dependiente pero no borrado, que a menudo llamamos pi . El tipo y la implementación de vec debería ser algo como
vec :: pi (n :: Nat) -> forall (x :: *). Vec n x
vec ''Zero x = VNil
vec (''Suc n) x = VCons x (vec n x)
donde los argumentos en las posiciones pi se escriben en el lenguaje de tipo, pero los datos están disponibles en tiempo de ejecución.
Entonces, ¿qué hacemos en su lugar? Usamos singletons para capturar indirectamente lo que significa ser una copia en tiempo de ejecución de los datos de nivel de tipo .
data SNat :: Nat -> * where
SZero :: SNat Zero
SSuc :: SNat n -> SNat (Suc n)
Ahora, SZero y SSuc hacen datos en tiempo de ejecución. SNat no es isomorfo a Nat : el primero tiene el tipo Nat -> * , mientras que el segundo tiene el tipo * , por lo que es un error de tipo tratar de hacerlos isomorfos. Hay muchos valores de tiempo de ejecución en Nat , y el sistema de tipos no los distingue; hay exactamente un valor de tiempo de ejecución (vale la pena hablar de) en cada SNat n diferente, por lo que el hecho de que el sistema de tipos no pueda distinguirlos está al lado del punto. El punto es que cada SNat n es un tipo diferente para cada n diferente, y que la coincidencia de patrones GADT (donde un patrón puede ser de una instancia más específica del tipo GADT que se sabe que coincide) puede refinar nuestro conocimiento de n .
Ahora podemos escribir
vec :: forall (n :: Nat). SNat n -> forall (x :: *). x -> Vec n x
vec SZero x = VNil
vec (SSuc n) x = VCons x (vec n x)
Los Singletons nos permiten cerrar la brecha entre el tiempo de ejecución y los datos de nivel de tipo, mediante la explotación de la única forma de análisis de tiempo de ejecución que permite el refinamiento de la información de tipo. Es bastante sensato preguntarse si son realmente necesarios, y actualmente lo son, solo porque esa brecha aún no se ha eliminado.