[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