Théorie des types: types de types

Question

J'ai lu beaucoup de choses intéressantes sur les types de types, les types plus élevés et ainsi de suite. Par défaut, Haskell prend en charge deux sortes de genre:

• Type simple: *
• constructeur Type: * → *

Dernières extensions de langage de GHC ConstraintKinds ajoute un nouveau genre:

• paramètre Type contrainte: Constraint

également après avoir lu this mailing list il devient clair qu'un autre type de genre peut existe, mais il est pas pris en charge par GHC (mais un tel soutien est mis en œuvre dans le .NET):

• Type Unboxed: #

J'ai entendu parler de polymorphic kinds et je pense avoir compris l'idée. Haskell soutient également la quantification explicitement liée.

Mes questions sont les suivantes:

• t-il des autres types de types existe?
• Existe-t-il d'autres fonctionnalités de langage aimables?
• Que signifie subkinding? Où est-il mis en œuvre/utile?
• Existe-t-il un système de type au-dessus de kinds, comme kinds sont un système de type au-dessus de types? (juste intéressé)

Answer 1

Oui, il existe d'autres types. La page Intermediate Types décrit d'autres types utilisés dans GHC (y compris les types non-boxed et certains types plus compliqués ainsi). Le langage Ωmega prend les types les plus élevés dans l'extension logique maximale, ce qui permet des types définis par l'utilisateur (et des tris, et plus). This page propose une extension de type kind pour GHC qui permettrait des types définissables par l'utilisateur dans Haskell, ainsi qu'un bon exemple de pourquoi ils seraient utiles.

Comme un court extrait, supposons que vous vouliez un type de liste qui avait une annotation au niveau du type de la longueur de la liste, comme ceci:

data Zero 
data Succ n 

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

L'intention est que le dernier argument de type ne devrait être Zero ou Succ n, où n est de nouveau seulement Zero ou Succ n. En bref, vous devez introduire un nouveau type, appelé Nat qui contient uniquement les deux types Zero et Succ n. Ensuite, le List datatype pourrait exprimer que le dernier argument n'est pas un *, mais un Nat, comme

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

Cela permettrait au contrôleur de type à être beaucoup plus discriminante dans ce qu'il accepte, ainsi que de faire au niveau du type programmation beaucoup plus expressive.

Answer 2

Tout comme les types sont classés avec les types, les types sont classés avec les sortes.

Ωmega programming language a un système de type avec des types définissables par l'utilisateur à tout niveau. (Donc, dit son wiki, je pense qu'il se réfère aux sortes et niveaux ci-dessus, mais je ne suis pas sûr.)

Answer 3

Il y a eu une proposition pour soulever des types dans le niveau de type et des valeurs dans le niveau de type. Mais je ne sais pas si cela est déjà mis en œuvre (ou si jamais il atteindra « prime time »)

Considérez le code suivant:

data Z 
data S a 

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

Ceci est un vecteur qui a sa dimension codée dans le type. Nous utilisons Z et S pour générer le nombre naturel.C'est sympa mais on ne peut pas "taper check" si on utilise les bons types en générant un Vec (on pourrait accidentellement changer de type de contenu) et on doit aussi générer un type S et Z, ce qui n'est pas pratique si on a déjà défini les nombres naturels comme ceci:

data Nat = Z | S Nat 

Avec la proposition que vous pourriez écrire quelque chose comme ceci:

data Nat = Z | S Nat 

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

cela lèverait Nat dans le niveau de nature et S et Z dans le niveau du type si nécessaire. Donc Nat est un autre genre et vit au même niveau que *.

Voici la présentation par Brent Yorgey

Typed type-level functional programming in GHC