June 2023 - Typer - mailman.iro.umontreal.ca

Re: [Typer] pp_print
by Stefan Monnier 14 Jul '23

14 Jul '23

> Dans cette branche, j'escape les symboles et les noms de variable. > > https://gitlab.com/monnier/typer/-/compare/main...simon--escape-symbols > > Dites-moi si ça vous convient. LGTM, please push. sauf: c <> ' ' devrait être c > ' ' vu que Typer considère tous les charactères <= 32 comme du whitespace. Stefan

1 1

Re: [Typer] Implémentation du type Interval
by Stefan Monnier 05 Jul '23

05 Jul '23

... 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

2 7

Cubicalish thingies
by Stefan Monnier 19 Jun '23

19 Jun '23

Cubical Agda represents equality proofs as functions from an "interval" (a structure with two end points I₀ and I₁) to some type, such that if we have such a function `f : I → τ` then it is considered as proof that `Eq (f I₀) (f I₁)`. This works because those functions from I are special: the operations provided on I are limited such that they basically can't examine whether they have an I₀ or an I₁. So they're necessarily "constant functions". In Typer we can represent a similar idea using erasable arguments: Eq.eq : (f : Bool ≡> ?τ) → Eq (f true) (f false); notice the `≡>` on the type of `f` which means that this function can't use its boolean argument in any significant way because it'll be erased. So `Eq x y` basically is a proof that we were able to provide a constant function that returns `x` or `y` depending on a boolean that it's not allowed to use. [ Note: in reality, Typer's erasable arguments are also implicit, so rather than `f true` we have to write `f (_ := true)` to explicitly provide those erasable arguments. But I'll write it the sloppy way in this message. ] So we can define our usual reflection constructor: Eq.refl : Eq ?x ?x; Eq.refl = Eq.eq (λ_ ≡> ?x); things To be interesting, tho, we do need those functions to be not-quite-constant. For that reason, we add an eliminator Eq.uneq : (x : ?τ) → (y : ?τ) → Eq x y → Bool ≡> ?τ; with reduction rules: Eq.uneq x y eq true ↝ x Eq.uneq x y eq false ↝ y IOW, `Eq.uneq x y eq` returns a function which takes an erasable argument and returns different results depending on that argument. This is a bit weird since a function should not be allowed to look at its erasable argument, but it's exceptionally tolerated because we have a proof that the two possible return values are actually equal, so they're not really different after all. With that we can prove functional extensionality: funext : ((x : ?τ) → Eq (?f x) (?g x)) → Eq ?f ?g; funext eqf = Eq.eq (λ i ≡> λx → Eq.uneq (?f x) (?g x) (eqf x) i); What's so special about an erasable `Bool` (a.k.a `I`), tho? We can generalize the above to any function taking an erasable argument: Const : (τ₁ → τ₂) → Type; Const.in : (f : τ₁ ≡> τ₂) → Const (λx → f x); Const.out : (f : τ₁ → τ₂) → Const f → τ₁ ≡> τ₂; such that Const.out f cst x ↝ f x And we can recover the old `Eq` with: Eq x y = Const (λi → if i then x else y); But when we try to prove functional extensionality: funext : ((x : ?τ) → Const (λi → if i then ?f x else ?g x)) → Const (λi → if i then ?f else ?g); funext eqf = Const.in (λi ≡> λx → Const.out (λi → if i then ?f x else ?g x) (eqf x) i) ↝ Const.in (λi ≡> λx → if i then ?f x else ?g x); [ Let's disregard the fact after this reduction `i` is used in a way that's incompatible with an erasable argument. ] This does not have the desired type because Const (λi → if i then ?f else ?g); ≠ Const (λi → λx → if i then ?f x else ?g x) We'd need functional extensionality to prove functional extensionality :-( So, in a sense, what's special about `Eq x y` compared to `Const f` is that it provides an extensional representation of the constant function: `Const f` exposes the intensional definition of `f`, which ends up being too detailed for what we want. In constrast `Eq.eq` returns an `Eq x y` whose type hides the intensional definition of the witness function, which is key to making it possible to prove `funext`. Stefan

1 0

Re: [Typer] Implémentation du type Interval
by Stefan Monnier 15 Jun '23

15 Jun '23

> Pour éviter que le patch soit signalé comme malveillant, je lui ai donné une > extension `.txt`. FWIW, j'ai encore pas eu de problèmes avec des attachments `text/x-diff` et/ou extensions `.diff` ou `.patch` :-) > Au début, je voulais nommer le type interval `I` mais le nom a déjà été pris > par le combinateur I, donc j’ai fini par le nommer `Interval`. Je pense que c'est mieux de renommer le combinateur `I`. En Haskell ça s'appelle `id`, donc on pourrait utiliser ça. > Je voulais également définir le type interval en Typer, mais j’avais > du mal à référencer le type en OCaml de manière satisfaisante, j’ai > fini donc par le définir dans `debruijn.ml`, peut-être que vous auriez > une meilleure idée. 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`). > Dans `samples/cubical.typer`, j’essayais de prouver que `(Eq_comm (Eq_comm > p)) = p`. Je pensais que si le typechecker était capable de faire la > réduction `Eq_uneq (Eq_eq f) i = f (_ := i)`, je pourrais donc compléter la > preuve, mais encore faut-il que le typechecker puisse utiliser le lemme qui > dit que `not (not i) = i`. Le typechecker ne sait pas utiliser des lemmes, donc ça ne va probablement pas marcher "juste par réduction" :-( > %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l > %% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l > + > +Eq_eq : (l : TypeLevel) ≡> (t : Type_ l) > + ≡> (f : Interval ≡> t) > + -> Eq (f (_ := i0)) (f (_ := i1)); > +Eq_eq = ##Eq\.eq; 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)); Et peut-être qu'il serait mieux d'utiliser la version hétérogène pour le "builtin" et définir la version homogène (pour laquelle l'inférence de types devrait mieux fonctionner) par dessus, plutôt que l'inverse. Mais, pour ça, je pense qu'il faudra redéfinir `Eq`. > +Eq_uneq : (l : TypeLevel) ≡> (t : Type_ l) > + ≡> (x : t) => (y : t) > + => Eq x y -> (Interval ≡> t); > +Eq_uneq = ##Eq\.uneq; Même chose ici. > -Eq_refl : ((x : ?t) ≡> Eq x x); > +Eq_refl : (l : TypeLevel) ≡> (t : Type_ l) > + ≡> (x : t) => Eq x x; Hmm... on change ≡> en => ... Si je comprends bien c'est à cause du "->" dans le type de `Eq_eq`, mais je crois que ce "->" peut-être changé en "≡>" aussi (sinon, ça veut dire que nos preuves d'égalité portent vraiment de l'information et donc qu'elles ne sont pas effaçables). > -Eq_refl = ##Eq\.refl; > +Eq_refl = lambda (l : TypeLevel) ≡> lambda (t : Type_ l) ≡> > + lambda (x : t) => Eq_eq (lambda _ ≡> x); A.k.a Eq_refl = lambda l ≡> lambda t ≡> lambda x => Eq_eq (lambda _ ≡> x); [ Side note: autour de `Eq` il y a souvent besoin de passer explicitement des arguments effaçables, ce qui suggère qu'il serait utile de pouvoir définir certains arguments effaçable comme étant "effaçables mais pas implicites". ] > -Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x; > +Eq_comm : (x : ?t) => (y : ?t) => Eq x y -> Eq y x; 🙁 > -Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) > - %% FIXME: The code is incorrectly accepted even > - %% without this `(p := p)` because we just get a > - %% metavar which remains uninstantiated and then > - %% the definition gets ignored in the runtime > - %% environment (see Eval.from_lctx). > - (p := p) > - Eq_refl; > +Eq_comm p = Eq_eq (lambda i ≡> Eq_uneq p (_ := Interval_not i)); 🙂 > +%% If `y=z` is taken to be unnecessary, this implies that we could define > +%% Eq_broken_trans : Eq ?x ?y -> Eq ?x ?z; > +Eq_trans : (x : ?t) => (y : ?t) => (z : ?t) => Eq x y -> Eq y z -> Eq x z; > +Eq_trans x=y = lambda y=z -> Eq_cast (p := y=z) (f := lambda x' -> Eq x x') x=y; Good. > +%% FIXME: The below code is accepted even in the absence of `p := y=z`. !!! > +Eq_funext : (f : ? -> ?) => (g : ? -> ?) => > + ((x : ?) -> Eq (f x) (g x)) -> > + Eq (lambda x -> f x) (lambda x -> g x); > +Eq_funext p = Eq_eq (lambda i ≡> lambda x -> Eq_uneq (p x) (_ := i)); 🙂 > +%% FIXME: It'd be nice to be able to say `Eq f g` directly En effet. Pour ça, il faut ajouter η dans `conv_p`. Ça devrait pas être trop difficile. > +++ b/samples/cubical.typer Tu pourrais le mettre dans `HoTT.typer` :-) > +hello : String; > +hello = Eq_cast (p := reflString) (f := lambda x -> x) "hello"; 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; > +%% FIXME: This should be provable, need to reduce `(Eq_comm (Eq_comm p))` to `p`. > +%% It should be sufficient to add the following reduction: > +%% Eq_uneq (Eq_eq f) i = f (_ := i) Sounds good. > +%% and apply `notnot=id`. > +%% Eq_comm_inv : (x : ?t) => (y : ?t) => (p : Eq x y) -> Eq (Eq_comm (Eq_comm p)) p; > +%% Eq_comm_inv p = Eq_refl; 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. > --- a/src/debruijn.ml > +++ b/src/debruijn.ml J'me suis arrêté ici pour l'instant. Stefan

1 0

[Git][monnier/typer][gensym-without-spaces] Deleted 1 commit: Escape charaters like spaces when printing a symbol or vname.
by Simon Génier (＠ilovemonoids) 12 Jun '23

12 Jun '23

Simon Génier pushed to branch gensym-without-spaces at Stefan / Typer WARNING: The push did not contain any new commits, but force pushed to delete the commits and changes below. Deleted commits: 01dbc11d by Simon Génier at 2023-03-25T12:28:15-04:00 Escape charaters like spaces when printing a symbol or vname. - - - - - 4 changed files: - src/grammar.ml - src/sexp.ml - src/util.ml - tests/sexp_test.ml Changes: ===================================== src/grammar.ml ===================================== @@ -46,6 +46,9 @@ let find (name : string) (Grammar (ps) : t) : int option * int option = try SMap.find name ps with | Not_found -> (None, None) +let separate_chars = + CSet.of_list [','; '('; ')'; ';'] + (* A token_end array indicates the few chars which are separate tokens, * even if not surrounded by spaces, such as '(', ')', and ';'. * It also indicates which chars are "inner" operators, i.e. those chars @@ -54,13 +57,10 @@ let find (name : string) (Grammar (ps) : t) : int option * int option = type char_kind = | CKnormal | CKseparate | CKinner of int type token_env = char_kind array let default_stt : token_env = - let stt = Array.make 256 CKnormal - in stt.(Char.code ';') <- CKseparate; - stt.(Char.code ',') <- CKseparate; - stt.(Char.code '(') <- CKseparate; - stt.(Char.code ')') <- CKseparate; - stt.(Char.code '.') <- CKinner 5; - stt + let stt = Array.make 256 CKnormal in + CSet.iter (fun c -> stt.(Char.code c) <- CKseparate) separate_chars; + stt.(Char.code '.') <- CKinner 5; + stt (* default_grammar is auto-generated from typer-smie-grammar via: ===================================== src/sexp.ml ===================================== @@ -26,6 +26,17 @@ open Prelexer let sexp_error ?print_action loc fmt = Log.log_error ~section:"SEXP" ?print_action ~loc fmt +(** Prints an identifier in a way that reading it back will yield the same + identifier. Spaces, inner operators like ‘.’, and separate characters like + ‘,’ are escaped. *) +let pp_print_id (f : Format.formatter) (name : string) : unit = + let pp_print_escaped_char c = + if c = '.' || c = ' ' || CSet.mem c Grammar.separate_chars then + Format.pp_print_char f '\\'; + Format.pp_print_char f c + in + String.iter pp_print_escaped_char name + module Sym = struct type t = Source.Location.t * string @@ -53,7 +64,10 @@ module Sym = struct && name l = name r let pp_print (f : Format.formatter) (_, name : t) : unit = - Format.pp_print_string f name + pp_print_id f name + + let to_string : t -> string = + Format.asprintf "%a" pp_print end type symbol = Sym.t @@ -105,7 +119,7 @@ let string_of_vname ?(default : string = "<anon>") : vname -> string = function let pp_print_vname ?(default : string option) (f : Format.formatter) (name : vname) : unit = - Format.pp_print_string f (string_of_vname ?default name) + pp_print_id f (string_of_vname ?default name) (********************** Sexp tests **********************) ===================================== src/util.ml ===================================== @@ -22,6 +22,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) module SMap = Map.Make(String) module IMap = Map.Make(Int) +module CSet = Set.Make(Char) type location = Source.Location.t let dummy_location = Source.Location.dummy ===================================== tests/sexp_test.ml ===================================== @@ -87,5 +87,33 @@ let _ = "x = 4 : Int" "(_=_ x (_:_ 4 Int))" +let () = + add_test + "SEXP" + "Spaces are escaped in symbols" + (fun () -> + if + "Laura Palmer" + |> Sym.intern ~location:Source.Location.dummy + |> Sym.to_string + = "Laura\\ Palmer" + then + success + else failure) + +let () = + add_test + "SEXP" + "Dots are escaped in symbols" + (fun () -> + if + "DaleB.Cooper" + |> Sym.intern ~location:Source.Location.dummy + |> Sym.to_string + = "DaleB\\.Cooper" + then + success + else failure) + (* run all tests *) let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/-/commit/01dbc11da02b8e5e5896659d712e6e1ab… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/01dbc11da02b8e5e5896659d712e6e1ab… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch simon--escape-symbols
by Simon Génier (＠ilovemonoids) 12 Jun '23

12 Jun '23

Simon Génier pushed new branch simon--escape-symbols at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/simon--escape-symbols You're receiving this email because of your account on gitlab.com.

1 0