[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