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 _______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
