Teoría de tipos: tipos de tipos

Question

He leído muchas cosas interesantes sobre tipos de tipos, tipos de mayor calidad, etc. Por defecto Haskell admite dos tipos de clase:

• tipo simple: *
• Tipo constructor: * → *

últimas extensiones de lenguaje de GHC ConstraintKinds añade un nuevo tipo:

• parámetro Type restricción: Constraint

también después de leer this mailing list se hace evidente que puede existe otro tipo de especie, pero no es compatible con GHC (pero ese apoyo se implementa en .NET):

• Tipo de Embalaje: #

He aprendido acerca de polymorphic kinds y creo que entiendo la idea. También Haskell admite la cuantificación explícitamente emparentada.

Así que mis preguntas son:

• hacer cualquier otro tipo de clases existe?
• ¿Hay alguna otra característica relacionada con el tipo de lenguaje?
• ¿Qué significa subkinding? ¿Dónde está implementado/útil?
• ¿Hay un sistema de tipo en la parte superior de kinds, como kinds son un sistema de tipo en la parte superior de types? (solo interesado)

Answer 1

Sí, existen otros tipos. La página Intermediate Types describe otros tipos utilizados en GHC (incluidos los tipos no compartidos y también algunos tipos más complicados). El lenguaje Ωmega lleva los tipos de mayor nivel a la extensión lógica máxima, lo que permite tipos definibles por el usuario (y géneros, y más). This page propone una amable extensión de sistema para GHC que permitiría tipos definibles por el usuario en Haskell, así como un buen ejemplo de por qué serían útiles.

Como un breve extracto, suponga que desea un tipo de lista que tenía una anotación de nivel de tipo de la longitud de la lista, así:

data Zero 
data Succ n 

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

La intención es que el último argumento de tipo debe ser sólo Zero o Succ n, donde n es de nuevo solo Zero o Succ n. En resumen, debe introducir un nuevo tipo, llamado Nat que contiene solo los dos tipos Zero y Succ n. A continuación, el List tipo de datos podría expresar que el último argumento no es un *, sino una Nat, como

data List :: * -> Nat -> * where 
    Nil :: List a Zero 
    Cons :: a -> List a n -> List a (Succ n) 

Esto permitiría que el tipo de corrector sea mucho más discriminativo en lo que acepta, así como hacer el tipo de nivel programación mucho más expresiva.

Answer 2

Así como los tipos están clasificados por tipos, los tipos se clasifican por géneros.

Ωmega programming language tiene un sistema amable con tipos definibles por el usuario en cualquier nivel. (Así dice su wiki. Creo que se refiere a los géneros y los niveles anteriores, pero no estoy seguro).

Answer 3

Se ha propuesto elevar los tipos al nivel de tipo y los valores al nivel de tipo. Pero no sé si es que ya se implementa (o si alguna vez llegará a "prime time")

Considere el siguiente código:

data Z 
data S a 

data Vec (a :: *) (b :: *) where 
    VNil :: Vec Z a 
    VCons :: a -> Vec l a -> Vec (S l) a 

Este es un vector que tiene se codifica dimensión en el tipo. Estamos usando Z y S para generar el número natural.Eso es agradable, pero no podemos "verificar el tipo" si estamos utilizando los tipos correctos cuando generamos un Vec (podríamos accidentalmente cambiar la longitud por un tipo de contenido) y también necesitamos generar un tipo S y Z, lo cual es inconveniente si ya lo hacemos definidos los números naturales, así:

data Nat = Z | S Nat 

Con la propuesta se podría escribir algo como esto:

data Nat = Z | S Nat 

data Vec (a :: Nat) (b :: *) where            
    VNil :: Vec Z a 
    VCons :: a -> Vec l a -> Vec (S l) a 

esto levantaría Nat en el nivel de especie y S y Z en el nivel de tipo, si es necesario. Entonces Nat es otro tipo y vive en el mismo nivel que *.

Aquí es la presentación por Brent Yorgey

Typed type-level functional programming in GHC