[Ur] Generating fresh name (gensym :: {Unit} -> Name).

[Adam Chlipala]

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.