Re: [Ur] Result monad

2020-02-06 Thread 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 |

Re: [Ur] Result monad

2020-02-06 Thread 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

[Ur] Result monad

2020-02-06 Thread 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 {