[Ur] Result monad

[Adam Chlipala]

In this case, I think the straightforward answer is that result is 
clearly not a monad, just on the basis of its kind!  However, for any 
fixed x, fn a => result a x can be a monad.  I suggest reformulating 
your last definition to be polymorphic in that way.  Probably everything 
resolves most nicely if you swap the order of arguments to result.

On 2/6/20 1:34 PM, Urs Wegmann wrote:
>
> I try to create a monad:
>
> datatype result a x =
>
>   Ok of a
>
> | Err of x
>
> fun mreturn [a] [x] (r : a) : result a x = Ok r
>
> fun mbind [a] [b] [x] (r : result a x) (f : a -> result b x) : result 
> b x =
>
>   case r of
>
>     Ok r => f r
>
>   | Err x => Err x
>
> val result_monad = mkMonad
>
>   {
>
>     Return = @@mreturn,
>
>     Bind = @@mbind
>
>   }
>
> I think the error message tries to tell me that x is not defined 
> enough. Is there a way to fix this? When I remove x from result, it 
> compiles.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20200206/9d3f4fa5/attachment.html>