- Les niveaux d'univers d'un quotient, je ne les connais pas bien, mais mon intuition me dit que `Quotient τ R` devrait pouvoir être dans le même niveau d'univers que celui de `τ`, quelque soit `R`, vu que c'est un "sous ensemble" de `τ`. Pas sûr si c'est vrai dans HoTT, par contre. J'imagine qu'en pratique ça fait probablement pas de grosse différence, donc ton choix est plus sûr. Je sais pas si concrètement ça poserait des problèmes si le niveau d’univers de `Quotient` ignore celui de `τ`. Pour nous rassurer un peu, Cubical Agda utilise aussi le max des 2 niveaux :)

Au fait, j’ai appris que dans l’absence de la ’set truncation’, si on construit le type quotient de `Unit` avec une relation totale quelconque, il se trouve que ça nous donnerait quelque chose qui est equivalent à S¹, c’est à dire le type avec les constructeurs suivants:

data S¹ : Type where base : S¹ loop : base ≡ base

Donc, c’est vrai que intuitivement parlant, le quotient d’un type devrait être un “sous ensemble” du type de base, mais en fait ce n’est pas forcément le cas, et je trouve que c’est très intéressant.

On devrait pouvoir simplifier ça pas mal, genre:

Quotient_elim : (f : ?A -> ?B) -> (p : (a : ?) -> (a' : ?) -> ?R a a' -> Eq (f a) (f a')) ≡> (q : Quotient (A := ?A) ?R) -> ?B; Quotient_elim = Built-in "Quotient.elim";

Même chose:

Quotient_eq : (a : ?) ≡> (a' : ?) ≡> (p : ?R a a') ≡> Eq (Quotient_in (R := R?) a) (Quotient_in (R := R?) a'); Quotient_eq = Built-in "Quotient.eq”;

Ah alors là, en fait j’ai déjà essayé de faire ça, mais il y a eu un petit problème lors de l’élaboration, j’ai rencontré l’erreur qui dit "Bug in the elaboration of a repeated metavar!”. Pour l’instant, je vais juste ajouter un commentaire dans le code.

Quotient_eq : (a : ?) ≡> (a' : ?) ≡> (p : ?R a a') ≡> Eq (Quotient_in (R := R?) a) (Quotient_in (R := R?) a'); Quotient_eq = Built-in "Quotient.eq";

Et tu pourrais marquer `p` comme argument normal. C’est vrai que c’est plus cohérent avec la règle d’elimination.

En effet. C'est probablement parce que l'argument `p` vient avant le quotient, ce qui fait qu'on unifie d'abord avec `?R a a'`, qui est une unification difficile, et pour l'instant on ne gère pas les résidus d’unification Mmm je vois, je vais mettre à jour le commentaire pour l’instant.

Tho, more useful would be a Rational library (based on `Int` or `Integer` rather than `Nat`). Will/would require adding various axioms about the properties of our builtin operations on `Int`s (and `Integer`s). Bonne idée, j’ajoute ça à ma to-do list.

Sinon, j’ai effectué tous les autres petits changements que vous avez conseillés :)

James

Le 18 juill. 2023 à 18:20, Stefan Monnier monnier@iro.umontreal.ca a écrit :

Super! Au fait, je viens de pousser ce que j’ai fait jusqu’à présent sur les types quotients sur une nouvelle branche `quotient-types`.

--- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -183,6 +183,32 @@ let eq_eq = Anormal, mkCall (dsinfo, mkVar (fv, 0), [Aerasable, interval_i1])])))))

+ +let type_quotient_type = + let lv1 = (dsinfo, Some "l1") in + let lv2 = (dsinfo, Some "l2") in + let tv = (dsinfo, Some "A") in + let rv = (dsinfo, Some "R") in + let rtype = mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 0), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 1), + mkSort (dsinfo, Stype (mkVar (lv2, 3))))) in + mkArrow (dsinfo, Aerasable, lv1, + type_level, + mkArrow (dsinfo, Aerasable, lv2, + type_level, + mkArrow (dsinfo, Aerasable, tv, + mkSort (dsinfo, Stype (mkVar (lv1, 1))), + mkArrow (dsinfo, Anormal, rv, + rtype, + mkSort (dsinfo, Stype + (mkSortLevel + (mkSLlub' (mkVar (lv1, 3), + mkVar (lv2, 2))))))))) + +let type_quotient = mkBuiltin ((dloc, "Quotient"), type_quotient_type)

J'espère qu'on peut déplacer ça dans `builtins.typer`, quoique je vois que c'est la déclaration de `Quotient` (et non `Quotient.in` comme je pensais dans le courriel précédent), donc c'est comme `type_eq_type` qu'on a encore dans `builtin.ml` :-(

+%% Quotient : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡> +%% (R : A -> A -> Type_ l2) -> Type_ (TypeLevel_⊔ l1 l2) +%%

- Les niveaux d'univers d'un quotient, je ne les connais pas bien, mais mon intuition me dit que `Quotient τ R` devrait pouvoir être dans le même niveau d'univers que celui de `τ`, quelque soit `R`, vu que c'est un "sous ensemble" de `τ`. Pas sûr si c'est vrai dans HoTT, par contre. J'imagine qu'en pratique ça fait probablement pas de grosse différence, donc ton choix est plus sûr.

- Je laisserais `A` comme argument normal plutôt qu'argument effaçable (même si c'est vrai qu'il est trivial de l'inférer sur la base de `R`).

+Quotient_in : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡> + A -> (R : A -> A -> Type_ l2) ≡> Quotient (A := A) R;

L'argument `A` devrait arriver dernier, après `R`. Et tu devrais pouvoir simplifier ça à:

Quotient_in : ?A -> Quotient (A := ?A) ?R;

--- a/samples/quotient.typer +++ b/samples/quotient.typer @@ -26,8 +26,21 @@ normaliseZ np = case np equalZ : NatPair -> NatPair -> Type; equalZ x1 x2 = Pair (Eq (fst x1) (snd x2)) (Eq (snd x1) (fst x2));

+%% See definition in `builtins.typer` +%% Quotient : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡> +%% (R : A -> A -> Type_ l2) -> Type_ (TypeLevel_⊔ l1 l2) +%% +%% Quotient_in : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡> +%% A -> (R : A -> A -> Type_ l2) => Quotient A R + %% FIXME: We shouldn't get this error %% "Requested Built-in "Quotient" does not exist" %% Z = Quotient (A := NatPair) equalZ;

-%% TODO: Intro and elim \ No newline at end of file +Z_To_Int : Quotient (A := NatPair) equalZ -> Int; +Z_To_Int q = 5 : Int; + +test : Int; +test = Z_To_Int (Quotient_in (A := NatPair) (pair zero zero) (R := equalZ)); + +%% TODO: Elim \ No newline at end of file

SVP: assures-toi que tes fichiers textes se terminent par un retour à la ligne.

+let quotient_in = + let lv1 = (dsinfo, Some "l1") in + let lv2 = (dsinfo, Some "l2") in + let tv = (dsinfo, Some "A") in + let rv = (dsinfo, Some "R") in + let rtype = mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 1), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 2), + mkSort (dsinfo, Stype (mkVar (lv2, 4))))) in + let qtype = mkCall (dsinfo, type_quotient, + [Aerasable, mkVar (lv1, 4); + Aerasable, mkVar (lv2, 3); + Aerasable, mkVar (tv, 2); + Anormal, mkVar (rv, 0)]) in + mkArrow (dsinfo, Aerasable, lv1, + type_level, + mkArrow (dsinfo, Aerasable, lv2, + type_level, + mkArrow (dsinfo, Aerasable, tv, + mkSort (dsinfo, Stype (mkVar (lv1, 1))), + mkArrow (dsinfo, Anormal, (dsinfo, None), + mkVar (tv, 0), + mkArrow (dsinfo, Aerasable, rv, + rtype, + qtype)))))

Celui-ci on devrait pouvoir l'éliminer en suivant l'exemple de `eq_eq`.

+ | [_; _; (_, t); (_, r)] when OL.conv_p ctx e' DB.type_quotient + -> sprintf "(inQ %s %s)" (Lexp.to_string t) (Lexp.to_string r)

Idéalement il faudrait utiliser une syntaxe "identique" à celle du code source, donc je recommande `Quotient.in` ici. Sur le plus long terme,

il faudrait essayer d'implémenter `value_string_with_type` en convertissant la `value` (plus son type) en une `lexp` (probablement en passant via `elexp`) puis une `sexp` puis une string.

+Quotient_elim : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (l3 : TypeLevel) ≡> + (A : Type_ l1) ≡> (B : Type_ l2) ≡> + (R : A -> A -> Type_ l3) ≡> + (f : A -> B) -> + (p : (a : A) -> (a' : A) -> R a a' -> Eq (f a) (f a')) ≡> + (q : Quotient (A := A) R) -> + B; +Quotient_elim = Built-in "Quotient.elim";

On devrait pouvoir simplifier ça pas mal, genre:

Quotient_elim : (f : ?A -> ?B) -> (p : (a : ?) -> (a' : ?) -> ?R a a' -> Eq (f a) (f a')) ≡> (q : Quotient (A := ?A) ?R) -> ?B; Quotient_elim = Built-in "Quotient.elim";

+%% FIXME: Explicitly providing a value for R should unnecessary? +%% This should be inferred based on the type of `q`?

En effet. C'est probablement parce que l'argument `p` vient avant le quotient, ce qui fait qu'on unifie d'abord avec `?R a a'`, qui est une unification difficile, et pour l'instant on ne gère pas les résidus d'unification (i.e. les problèmes non-résolus, qui souvent pourraient être résolus plus tard) donc l'unification renvoie une "erreur" alors qu'elle devrait facilement réussir.

Quotient_in : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡> - A -> (R : A -> A -> Type_ l2) ≡> Quotient (A := A) R; + (R : A -> A -> Type_ l2) ≡> A -> Quotient (A := A) R;

Aha! :-)

Tu devrais "squash" ce changement dans le commit qui introduit `Quotient_in`.

+Quotient_eq : (l1 : TypeLevel) ≡> (l2 : TypeLevel) ≡> (A : Type_ l1) ≡> + (R : A -> A -> Type_ l2) ≡> + (a : A) ≡> (a' : A) ≡> (p : R a a') ≡> + Eq (Quotient_in (A := A) (R := R) a) + (Quotient_in (A := A) (R := R) a'); +Quotient_eq = Built-in "Quotient.eq";

Même chose:

Quotient_eq : (a : ?) ≡> (a' : ?) ≡> (p : ?R a a') ≡> Eq (Quotient_in (R := R?) a) (Quotient_in (R := R?) a'); Quotient_eq = Built-in "Quotient.eq";

Et tu pourrais marquer `p` comme argument normal.

+𝟙=𝟙 : Eq (t := Quotient (A := NatPair) equalZ) 𝟙-𝟘 𝟚-𝟙; +𝟙=𝟙 = Quotient_eq + (R := equalZ) + (a := pair (succ zero) zero) + (a' := pair (succ (succ zero)) (succ zero)) + (p := Eq_refl);

Yay!

Tho, more useful would be a Rational library (based on `Int` or `Integer` rather than `Nat`). Will/would require adding various axioms about the properties of our builtin operations on `Int`s (and `Integer`s).

index b78d940..941e7af 100644 --- a/src/unification.ml +++ b/src/unification.ml @@ -561,6 +561,9 @@ and unify_sortlvl (matching : scope_level option) -> (* FIXME: This SLlub representation needs to be * more "canonicalized" otherwise it's too restrictive! *) (unify' l11 l21 ctx vs matching)@(unify' l12 l22 ctx vs matching) + | SLlub (l1, l2), other | other, SLlub (l1, l2) + when OL.conv_p ctx l1 l2 + -> unify' l1 (mkSortLevel other) ctx vs matching | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]) | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]

This should probably belong in a separate commit

Stefan