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

[Peter Brottveit Bock]

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