data - ¿Qué es[](list constructor) en Haskell?

eq haskell

Question

Estoy teniendo problemas para entender los funtores, específicamente lo que es un tipo concreto en LYAH. Creo que esto se debe a que no entiendo qué [] realmente es.

fmap :: (a -> b) -> f a -> f b  

1. ¿Es [] , un constructor de tipos? O bien, ¿es un constructor de valor?
2. ¿Qué significa tener el tipo de: [] :: [a] ?
3. ¿Es como Maybe type-constructor o Just value constructor?
   1. Si es así, Just cómo es que Just tiene una firma como Just :: a -> Maybe a más que Just :: Maybe a , en otras palabras, por qué no está [] tipeado [] :: a -> [a]
4. LYAH dice esto como se aplica a los funtores: Fíjate cómo no escribimos la instancia Functor [a] donde, porque desde fmap :: (a -> b) -> fa -> fb, vemos que f tiene que ser un tipo constructor que toma un tipo. [a] ya es un tipo concreto (de una lista con cualquier tipo dentro), mientras que [] es un constructor de tipo que toma un tipo y puede producir tipos como [Int], [String] o incluso [[String]] . Estoy confundido, aunque el tipo de [] implica que es como un literal para [a] ¿a qué intenta llegar LYAH?

Answer 1

1. es un constructor de tipo (por ejemplo [Int] es un tipo), y un constructor de datos ([2] es una estructura de lista).
2. La lista vacía es una lista que contiene cualquier tipo
3. [a] es como Maybe a, [2] es como Just 2.
4. [] es una función cero-aria (una constante) por lo que no tiene tipo de función.

Answer 2

Solo para hacer las cosas más explícitas, este tipo de datos:

data List a = Cons a (List a) 
            | Nil

... tiene la misma estructura que el tipo de lista incorporada, pero sin la sintaxis especial (más agradable, pero potencialmente confusa). Esto es lo que parecen algunas correspondencias:

• List = [] , escribe constructores con kind * -> *
• List a = [a] , tipos con tipo *
• Nil = [] , valores con tipos polimórficos List a y [a] respectivamente
• Cons = : constructores de datos con tipos a -> List a -> List a y a -> [a] -> [a] respectivamente
• Cons 5 Nil = [5] o 5:[] , listas de elementos individuales
• f Nil = ... = f [] = ... , coincidencia de patrones con listas vacías
• f (Cons x Nil) = ... = f [x] = ... `, listas de elementos de coincidencia de patrones
• f (Cons x xs) = ... = f (x:xs) = ... , coincidencia de patrones de listas no vacías

De hecho, si preguntas a ghci sobre [] , te dice más o menos la misma definición:

> :i []
data [] a = [] | a : [a]           -- Defined in GHC.Types

Pero usted no puede escribir esa definición usted mismo porque la sintaxis de la lista y su constructor de tipo "outfix" es un caso especial, definido en la especificación del idioma.

Answer 3

1. Es (de manera confusa, te lo concedo) sobrecargado sintácticamente para ser tanto un constructor de tipo como un constructor de valor.

2. Significa que (el constructor de valor) [] tiene el tipo que, para todos los tipos a , es una lista de a (que se escribe [a] ). Esto se debe a que hay una lista vacía en cada tipo.

3. El constructor de valor [] no está escrito a -> [a] porque la lista vacía no tiene elementos, y por lo tanto no necesita a para hacer una lista vacía de a ''s. Comparar con Nothing :: Maybe a lugar.

4. LYAH está hablando del constructor de tipos [] con kind * -> * , a diferencia del constructor de valores [] con type [a] .

Answer 4

El tipo se describe (en una sesión GHCI) como:

$ ghci
Prelude> :info []
data [] a = [] | a : [a] -- Defined 

También podemos pensar en ello como si estuviera definido como:

data List a = Nil
            | Cons a (List a)

o

data List a = EmptyList
            | ListElement a (List a)

Tipo Constructor

[a] es un tipo de datos polimórficos, que también puede escribirse [] a como se indica anteriormente. Esto se puede pensar como si fuera List a

En este caso, [] es un constructor de tipos que toma un argumento de tipo a y devuelve el tipo [] a , que también se permite escribir como [a] .

Uno puede escribir el tipo de una función como:

sum :: (Num a) => [a] -> a

Constructor de datos

[] es un constructor de datos que esencialmente significa "lista vacía". Este constructor de datos no toma argumentos de valor.

Hay otro constructor de datos, : , que antepone un elemento al frente de otra lista. La firma para este constructor de datos es a : [a] - toma un elemento y otra lista de elementos y devuelve una lista resultante de elementos.

La notación [] también se puede usar como abreviatura para construir una lista. Normalmente, construiríamos una lista como:

myNums = 3 : 2 : 4 : 7 : 12 : 8 : []

que se interpreta como

myNums = 3 : (2 : (4 : (7 : (12 : (8 : [])))))

pero Haskell nos permite también usar la taquigrafía

myNums = [ 3, 2, 4, 7, 12, 8 ]

como un equivalente en significado, pero un poco más agradable en apariencia, notación.

Caso ambiguo

Hay un caso ambiguo que se ve comúnmente: [a] . Dependiendo del contexto, esta notación puede significar "una lista de a " o "una lista con exactamente un elemento, es decir, a ". El primer significado es el significado previsto cuando [a] aparece dentro de un tipo , mientras que el segundo significado es el significado previsto cuando [a] aparece dentro de un valor .