[Ur] sourcing a record

[Adam Chlipala]

Gergely Buday wrote:
> I would like to express a function that computes the source of each
> member of a record and produces a new record of them.
>
> Upon reading chapter 2 of the tutorial, I arrived to the following,
> which, of course, does not work:
>
> fun sourcify [ r ::: {Type} ] (record : r) : ($(map (fn n =>
> transaction (source n))) r) =
>      @fold [ fn t =>  transaction (source t)) ] (fn [nm ::_]  [ v::_]
> [r::_] [[nm=m]~r] value =>  [nm = source m ++ value]) {} record
>    

There are a number of basic problems here:
1. [r] is not a type, so you can't use it as the type annotation for an 
argument.
2. Assuming that issue is corrected, just the function type is already 
provably impossible to implement in any way but non-termination.  To 
allow use of a monad's effects, the return type must be in that monad.  
(Resources on monadic programming in Haskell may be useful to understand 
this point.)
3. Mismatched parens in the type argument to [fold]
4. Reference to an unbound variable [m]
5. Some (illegal) mixing of type-level and value-level syntax in the 
body of the anonymous function
6. The function doesn't take the right number of value-level arguments.  
As usual, a fold function takes both the next "list" item to process and 
the accumulator; your function only takes one argument [value].
7. Finally, the function can't possibly work unless it takes a [folder] 
as input and passes it off to [fold].  This is the only reason to 
preface [fold] with [@].

> How could this be written properly?
>    

I believe [Monad.mapR] from the standard library lets you accomplish 
what you want very simply, though it is probably useful to understand 
how to write your computation more directly.