[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