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