Re: [Ur] Generating fresh name (gensym :: {Unit} -> Name).
On 07/09/2017 05:58 PM, Peter Brottveit Bock wrote: You mean something like val lolli_right'' : n :: Name -> [[n] ~ gamma] => t0 ::: Type -> t1 ::: Type -> gamma ::: {Type} -> (n :: Name -> [[n] ~ gamma] => lin (gamma ++ [n = t0]) t1) -> lin gamma (lolli t0 t1) ? Yeah, that would be possible to implement, but it wouldn't really be an improvement, would it? Yes, that's what I meant. The added benefit is that you really do have exactly the proof terms you were looking for; they just have these extra names tacked on them, but you can ignore those from a formal perspective! ___ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
Re: [Ur] Generating fresh name (gensym :: {Unit} -> Name).
Thanks for the quick reply! On Sun, 9 Jul 2017, at 23:22, Adam Chlipala wrote: > Short answer: I can't think of any way to implement that feature, with > Ur as it stands today. > > It seems consistent with the model of Ur in Coq, though the > representation of rows might need to be extended to allow iteration even > without a folder (to find a fresh name). I honestly hadn't thought about the possibility of defining it within Ur, but that's of course something I should have thought about. Anyway, to extend Ur so that it is possible would require a non-trivial effort I guess. > Well, you could combine the two: take in a polymorphic premise, but also > ask for a concrete disjoint name to be passed at the top level. The > implementation can instantiate the premise with the concrete name. You mean something like val lolli_right'' : n :: Name -> [[n] ~ gamma] => t0 ::: Type -> t1 ::: Type -> gamma ::: {Type} -> (n :: Name -> [[n] ~ gamma] => lin (gamma ++ [n = t0]) t1) -> lin gamma (lolli t0 t1) ? Yeah, that would be possible to implement, but it wouldn't really be an improvement, would it? — Peter ___ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
Re: [Ur] Generating fresh name (gensym :: {Unit} -> Name).
On 07/09/2017 05:11 PM, Peter Brottveit Bock wrote: Is it possible to generate a fresh name relative to some collection of names? I.e. something of kind "gensym :: {Unit} -> Name". Short answer: I can't think of any way to implement that feature, with Ur as it stands today. Does it break some nice meta-properties of Ur/Web? It seems consistent with the model of Ur in Coq, though the representation of rows might need to be extended to allow iteration even without a folder (to find a fresh name). I have two possible types which can be used to represent this: val lolli_right : t0 ::: Type -> t1 ::: Type -> gamma ::: {Type} -> (n :: Name -> [[n] ~ gamma] => lin (gamma ++ [n = t0]) t1) -> lin gamma (lolli t0 t1) and val lolli_right' : n ::: Name -> t0 ::: Type -> t1 ::: Type -> gamma ::: {Type} -> [[n] ~ gamma] => lin (gamma ++ [n = t0]) t1 -> lin gamma (lolli t0 t1) The first type is arguably nicer, since when used as a proof term, it actually binds the name "n" locally. The second version works, but it's not a binder proper, so it "pushes" the problem of finding a suitable name further out. Said another way, the first version is modular while the second is not. While it is straight forward to implement the second version, I can not immediately see a way to implement the first one, without a way to generate a fresh name. Well, you could combine the two: take in a polymorphic premise, but also ask for a concrete disjoint name to be passed at the top level. The implementation can instantiate the premise with the concrete name. ___ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
[Ur] Generating fresh name (gensym :: {Unit} -> Name).
Hello Ur/Web'ers, Is it possible to generate a fresh name relative to some collection of names? I.e. something of kind "gensym :: {Unit} -> Name". Does it break some nice meta-properties of Ur/Web? To give some context for why I'm thinking about this: I've played a bit with Ur/Web, and I just tried to embed linear logic into Ur/Web's type system. I've put some of what I've done in a github repository here: https://github.com/peterbb/ur-linear. The basic idea is to define a type "lin :: {Type} -> Type -> Type", where the intuition of "lin gamma tau" is that an object of "tau" can be produced linearly from the a record "$gamma" (this is similar to the box type found in contextual modal type theory). Using Ur/Web's module system to hide the definition of "lin" and exposing functions correspond to the rules of inference of linear logic, it seems to me that one gets a faithful shallow representation of linear logic. The rules where generation of fresh names would be useful, are rules that have binders. Consider the inference rule for lollipop in a two-sided sequent calculus: Gamma, n : t0 |- t1 - Gamma |- t0 -o t1 I have two possible types which can be used to represent this: val lolli_right : t0 ::: Type -> t1 ::: Type -> gamma ::: {Type} -> (n :: Name -> [[n] ~ gamma] => lin (gamma ++ [n = t0]) t1) -> lin gamma (lolli t0 t1) and val lolli_right' : n ::: Name -> t0 ::: Type -> t1 ::: Type -> gamma ::: {Type} -> [[n] ~ gamma] => lin (gamma ++ [n = t0]) t1 -> lin gamma (lolli t0 t1) The first type is arguably nicer, since when used as a proof term, it actually binds the name "n" locally. The second version works, but it's not a binder proper, so it "pushes" the problem of finding a suitable name further out. Said another way, the first version is modular while the second is not. While it is straight forward to implement the second version, I can not immediately see a way to implement the first one, without a way to generate a fresh name. — Peter Brottveit Bock ___ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur