Salut Simon,
Tu parlais l'autre jour du "levity polymorphism" (https://dl.acm.org/doi/abs/10.1145/3140587.3062357) où ils remplacent le "sort" `Type` par plusieurs "sort"es différents selon les contraintes qu'il veulement imposer au type. Supposément avant ils utilisent du sous-typage à la place.
Ça me rappelle quelques autres usages où `Type` est subdivisé en différents cas. Bien sûr, d'abord dans Typer où `Type` est indexé par le niveau d'univers.
Plus proche du cas de "levity", il y a aussi l'usage d'index de taille, ou `Type N` correspond à la sorte des valeurs qui tiennent dans N bits.
Dans Cayenne, `Type` était indexé par un "level" similaire à celui de Typer mais utilisé pour le "erasure" (le niveau 0 est gardé, tous les autres sont erased, IIRC).
Dans Arendt, `Type` est indexé par 2 "levels" le premier est le même que celui de Typer, et le deuxième est le "h-level", qui nous vient du "homotopy type theory". En gros:
h-level 0 => les types des "mere propositions", où chaque type ne peut avoir qu'une seule valeur: ∀x, y : τ : Type (h-level 0) => Eq x y h-level 1 => les types des "sets", où chaque preuve d'égalité sur ces valeur est unique ∀x, y : τ : Type (h-level 1) P1, P2 : Eq x y => Eq P1 P2 h-level 2 => il peut y avoir plusieurs preuves d'égalités différentes pour deux valeurs données, mais il ne peut y avoir qu'une seule preuve d'égalité entre ces preuves d'égalités: ∀x, y : τ : Type (h-level 1) P1, P2 : Eq x y Pa1, Pa2 : Eq P1 P2 => Eq Pa1 Pa2 ...
Il y a d'autres manière de classifier les types, bien sûr. Les cas ci-dessus correspondent à des types "intrinsically typed", mais on pourrait remplacer en tout cas plusieurs d'entre eux par des preuves séparées, genre:
t : Type N ==devient==> (t : Type, P: hasSize t N)
En fait, c'est ce qu'on fait aussi avec les type classes.
Stefan
Afficher les réponses par date