[Ur] Variable record projection using free variables

[Adam Chlipala]

Ron de Bruijn wrote:
> I want to solve the following problem:
>
> Give a function unknown, such that unknown applied to [#X] returns
> (Some 1) and f applied to [#Y] returns (Some 2) in the following
> example, but any given solution should work for an unbounded number of
> fields in a free variable r.
>
> (* mem comes from the meta library *)
>
> val r = {X=Some 1,Y=Some 2}
> val f = fn [nm::Name] [l:::{Type}] [[nm=option int]~l] (x:
> $([nm=option int] ++ l))=>  proj (mem [nm] [option int] [l]) x
> val g = f [#Y] r (* This is sort of interesting, but still redundant
> (unknown [#Y] contains less tokens than f [#Y] r). *)
>    

...and a silly way of writing the function.  A simple [x.nm] would work 
in the body of [f], with no need to bring Mem into the picture.

You are probably looking for something like this:

val r = {X = Some 1, Y = Some 2}

fun grabber [nm :: Name] (m : mem nm (option int) [X = option int, Y = 
option int]) : option int =
     proj m r

val g = grabber [#Y] (mem [_] [_] [_])