haskell - imprimir - ¿Cuál es el significado de los tipos de datos algebraicos con cero constructores?

imprimir en haskell

Question

Este pasaje, que lamentablemente carece de referencias, sobre el desarrollo de los ADT en Haskell, de A History of Haskell: Being Lazy With Class , sección 5.1:

En general, un tipo algebraico especifica una suma de una o más alternativas, donde cada alternativa es un producto de cero o más campos. Podría haber sido útil permitir una suma de cero alternativas, que sería un tipo completamente vacío, pero en el momento en que no se apreció el valor de dicho tipo.

me deja pensando, ¿cómo sería útil un TDA?

Answer 1

Entre los correspondientes al falso lógico (como se indica en otra respuesta), a menudo se utilizan para crear restricciones de tipo adicionales en combinación con GADT . Por ejemplo:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyDataDecls #-}

import Data.List (groupBy)

data Zero
data Succ n

data Vec n a where
    Nil  ::                 Vec Zero a
    Cons :: a -> Vec n a -> Vec (Succ n) a

vhead :: Vec (Succ n) a -> a
vhead (Cons v _) = v

vtail :: Vec (Succ n) a -> Vec n a
vtail (Cons _ v) = v

Aquí tenemos dos tipos de datos sin constructor. Su significado aquí es simplemente representar números naturales: Zero , Succ Zero , Succ (Succ Zero) etc. Se usan como tipos fantasma en el tipo de datos Vec para que podamos codificar la longitud de un vector en su tipo. Entonces, podemos escribir funciones seguras de tipo como vhead / vtail que se pueden aplicar solo a vectores no vacíos.

Ver también [Haskell] Vectores de longitud fija en Haskell, Parte 1: Usar GADT donde el ejemplo se elabora en detalle.

Answer 2

Los tipos sin constructores se llaman tipos fantasmas . Vea la página en la wiki de Haskell .

Answer 3

No hay forma de construir un valor "real" de un tipo sin constructor (donde por "real" me refiero a un cómputo de terminación; Haskell undefined :: a ha undefined :: a , error :: String -> a y la posibilidad de escribir programas no determinantes) como mwahaha = mwahaha , que para simplificar llamaré valores "falsos").

Un ejemplo de cómo esto puede ser útil son las versiones 0.5 y posteriores de la biblioteca de conductos . El tipo básico en la biblioteca es Pipe lioumr ; con diferentes parámetros para estos tipos, un Pipe puede servir como fuente (que produce salida sin consumir ninguna entrada), un sumidero (consume entrada sin producir ninguna salida) o un conducto (consume entrada y produce salida). Los parámetros de tipo i y o para Pipe son los tipos de su entrada y salida, respectivamente.

Por lo tanto, una de las formas en que la biblioteca de conductos aplica la noción de que las fuentes no consumen entradas y sumideros no produce salida al usar el tipo Void de Data.Void como tipo de entrada para fuentes y tipo de salida para receptores. Nuevamente, no existe una forma definitiva de construir un valor de ese tipo, por lo que un programa que intente consumir la salida de un receptor no terminará (lo cual, como recordatorio, en Haskell esto puede significar "generar un error" y no necesariamente "). bucle por siempre ").

Answer 4

Teóricamente: el isomorfismo de Curry-Howard nos da una interpretación de este tipo como la proposición "falsa". "falso" es útil como una proposición en sí misma; pero también es útil para construir el combinador "no" (como type Not a = a -> False ) y otras construcciones similares.

Pragmáticamente: este tipo se puede usar para evitar la creación de ciertas ramas de tipos de datos parametrizados. Por ejemplo, he usado esto en una biblioteca para analizar varios árboles de juego algo como esto:

data RuleSet a            = Known !a | Unknown String
data GoRuleChoices        = Japanese | Chinese
data LinesOfActionChoices -- there are none in the spec!
type GoRuleSet            = RuleSet GoRuleChoices
type LinesOfActionRuleSet = RuleSet LinesOfActionChoices

El impacto de esto es que, al analizar un árbol de juegos de Líneas de Acción, si hay un conjunto de reglas especificado, sabemos que su constructor será Unknown y puede dejar otras ramas apagadas durante las coincidencias de patrones, etc.