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)])
This should probably belong in a separate commit
Stefan