[Ur] using mapR

Adam Chlipala adamc at impredicative.com
Thu Sep 29 09:49:27 EDT 2011


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.

Gergely Buday wrote:
> I would like to fix type constraints for using Monad.mapR so that I
> need not pass them when using for creating sources of values. I do not
> understand what this error message say, let alone fix the bug. How
> should I fix my code?
>
> - Gergely
>
> $ urweb mapr
> /home/gergoe/local/sandbox/sandbox/mapr.ur:2:5-2:16: Expression is not
> a constructor function
> Expression:  Monad.mapR[[<UNIF:R>]] [<UNIF:A::Type ->  Type>]
>        Type:
> ((Basis.monad<UNIF:A::Type ->  Type>) ->
>    tf ::<UNIF:R>  ->  Type ->
>     tr ::<UNIF:R>  ->  Type ->
>      ((nm :: Name ->
>         t ::<UNIF:R>  ->  ((tf t) ->  <UNIF:A::Type ->  Type+4>  (tr t)))
>        ->
>        r ::: {<UNIF:R>} ->
>         ((Top.folder[[<UNIF:R>]] r) ->
>           ($(map tf r) ->  <UNIF:A::Type ->  Type+3>  $(map tr r)))))
> $ head -3 mapr.ur
>
> fun sourceRecord [ r ::: {Type} ] (fl : folder r) (record : $r) :
> (transaction $(map source r)) =
> 	    @Monad.mapR  [id] [source] fl  (fn [nm :: Name] [t :: Type]  =>
> source  ) fl record
>    




More information about the Ur mailing list