scala - ramificada - teoria de los tipos quimica

Teoría de tipos: tipos de tipos

Question

He leído muchas cosas interesantes sobre tipos de tipos, tipos de tipos más altos y así sucesivamente. Por defecto, Haskell admite dos tipos de clases:

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

ConstraintKinds últimas extensiones de lenguaje de GHC, agrega un nuevo tipo:

• Tipo de restricción de parámetro: Constraint

Además, después de leer esta lista de correo , queda claro que puede existir otro tipo de tipo, pero no es compatible con GHC (pero dicho soporte se implementa en .NET):

• Tipo sin caja: #

He aprendido sobre tipos polimórficos y creo que entiendo la idea. También Haskell soporta cuantificación explícitamente clasificada.

Así que mis preguntas son:

• ¿Existen otros tipos de tipos?
• ¿Hay alguna otra característica de lenguaje de tipo repetido?
• ¿Qué significa subkinding ? ¿Dónde está implementado / útil?
• ¿Hay un sistema de kinds sobre kinds , como los kinds son un sistema de types sobre types ? (solo interesado)

Answer 1

Así como los tipos se clasifican con clases, las clases se clasifican con clases.

El languagemega lenguaje de programación tiene un sistema amable con tipos definibles por el usuario en cualquier nivel. (Eso dice su wiki. Creo que se refiere a los géneros y los niveles anteriores, pero no estoy seguro).

Answer 2

Ha habido una propuesta para elevar los tipos al nivel de clase y los valores al nivel de tipo. Pero no sé si eso ya está implementado (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 su dimensión codificada en el tipo. Estamos utilizando Z y S para generar el número natural. Eso es bueno, pero no podemos "teclear" si estamos usando los tipos correctos cuando generamos un Vec (podríamos cambiar accidentalmente el tipo de contenido) y también necesitamos generar un tipo S y Z, lo cual es un inconveniente si ya Definí los números naturales así:

data Nat = Z | S Nat

Con la propuesta podrías 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 elevaría a Nat al nivel de clase y S y Z al nivel de tipo si fuera necesario. Así que Nat es otro tipo y vive en el mismo nivel que *.

Aquí está la presentación de Brent Yorgey.

Programación funcional a nivel de tipografía en GHC.

Answer 3

Sí, existen otros tipos. La página Tipos Intermedios describe otros tipos utilizados en GHC (incluyendo tanto los tipos sin caja como algunos tipos más complicados). El lenguaje Ωmega lleva los tipos de tipo superior a la extensión lógica máxima, lo que permite tipos definibles por el usuario (y tipo, y superior). Esta página propone una extensión de sistema tipo 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, supongamos que desea un tipo de lista que tenga una anotación de nivel de tipo de la longitud de la lista, como esta:

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 solo debe ser Zero o Succ n , donde n es nuevamente solo Zero o Succ n . En resumen, necesita introducir un nuevo tipo, llamado Nat que contiene solo los dos tipos Zero y Succ n . Entonces el tipo de datos de la List podría expresar que el último argumento no es un * , sino un Nat , como

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

Esto permitiría que el verificador de tipos sea mucho más discriminatorio en lo que acepta, así como que la programación a nivel de tipo sea mucho más expresiva.