valeurs, types, genres, ... comme une séquence infinie ?

Question

Je commence seulement à me familiariser avec le concept des genres, alors soyez indulgent avec moi si je ne formule pas bien mes questions...

Les valeurs ont des types :

3 :: Int
[1,2,3] :: [Int]
('c',True) :: (Char,Bool)

Les types ont des genres :

the type 'Int' has kind *
the type '[Int]' also has kind *
   but the type constructor [] has kind * -> *
similarly, the type (Char,Bool) has kind  *
   but the type constructor (,) has kind * -> * -> *

Qu'est-ce que les Kinds ont ?

Les genres ont-ils un genre, des genres, des races ou des variétés ?

Jusqu'où va cette séquence d'abstraction ? S'arrête-t-on parce qu'on manque de mots, ou parce qu'aller plus loin n'a aucune valeur ? Ou, peut-être, parce que nous atteignons rapidement les limites de la cognition humaine et que nous ne parvenons pas à comprendre les types d'une génération supérieure ?

Une question connexe : les langages nous fournissent des constructeurs de valeurs (comme l'opérateur cons) pour créer des valeurs. Les langages nous donnent également des constructeurs de type comme (,) ou [] pour créer des types. Existe-t-il des langages qui exposent des constructeurs de type pour créer des types ?

Un autre cas limite qui m'intrigue : Nous avons apparemment un type qui n'a pas de valeur, noté comme , appelé "le type de fond". Existe-t-il une sorte qui n'a pas de type : une sorte inférieure ?

Answer 1

La terminologie type y kind n'a pas une bonne échelle. Depuis Bertrand Russell, les théoriciens des types utilisent une hiérarchie de "types". Une version de cette hiérarchie est la suivante Integer : Type 0, Type 0 : Type 1, Type 1 : Type 2, ..., Type n : Type (n+1), .... Dans les langages typés de manière dépendante comme Coq et Agda, on a souvent besoin de ces "tris supérieurs".

Des niveaux comme celui-ci sont utiles pour éviter Le paradoxe de Russell . Utilisation de Type : Type tend à provoquer une contradiction (voir Quine pour des conceptions alternatives).

Cette utilisation des chiffres est la notation standard lorsque nous en avons besoin. Certaines théories des types ont une notion de "types cumulatifs", de "niveaux cumulatifs" ou de "sortes cumulatives" qui dit "si t : Type n alors aussi t : Type (n+1) ".

Les niveaux cumulatifs + le "polymorphisme de niveau" donnent une théorie presque aussi flexible que Type : Type mais évite les paradoxes. Coq rend les niveaux implicites la plupart du temps, bien que les sortes Set y Prop sont toutes deux typées Type , Type {1} : Type {2} . En d'autres termes, vous ne voyez généralement pas les chiffres, et la plupart du temps, cela fonctionne tout simplement.

Agda possède un langage pragma qui fournit un polymorphisme de niveau, et rend les choses très flexibles, mais peut être légèrement bureaucratique (Agda est cependant généralement moins "bureaucratique" que Coq dans d'autres domaines).

Un autre bon mot est "univers".

Answer 2

Vous devriez probablement lire l'article de Tim Sheard sur Omega, un dialecte de Haskell avec une tour infinie de types/kinds/sorts, mais sans types dépendants à part entière. Il explique pourquoi vous voulez cela, et mentionne que les niveaux au-dessus de "sort" sont en pratique (du moins jusqu'à présent) très peu utilisés.