[Ur] Troubles writing error monad
Sergey Mironov
grrwlf at gmail.com
Tue Jun 9 19:19:15 EDT 2015
Hi. I am trying to write an [Error] monad. So far I've managed to
write the code (see below), which is rejected by the compiler with the
following message:
/home/grwlf/proj/urweb-etab/lib/urweb-monad-pack/error.ur:42:2: (to
42:95) Constructor unification failure in signature matching:
Have: val monad_error : e ::: Type -> monad S.m
Need: val monad_error : e ::: Type -> monad (error e)
Con 1: e ::: Type -> monad S.m
Con 2: e ::: Type -> monad (fn a :: Type => S.m (either e a))
Incompatible constructors
Have: S.m
Need: (fn a :: Type => S.m (either e a)
Could you please help me to understand its meaning? I have very
similar State monad which compiles without problem
(https://github.com/grwlf/urweb-monad-pack/blob/master/state.ur).
Intuition says me that the compiler is confused by the [either]
datatype, am I correct? If so, what can I use in place of it to make
the monad work?
Regards,
Sergey
---
(* error.ur *)
datatype either l r = ELeft of l | ERight of r
functor Trans(S :
sig
con m :: Type -> Type
val monad_m : monad m
end) :
sig
con error :: Type -> Type -> Type
val unError : e ::: Type -> a ::: Type -> error e a -> S.m (either e a)
val run : e ::: Type -> a ::: Type -> error e a -> S.m (either e a)
val fail : e ::: Type -> a ::: Type -> e -> error e a
val monad_error : e ::: Type -> monad (error e)
end =
struct
con error = fn e => fn a => S.m (either e a)
fun unError [e] [a] (m:error e a) : S.m (either e a) = m
val run [e] [a] (m:error e a) = unError m
val fail [e] [a] (err:e) = (return (ELeft err))
fun mreturn [e] [a] (r:a) : error e a = (return (ERight r))
fun mbind [e] [a] [b] (m1 : error e a) (m2 : a -> error e b) : error e b =
( r <- unError m1;
case r of
| ELeft e => return (ELeft e)
| ERight a => unError (m2 a))
val monad_error = fn [e ::: Type] => (mkMonad { Return = @@mreturn
[e], Bind = @@mbind [e] })
end
More information about the Ur
mailing list