[Ur] Result monad

[Urs Wegmann]

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/a3504c60/attachment.html>