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 [_] [_] [_])
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
