¿Cuál es la diferencia entre un tipo y un tipo?

Estoy aprendiendo el lenguaje de programación Haskell, y estoy tratando de entender cuál es la diferencia entre ay typea kind.

Como yo lo entiendo, a kind is a type of type. Por ejemplo, a ford is a type of cary a car is a kind of vehicle.

¿Es esta una buena manera de pensar en esto?

Porque, la forma en que mi cerebro está conectado actualmente, a ford is a **type** of car, pero también car is a **type** of vehicleal mismo tiempo a car is a **kind** of vehicle. Es decir, los términos typey kindson intercambiables.

¿Alguien podría arrojar algo de luz sobre esto?

Aquí, "valores", "tipos" y "tipos" tienen significados formales, por lo que considerar su uso común en inglés o analogías para clasificar automóviles solo lo llevará hasta cierto punto.

Mi respuesta se refiere a los significados formales de estos términos en el contexto de Haskell específicamente; Estos significados se basan en (aunque no son realmente idénticos a) los significados utilizados en la "teoría de tipos" matemática / CS. Entonces, esta no será una muy buena respuesta de "informática", pero debería servir como una muy buena respuesta de Haskell.

En Haskell (y otros lenguajes), resulta útil asignar un tipo a una expresión de programa que describe la clase de valores que se permite que tenga la expresión. Asumo aquí que has visto suficientes ejemplos para entender por qué sería útil saber que en la expresión sqrt (a**2 + b**2), las variables ay bsiempre serán valores de tipo Doubley no, digamos, Stringy Boolrespectivamente. Básicamente, tener tipos nos ayuda a escribir expresiones / programas que funcionarán correctamente en una amplia gama de valores .

Ahora, algo que quizás no se haya dado cuenta es que los tipos de Haskell, como los que aparecen en las firmas de tipos:

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

en realidad están escritos en un sublenguaje de Haskell de tipo tipo. El texto del programa Functor f => (a -> b) -> f a -> f bes, literalmente, una expresión de tipo escrita en este sublenguaje. El sublenguaje incluye operadores (p. Ej., ->Es un operador infijo asociativo correcto en este idioma), variables (p. Ej f. a, Y b) y "aplicación" de una expresión de tipo a otra (p. Ej., f aSe faplica a a).

¿Mencioné cómo fue útil en muchos idiomas asignar tipos a expresiones de programa para describir clases de valores de expresión? Bueno, en este sublenguaje de nivel de tipo, las expresiones evalúan los tipos (en lugar de los valores ) y termina siendo útil asignar tipos a expresiones de tipo para describir las clases de tipos que se les permite representar. Básicamente, tener clases nos ayuda a escribir expresiones de tipo que funcionarán correctamente en una amplia gama de tipos .

Entonces, los valores son para tipos como los tipos son para tipos , y los tipos nos ayudan a escribir programas de nivel de valor , mientras que los tipos nos ayudan a escribir programas de nivel de tipo .

¿Cómo son estos tipos ? Bueno, considere la firma de tipo:

id :: a -> a

Si la expresión de tipo a -> aes válida, ¿qué tipo de tipos deberíamos permitir aque sea la variable ? Bueno, las expresiones tipográficas:

Int -> Int
Bool -> Bool

parece válido, por lo que los tipos Int y Boolobviamente son del tipo correcto . Pero tipos aún más complicados como:

[Double] -> [Double]
Maybe [(Double,Int)] -> Maybe [(Double,Int)]

parece válido De hecho, ya que deberíamos poder invocar idfunciones, incluso:

(a -> a) -> (a -> a)

Se ve bien. Así, Int, Bool, [Double], Maybe [(Double,Int)], y a -> atoda la mirada como tipos de la derecha tipo .

En otras palabras, parece que solo hay un tipo , llamémoslo *como un comodín de Unix, y cada tipo tiene el mismo tipo * , final de la historia.

¿Correcto?

Bueno, no del todo. Resulta que Maybe, en sí mismo, es una expresión de tipo tan válida como Maybe Int(de la misma manera sqrt, en sí misma, es una expresión de valor tan válida como sqrt 25). Sin embargo , la siguiente expresión de tipo no es válida:

Maybe -> Maybe

Porque, si bien Maybees una expresión de tipo, no representa el tipo de tipo que puede tener valores. Entonces, así es como debemos definir *: es el tipo de tipos que tienen valores; incluye tipos "completos" como Doubleo Maybe [(Double,Int)]pero excluye tipos incompletos y sin valor como Either String. Para simplificar, llamaré a estos tipos completos de tipo *"tipos concretos", aunque esta terminología no es universal, y "tipos concretos" podrían significar algo muy diferente a, por ejemplo, un programador de C ++.

Ahora, en la expresión de tipo a -> a, siempre y cuando el tipo atiene clase * (la clase de tipos concretos), el resultado de la expresión de tipo a -> aserá también tienen clase * (es decir, la clase de tipos concretos).

Entonces, ¿qué tipo de tipo es Maybe? Bueno, Maybese puede aplicar a un tipo de concreto para producir otro tipo de concreto. Entonces, se Maybeparece un poco a una función de nivel de tipo que toma un tipo de tipo * y devuelve un tipo de tipo * . Si tuviéramos una función de nivel de valor que tomara un valor de tipo Int y devolviera un valor de tipo Int , le daríamos una firma de tipoInt -> Int , así que por analogía deberíamos dar Maybeuna firma amable* -> * . GHCi está de acuerdo:

> :kind Maybe
Maybe :: * -> *

Volviendo a:

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

En este tipo de firma, variable ftiene kind * -> *y variables ay bhave kind *; el operador incorporado ->tiene kind * -> * -> *(toma un tipo de tipo *a la izquierda y uno a la derecha y devuelve un tipo también de tipo *). A partir de esto y de las reglas de inferencia amable, puede deducir que a -> bes un tipo válido con tipo *, f ay f btambién son tipos válidos con tipo *, y (a -> b) -> f a -> f bes un tipo de tipo válido *.

En otras palabras, el compilador puede "verificar el tipo" de la expresión de tipo (a -> b) -> f a -> f bpara verificar que sea válida para las variables de tipo del tipo correcto de la misma manera que "comprueba de tipo" sqrt (a**2 + b**2)para verificar que sea válida para las variables del tipo correcto.

La razón para usar términos separados para "tipos" versus "tipos" (es decir, no hablar de los "tipos de tipos") es principalmente para evitar confusiones. Los tipos anteriores se ven muy diferentes de los tipos y, al menos al principio, parecen comportarse de manera bastante diferente. (Por ejemplo, lleva algún tiempo comprender la idea de que cada tipo "normal" tiene el mismo tipo *y el tipo no lo a -> bes ).** -> *

Algo de esto también es histórico. A medida que GHC Haskell ha evolucionado, las distinciones entre valores, tipos y clases han comenzado a desdibujarse. En estos días, los valores se pueden "promocionar" en tipos, y los tipos y clases son realmente lo mismo. Por lo tanto, en Haskell moderno, los valores tienen tipos y tipos ARE (casi), y los tipos de tipos son simplemente más tipos.

@ user21820 pidió una explicación adicional de "los tipos y tipos son realmente lo mismo". Para ser un poco más claro, en el GHC Haskell moderno (desde la versión 8.0.1, creo), los tipos y clases se tratan de manera uniforme en la mayoría del código del compilador. El compilador hace un esfuerzo en los mensajes de error para distinguir entre "tipos" y "tipos", dependiendo de si se queja del tipo de un valor o del tipo de un tipo, respectivamente.

Además, si no hay extensiones habilitadas, se pueden distinguir fácilmente en el lenguaje de superficie. Por ejemplo, los tipos (de valores) tienen una representación en la sintaxis (por ejemplo, en las firmas de tipos), pero los tipos (de tipos) son, creo, completamente implícitos, y no hay una sintaxis explícita donde aparecen.

Pero, si activa las extensiones apropiadas, la distinción entre tipos y clases desaparece en gran medida. Por ejemplo:

{-# LANGUAGE GADTs, TypeInType #-}
data Foo where
  Bar :: Bool -> * -> Foo

Aquí, Bares (tanto un valor como) un tipo. Como tipo, su tipo es Bool -> * -> Foo, que es una función de nivel de tipo que toma un tipo de tipo Bool(que es un tipo, pero también un tipo) y un tipo de tipo *y produce un tipo de tipo Foo. Asi que:

type MyBar = Bar True Int

correctamente verificaciones de tipo.

Como @AndrejBauer explica en su respuesta, esta incapacidad para distinguir entre tipos y clases no es segura: tener un tipo / tipo *cuyo tipo / tipo es en sí mismo (que es el caso en Haskell moderno) conduce a paradojas. Sin embargo, el sistema de tipos de Haskell ya está lleno de paradojas debido a la no terminación, por lo que no se considera un gran problema.

• Bool es un tipo
• Type es un tipo porque sus elementos son tipos
• Bool -> Int es un tipo
• Bool -> Type es un tipo porque sus elementos son funciones que devuelven tipos
• Bool * Int es un tipo
• Bool * Type es un tipo porque sus elementos son pares con un componente un tipo

$U_0$$U_1$$U_2$$U_0$$\mathtt{Bool}$$\mathtt{Nat}$$\mathtt{Nat} \to \mathtt{Nat}$$U_1$$U_0$$\mathtt{Bool} \to U_0$$U_0 \to U_0$$U_{n+1}$$U_n$$U_n$$\times$$\to$

$U_0$$U_1$$U_0$$U_1$$U_0$**U_1

Un valor es como el Ford Mustang 2011 rojo específico con 19,206 millas que tiene sentado en su camino de entrada.

Ese valor específico, informalmente, podría tener muchos tipos : es un Mustang, y es un Ford, y es un automóvil, y es un vehículo, entre muchos otros muchos tipos que podría inventar (el tipo de "cosas" que te pertenece ", o el tipo de" cosas que son rojas ", o ...).

(En Haskell, para una aproximación de primer orden (los GADT rompen esta propiedad, y la magia alrededor de los literales numéricos y la extensión OverloadedStrings lo oscurecen un poco), los valores tienen un tipo principal en lugar de la gran cantidad de "tipos" informales que puede dar a su ' stang. 42es, para los propósitos de esta explicación, un Int; no hay ningún tipo en Haskell para "números" o "números enteros", o más bien, podría hacer uno, pero sería un tipo disjunto de Int).

Ahora, "Mustang" puede ser un subtipo de "automóvil", cada valor que es un Mustang también es un automóvil. Pero el tipo , o, para usar la terminología de Haskell, el tipo de "Mustang" no es "auto". "Mustang", el tipo no es algo que pueda estacionar en su camino de entrada o conducir. "Mustang" es un sustantivo, o una categoría, o simplemente un tipo. Esos son, informalmente, los tipos de "Mustang".

(Una vez más, Haskell solo reconoce un tipo por cada cosa de nivel de tipo. Por lo tanto, Inttiene tipo *, y ningún otro tipo. MaybeTiene tipo * -> *, y ningún otro tipo. Pero la intuición aún debe sostenerse: 42es un Int, y puedes hacer Intmuchas cosas con él como sumar y restar. en Intsí mismo no es un Int; no existe un número como Int + Int. Es posible que escuche informalmente que la gente dice que Intes un Num, por lo que quieren decir que hay una instancia de la Numclase de tipo para el tipo Int; esto no es lo mismo como decir que Inttiene kind Num . Inttiene kind "type", que en Haskell se deletrea *.)

Entonces, ¿no es cada "tipo" informal solo un sustantivo o una categoría? ¿Todos los tipos tienen el mismo tipo? ¿Por qué hablar de los tipos si son tan aburridos?

Aquí es donde la analogía en inglés se volverá un poco difícil, pero tengan paciencia conmigo: pretendan que la palabra "propietario" en inglés no tiene sentido de forma aislada, sin una descripción de lo que se posee. Imagina que si alguien te llamara "dueño", eso no tendría ningún sentido para ti; pero si alguien te llama "dueño de un auto", puedes entender lo que significan.

"Propietario" no tiene el mismo tipo que "automóvil", porque puede hablar sobre un automóvil, pero no puede hablar sobre un propietario en esta versión inventada del inglés. Solo se puede hablar del "propietario de un automóvil". "Propietario" solo crea algo parecido al "sustantivo" cuando se aplica a algo que ya tiene el tipo "sustantivo", como "auto". Diríamos que el tipo de "propietario" es "sustantivo -> sustantivo". "Propietario" es como una función que toma un sustantivo y produce a partir de eso un sustantivo diferente; pero no es un sustantivo en sí mismo.

Tenga en cuenta que "propietario del automóvil" no es un subtipo de "automóvil". ¡No es una función que acepta o devuelve automóviles! Es solo un tipo completamente separado de "automóvil". Describe valores con dos brazos y dos piernas que en un momento tenían una cierta cantidad de dinero, y llevaron ese dinero a un concesionario. No describe valores que tienen cuatro ruedas y un trabajo de pintura. También tenga en cuenta que el "dueño del automóvil" y el "dueño del perro" son diferentes tipos, y que las cosas que desee hacer con uno pueden no ser aplicables al otro.

(Del mismo modo, cuando decimos que eso Maybees amable * -> *en Haskell, queremos decir que no tiene sentido (formalmente; informalmente, lo hacemos todo el tiempo) hablar de tener "a Maybe". En cambio, podemos tener un Maybe Into un Maybe String, ya que esas son cosas de amable *)

Entonces, el punto de hablar sobre los tipos es para que podamos formalizar nuestro razonamiento en torno a palabras como "propietario" y hacer cumplir que solo tomamos valores de tipos que han sido "completamente construidos" y que no tienen sentido.

Según tengo entendido, un tipo es un tipo de tipo.

Así es, exploremos lo que eso significa. Into Textson tipos concretos, pero Maybe aes un tipo abstracto . No se convertirá en un tipo concreto hasta que decida qué valor específico desea apara una variable particular (o valor / expresión / lo que sea), por ejemplo Maybe Text.

Decimos que Maybe aes un constructor de tipos porque es como una función que toma un solo tipo concreto (por ejemplo Text) y devuelve un tipo concreto ( Maybe Texten este caso). Pero otros constructores de tipos pueden tomar incluso más "parámetros de entrada" antes de devolver un tipo concreto. Por ejemplo, Map k vnecesita tomar dos tipos concretos (por ejemplo, Inty Text) antes de poder construir un tipo concreto ( Map Int Text).

Entonces, los constructores de tipo Maybe ay List atienen la misma "firma" que denotamos como * -> *(de manera similar a la firma de la función Haskell) porque si les das un tipo concreto, escupirán un tipo concreto. Llamamos a esto el "tipo" del tipo Maybey Listtenemos el mismo tipo.

Se dice que los tipos concretos tienen tipo *, y nuestro ejemplo de Mapa es amable * -> * -> *porque toma dos tipos concretos como entrada antes de que pueda generar un tipo concreto.

Puede ver que se trata principalmente de la cantidad de "parámetros" que pasamos al constructor de tipos, pero tenga en cuenta que también podríamos tener constructores de tipos anidados dentro de los constructores de tipos, por lo que podemos terminar con un tipo que se parece, * -> (* -> *) -> *por ejemplo .

Si es un desarrollador de Scala / Java, también puede encontrar útil esta explicación: https://www.atlassian.com/blog/archives/scala-types-of-a-higher-kind