[Ur] Variable record projection using free variables

[Ron de Bruijn]

Hi,

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). *)
val unknown = fn ??????

The following 'solution' doesn't work, because it is not constrained
by depending on the type of r.

(* val unknown_candidate_failure = fn [nm::Name] => f nm r  *)

Best regards,
 Ron de Bruijn