[Ur] Result monad

[Urs Wegmann]

Thank your for your input! I changed it to the following and in seems to do what I want now:

datatype result x a =
  Ok of a
| Err of x

fun mreturn [x] [a] (r : a) : result x a = Ok r

fun mbind [x] [a] [b] (r : result x a) (f : a -> result x b) : result x b =
  case r of
    Ok r => f r
  | Err x => Err x

val result_monad = fn [x ::: Type] => mkMonad
  {
    Return = @@mreturn [x],
    Bind = @@mbind [x]
  }

From: Ur <ur-bounces at impredicative.com> On Behalf Of Adam Chlipala
Sent: Thursday, 6 February 2020 19:40
To: ur at impredicative.com
Subject: Re: [Ur] Result monad

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.