[Ur] sourcing a record
Adam Chlipala
adamc at impredicative.com
Wed Sep 28 08:24:55 EDT 2011
Gergely Buday wrote:
> I stepped back to solve a simpler problem: an identity function on
> records using fold.
>
> fun identity [ r ::: {Type} ] (record : $r) : ($r) =
> fold [ fn t => $t ] (fn [nm ::_] [ v::_] [r::_] [[nm]~r] v => fn
> acc => ({nm = v} ++ acc )) () record
>
> but the compiler complains that I have too much arguments for the step function:
>
Sorry, I gave wrong advice before. The basic [fold] function only takes
an accumulator. However, to implement this function directly with
[fold], you'll want to pass an explicit type argument that makes the
accumulator type a function type, such that you then _would_ have two
value-level arguments to the anonymous function.
More information about the Ur
mailing list