[Ur] using mapR
Adam Chlipala
adamc at impredicative.com
Thu Sep 29 10:13:39 EDT 2011
Gergely Buday wrote:
>> By prefacing [Monad.mapR] with [@], you have requested that type class
>> arguments be passed explicitly. Membership in the class [monad] is an
>> example of such an argument, and you can see it early in the type of [mapR]
>> (and it appears first in the error message). That argument should go first,
>> before [[id]]. Just put an underscore in that position and it should work.
>>
> For some reasons it doesn't:
>
> [gergoe at flagship sandbox]$ head -3 mapr.ur
> fun sourceRecord [ r ::: {Type} ] (fl : folder r) (record : $r) :
> (transaction $(map source r)) =
> @Monad.mapR [_] [id] [source] (fn [nm :: Name] [t :: Type] =>
> source ) fl record
>
Just an underscore, with no brackets around it, because this is a
value-level, not type-level, argument.
More information about the Ur
mailing list