... suite:
let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) -let eq_refl =
+(* FIXME: Is this the best way to do this? Originally, I wanted to
define this in Typer and then reference it from OCaml code.- *)
Comme discuté, c'est possible que ce soit le mieux qu'on puisse faire pour l'instant, en effet :-( Quoique... voir ci-dessous.
+(* Defining the following:
- typecons Interval i0 i1
- *)
+let type_interval = mkInductive (dsinfo, (dloc, "Interval"), [],
List.fold_left (fun m name -> SMap.add name [] m)SMap.empty["i0"; "i1"])
SVP évite de dépasser les 80 colonnes (e.g. ajoute un line-break juste avant le `=`).
+let eq_eq =
- (* Variables for the type level, type and the function (I -> ?A) *)
- let lv = (dsinfo, Some "l") in
- let tv = (dsinfo, Some "t") in
- let fv = (dsinfo, Some "f") in
- mkBuiltin ((dloc, "Eq.eq"),
mkArrow (dsinfo, Aerasable, lv,type_level,mkArrow (dsinfo, Aerasable, tv,mkSort (dsinfo, Stype (mkVar (lv, 0))),mkArrow (dsinfo, Anormal, fv,mkArrow (dsinfo, Aerasable, (dsinfo, None),type_interval,mkVar (tv, 1)),mkCall (dsinfo, type_eq,[Aerasable, mkVar (lv, 2);Aerasable, mkVar (tv, 1);Anormal, mkCall (dsinfo, mkVar (fv, 0),[Aerasable, interval_i0]);Anormal, mkCall (dsinfo, mkVar (fv, 0),
Hmm... je cois qu'on faisait déjà ça pour `eq_refl` (où "ça", c'est de définir le builtin à double: une fois ici en OCaml et une fois en Typer. C'est redondant et en plus je ne suis pas sûr si le code vérifie que les deux types sont égaux).
Je pense qu'on aurait intérêt à utiliser un predef ici. Je vois que `eq_refl` était utilisé dans `opslexp.ml` et que maintenant tu utilises `eq_eq` au même endroit, donc on en a besoin tôt (avant de finir de lire `builtins.typer`), mais on devrait pouvoir utiliser un hack comme celui que j'utilise pour `Macro` (c.f. la définition de `predef_map` où je mets une version dummy de `Macro`), du moins tant qu'on utilise pas *vraiment* `eq_eq` dans `builtins.typer`.
C'est probablement vrai pour `Eq_uneq` aussi.
(* easier to debug with type annotations *) type env_elem = (vname * varbind * ltype) diff --git a/src/env.ml b/src/env.ml index f60f0f3..77e3cb4 100644 --- a/src/env.ml +++ b/src/env.ml @@ -63,6 +63,7 @@ type value_type = | Vref of (value_type ref) | Velabctx of DB.elab_context | Varray of (value_type array)
- | Veq of value_type (* TODO: Do I need a runtime value of an equality proof? *)
Notre printer devrait prendre non seulement une `value_type` en argument, mais aussi son `ltype` (ou au moins la version `elexp` de son `ltype`), par exemple pour correctement imprimer une valeur de type `τ₁ ≡> τ₂` 🙂. Donc nos preuves d'égalité n'ont pas besoin d'être représentées par des valeurs qui disent "je suis une preuve d'égalité".
Ceci dit, c'est OK d'ajouter `Veq` pour l'instant (la performance ne nous préoccupe pas vraiment et ça peut faciliter le debugging).
- | Veq v -> let v' = value_string v in
v' ^ " = " ^ v' (* FIXME: Is this always correct? *)
What do you mean by "correct"? What kind of problem are you worried about?
+let eq_eq loc _ vs = match vs with
- | [v] -> Veq v
- | _ -> error loc "Eq_eq takes a single value as argument"
+let eq_uneq loc _ vs = match vs with
- | [_x; _y; Veq v] -> v
- | _ -> error loc "Eq_uneq takes 3 arguments"
Hmm... now I realize we do have a real problem:
If the `f` arg to `Eq_eq` is erased, then `eq_uneq` cannot return it, really. Because at run time, we can't extract that from the equality proof if it's erased.
So, instead of something like
Eq_uneq : Eq ?x ?y → (I ≡> τ);
we'd need something like:
Eq_uneq : Eq ?x ?y → ((f : I ≡> τ) ≡> ?α) → α
I.e. a kind of "let" version of "uneq" so we can mark the `f` erased. But that doesn't work for `eq_uneq_whnf` any more :-(
Hmm....
So we have to keep the `f` argument of `Eq_eq` as non-erased, indeed!!
diff --git a/src/opslexp.ml b/src/opslexp.ml index b18a7ea..d08d170 100644
....la suite au prochain épisode,
Stefan
Afficher les réponses par date
... suite:
diff --git a/src/opslexp.ml b/src/opslexp.ml index b18a7ea..d08d170 100644 --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -190,10 +190,10 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = lexp_whnf (mkCall (l, push_susp body (S.substitute (lexp_whnf arg ctx)), args)) ctx
| Call (l, f', xs1) -> mkCall (l, f', List.append xs1 xs)
| Call (l, f', xs1) -> lexp_whnf (mkCall (l, f', List.append xs1 xs)) ctx
Yup.
| Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with
| Some f -> Option.value ~default:e (f ctx args)
| Some f -> Option.value ~default:e (f ctx xs) | None -> e) | _ -> e) (* Keep `e`, assuming it's more readable! *)
[...]
@@ -289,18 +290,29 @@ and lexp'_whnf e (ctx : DB.lexp_context) : lexp' =
and eq_cast_whnf ctx args = match args with
- | [_l; _t; _x; _y; (_, p); _f; (_, fx)]
- | [_l1; _l2; _t; _x; _y; (_, p); _f; (_, fx)] -> (match lexp'_whnf p ctx with
| Call (_, refl, _) when conv_p ctx refl DB.eq_refl
| Call (_, eq, _) when conv_p ctx eq DB.eq_eq -> Some (lexp_whnf fx ctx) | _ -> None)
Good.
@@ -203,10 +203,11 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in
mkCall (l, DB.eq_refl,[Pexp.Aerasable, elevel;Pexp.Aerasable, etype;Pexp.Aerasable, e]) in
let constFunction = mkLambda (Pexp.Aerasable, (dsinfo, None), etype, e) inmkCall (l, DB.eq_eq,[Pexp.Aerasable, elevel;Pexp.Aerasable, etype;Pexp.Anormal, constFunction]) in let reduce it name aargs = let targs = match lexp'_whnf it ctx with | Inductive (_,_,fargs,_) -> fargs
It's probably worthwhile moving this to a separate function `mk_eq_witness` or some such.
+and eq_uneq_whnf ctx args =
- match args with
- | [_l; _t; (_, x); (_, y); _p; (_, i)]
- -> if conv_p ctx i DB.interval_i0
then Some (lexp_whnf x ctx)else if conv_p ctx i DB.interval_i1then Some (lexp_whnf y ctx)else None- | _ -> None
Good, compte tenu de la convention d'appel actuelle des "reducible_builtins". Mais cette convention d'appel devrait être changée:
- There can also be more arguments. Same thing with `Eq.cast` and probably most other builtins for which we'll want to add rules. So I think that we should return `Some (newexp, args)` where `args` are the "leftover" args. - Also, I think it'd be better to let the caller apply `lexp_whnf` to the result, since it's probably going to be useful for all the "reducible_builtins".
Voilà,
Stefan
So we have to keep the `f` argument of `Eq_eq` as non-erased, indeed!!
Actually, that's not quite true: we can get the runtime info needed for `Eq.uneq` to return the proper function either from the `Eq.eq` object (like you have currently), or from the `x` and `y` args passed to `Eq.uneq`.
IOW, we could make all `Eq.eq` arguments erasable, and instead make the `x` and `y` args to `Eq.uneq` non-erasable.
My first reaction to seeing `Eq.eq` take a non-erasable arg was one of horror, but after thinking some more about it, it's probably not that bad: it's still a "singleton type" (i.e. compatible with axiom K), so we can still make the proof passed to `Eq.cast` erasable, and equality proofs themselves are still almost universally erasable.
Stefan
Je pense que c'est mieux de renommer le combinateur `I`. En Haskell ça s'appelle `id`, donc on pourrait utiliser ça.
OK!
Pas sûr si c'est mieux, mais tu devrais pouvoir faire ce qu'on fait pour les booléens (via `predef_names` in `src/builtin.ml`).
Comme discuté, je pense que ce serait pas trivial d'implémenter ça car le type `Interval` et les fonctions `eq_eq` et `eq_uneq` sont référencés dans des endroits où on a pas accès au contexte d’élaboration (ce qui est nécessaire pour utiliser la fonction `get_predef`). Néanmoins, je pense que ce serait possible d’éviter de redéfinir le type de `eq_eq` et `eq_uneq` en Typer.
Side note: il serait bon de vérifier qu'on peut définir la version "hétérogène":
Eq_eq' : (t : Interval ≡> Type) ≡> (f : (i : ?) ≡> t (_ := i)) -> Eq (f (_ := i0)) (f (_ := i1));
Ca devrait pas poser trop de problèmes, je vais travailler là-dessus.
Je pense que pour l'instant on a pas de réductions sur `Eq_cast` dans `conv_p` mais il serait bon d'en ajouter pour qu'on puisse avoir
Eq_refl : Eq "hello" hello;
C’est noté :)
Je crois que `= Eq_refl;` est un peu optimiste vu que ça dépend de `notnot=id` et je ne vois pas de manière simple d'obtenir `notnot=id` de manière définitionnelle. En gros, ça nécessiterait de tester l'équivalence extensionnelle des fonctions passées aux deux `Eq_eq` et si on fait ça de manière définitionnelle, j'ai l'impression que ça donne l'axiome K, aka UIP.
Avec le recul, je suis d’accord que c’était plutôt optimiste de ma part. J’étais inspiré par ce qui était possible dans Cubical Agda, il y a clairement plus d’égalités qui tiennent de manière définitionnelle dans leur système. Mais ce serait quand même bien de pouvoir prouver `Eq (Eq_comm (Eq_comm p)) p`, je suis pas sûr si je pourrai y arriver par contre, à investiguer…
Notre printer devrait prendre non seulement une `value_type` en argument, mais aussi son `ltype` (ou au moins la version `elexp` de son `ltype`), par exemple pour correctement imprimer une valeur de type `τ₁ ≡> τ₂` 🙂.
C’est une bonne idée d’améliorer le printer, je compte garder le `Veq` mais ça ne portera plus une “valeur” lors de l’execution.
What do you mean by "correct"? What kind of problem are you worried about?
“Correct” était peut-être pas le meilleur mot pour communiquer mes intentions. Si on a une égalité `x = y`, il me semblait pas flexible de toujours afficher la forme normalisée de `x` et `y`, je pensais que ce serait mieux d’afficher ce que sont réellement X et Y et c’est ce que je compte faire dans la version améliorée du printer.
It's probably worthwhile moving this to a separate function `mk_eq_witness` or some such.
- There can also be more arguments. Same thing with `Eq.cast` and
probably most other builtins for which we'll want to add rules. So I think that we should return `Some (newexp, args)` where `args` are the "leftover" args.
- Also, I think it'd be better to let the caller apply `lexp_whnf` to
the result, since it's probably going to be useful for all the "reducible_builtins".
Ok!
IOW, we could make all `Eq.eq` arguments erasable, and instead make the `x` and `y` args to `Eq.uneq` non-erasable.
J’avoue que j’y avais pensé du tout. Je pense que c’est le mieux qu’on puisse faire pour le moment, merci pour l’astuce!
James
Le 19 juin 2023 à 20:12, Stefan Monnier monnier@iro.umontreal.ca a écrit :
So we have to keep the `f` argument of `Eq_eq` as non-erased, indeed!!
Actually, that's not quite true: we can get the runtime info needed for `Eq.uneq` to return the proper function either from the `Eq.eq` object (like you have currently), or from the `x` and `y` args passed to `Eq.uneq`.
IOW, we could make all `Eq.eq` arguments erasable, and instead make the `x` and `y` args to `Eq.uneq` non-erasable.
My first reaction to seeing `Eq.eq` take a non-erasable arg was one of horror, but after thinking some more about it, it's probably not that bad: it's still a "singleton type" (i.e. compatible with axiom K), so we can still make the proof passed to `Eq.cast` erasable, and equality proofs themselves are still almost universally erasable.
Stefan
Pas sûr si c'est mieux, mais tu devrais pouvoir faire ce qu'on fait pour les booléens (via `predef_names` in `src/builtin.ml`).
Comme discuté, je pense que ce serait pas trivial d'implémenter ça car le type `Interval` et les fonctions `eq_eq` et `eq_uneq` sont référencés dans des endroits où on a pas accès au contexte d’élaboration (ce qui est nécessaire pour utiliser la fonction `get_predef`).
OK, je suis allé voir pourquoi on a besoin du elab_context:
let get_predef (name: string) (ctx: DB.elab_context) : lexp = try let r = (DB.get_size ctx) - !builtin_size - 0 in let p = SMap.find name (!predef_map) in mkSusp p (S.shift r) with Not_found -> log_raise_error {|"%s" was not predefined|} name
[...ailleurs...]
let get_size (ctx : elab_context) = let (_, (n, _), lctx, _, _) = ctx in assert (n = M.length lctx); n
donc on a besoin du elab_context parce que `DB.get_size` prend un `elab_context` pour en extraire le `n` qui contient la taille du `lexp_context`, mais on pourrait aussi le calculer sur la base du `lexp_context`, sauf que c'est O(log N) au lieu de O(1).
:-(
Et tout ça pour faire un `S.shift` que l'on pourrait complètement éviter en évitant les indices de DeBruijn dans les predefs :-)
Je remarque cependant que t'as seulement besoin de `DB.eq_eq` (qui remplace `DB.eq_refl`) mais pas de `DB.eq_uneq`, donc on peut éliminer la définition en OCaml du type de `eq_uneq`.
Stefan
J’ai attaché 2 fichiers, `update.patch` qui contient les modifications que j’ai effectuées depuis le dernier patch et `full.patch` qui contient tout.
Pour résumer rapidement les changements dans `update.patch`:
- Le changement de nom `Interval` en `I`
- L’argument (f : I ≡> t) dans `Eq_eq` a été rendu effaçable, par conséquent la preuve d’égalité dans Eq_uneq est aussi effaçable.
- L'equivalence η des fonctions, ce qui nous permet d’écrire Eq_funext : (f : ? -> ?) => (g : ? -> ?) => ((x : ?) -> Eq (f x) (g x)) -> Eq f g; A part l’ajout du traitement de η dans `conv_p`, c’était aussi nécessaire d’ajouter la même logique dans l’unification des lambdas. Dans la fonction `unify’`, est-ce que c’est nécessaire de traiter les branches dans cet ordre? Par exemple, est-ce que ce serait correct de traiter d’abord les Vars avant les Lambdas?
- Petite amélioration du printer: - Eval.print_eval_result prend un `ltype` optionnel comme paramètre, c’est utile notamment pour mieux afficher les expressions du type Eq et les fonctions qui ont des paramètres effaçables. - la REPL garde le type des expressions après l’appel à `check` et les fournit à Eval.print_eval_result
Et voila.
James
Le 24 juin 2023 à 11:01, Stefan Monnier monnier@iro.umontreal.ca a écrit :
Pas sûr si c'est mieux, mais tu devrais pouvoir faire ce qu'on fait pour les booléens (via `predef_names` in `src/builtin.ml`). Comme discuté, je pense que ce serait pas trivial d'implémenter ça car le type `Interval` et les fonctions `eq_eq` et `eq_uneq` sont référencés dans des endroits où on a pas accès au contexte d’élaboration (ce qui est nécessaire pour utiliser la fonction `get_predef`).
OK, je suis allé voir pourquoi on a besoin du elab_context:
let get_predef (name: string) (ctx: DB.elab_context) : lexp = try let r = (DB.get_size ctx) - !builtin_size - 0 in let p = SMap.find name (!predef_map) in mkSusp p (S.shift r) with Not_found -> log_raise_error {|"%s" was not predefined|} name
[...ailleurs...]
let get_size (ctx : elab_context) = let (_, (n, _), lctx, _, _) = ctx in assert (n = M.length lctx); n
donc on a besoin du elab_context parce que `DB.get_size` prend un `elab_context` pour en extraire le `n` qui contient la taille du `lexp_context`, mais on pourrait aussi le calculer sur la base du `lexp_context`, sauf que c'est O(log N) au lieu de O(1).
:-(
Et tout ça pour faire un `S.shift` que l'on pourrait complètement éviter en évitant les indices de DeBruijn dans les predefs :-)
Je remarque cependant que t'as seulement besoin de `DB.eq_eq` (qui remplace `DB.eq_refl`) mais pas de `DB.eq_uneq`, donc on peut éliminer la définition en OCaml du type de `eq_uneq`.
Stefan
Salut James,
Ça sonne très bien. J'ai pas encore eu le temps de regarder, mais pourrais-tu pousser ça sur une branche dans le Git?
Stefan
Salut Stefan,
Oui bien sûr, je viens de demander l’accès au répo Git.
James
Le 5 juill. 2023 à 08:53, Stefan Monnier monnier@iro.umontreal.ca a écrit :
Salut James,
Ça sonne très bien. J'ai pas encore eu le temps de regarder, mais pourrais-tu pousser ça sur une branche dans le Git?
Stefan
-
James Juan Whei Tan -
Stefan Monnier