Constructores de tipos vs constructores de datos (Haskell)

publicado por: Anonymous

Si se crea un vector de con dos componentes genéricos, como:

data Vector a = MakeVector a a

(puse MakeVector en vez de Vector a propósito)

(Vector a) es el constructor de tipos mientras que
(MakeVector) es el constructor de datos.

si hago

:t MakeVector 1 2
MakeVector 1 2 :: Num a => Vector a

puedo ver que tiene sentido decir que MakeVector es un constructor puesto que obtengo una instancia de tipo (Vector a) con a de tipo Num

pero ¿por qué se llama a (Vector a) contructor de tipos?, no puedo hacer nada con (Vector a), no puedo construir nada, es el identificador del tipo en si mismo en dependencia del tipo que tenga a.

todavía más, personalmente encontraría acertado llamar a MakeVector constructor de tipo (dado que obtengo un tipo) en vez de constructor de datos, ¿por qué no lo llaman así?

Gracias.

solución

Tenemos

data Vector a = MkVector a a

entonces, se dice que Vector construye tipos, porque su firma (en la categoría Hask) es

> :k Vector
Vector :: * -> *

es decir, toma un tipo y devuelve un tipo (el “agujero” * es un tipo). Un constructor de tipos únicamente puede tomar tipos (*) y devolver tipos (*), mientras que un constructor de valores puede tomar cualquier cosa (Int, String, …) y devolver cualquier cosa (Int, String, …). La diferencia entre * y String, Int, Bool, … es la misma diferencia que hay entre String y "cabra", "melón", …

Por ejemplo, podemos ver cómo

> :k Vector Int
Vector Int :: *

es ahora un tipo “final”, hemos construido un tipo.

Por contra, MkVector es una función normal y corriente, veamos

> :t MkVector
MkVector :: a -> a -> Vector a

que toma dos valores y devuelve otro valor.

Como ves, la currificación puede aplicarse indistintamente a tipos como a funciones, es decir, podemos tener el constructor de tipos

data Vector' índice valor = MkVector' [(índice, valor)]

con firma

> :k Vector'
Vector' :: * -> * -> *

y podemos currificarla en el primer argumento para obtener otro constructor de tipos, veamos

> :k Vector' String
Vector' String :: * -> *

que sigue siendo un constructor de tipos (una función en Hask).

Así, Vector construye tipos y MkVector valores, porque el primero es una función sobre los tipos (la categoría Hask) y la segunda una función sobre valores.

En Haskell, los tipos se expanden en tiempo de compilación, perdiéndose cualquier información sobre ellos en el resultado. No obstante, el proceso de compilación puede ser usado para “ejecutar código”, por ejemplo Máquina de Turing en el sistema de tipos.

Respondido por: Anonymous

Leave a Reply

Your email address will not be published. Required fields are marked *