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-boun...@impredicative.com> On Behalf Of Adam Chlipala
Sent: Thursday, 6 February 2020 19:40
To: ur@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.
_______________________________________________
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
