Sorry for the very late and probably no longer relevant reply.
Building up on the exemple below, I have a problem with mixing effectful/effectless computations. For example, this would not compile:
noEff :: Exp NoEffect () noEff = return ()
hasEffect :: Exp Effect () hasEffect = do noEff <--- won't compile return ()
But it should: you should be able to run an effectless monad in an effectful one. How to encode this semantic?
This is a very, very common problem. We have an expression e of type T1, and we want to use it in the context that requires the type T2 (e.g., we want to pass 'e' to a function whose argument type is T2). We feel that we ought to be able to do that. One example is the one you cited: a computation that performs no effect can be regarded as a computation that _may_ perform an effect, and so we should be able to use a non-effectful expression in an effectful context. Another example is numerics: natural numbers are subset of rationals; so it should be morally OK to use a natural number where a rational is required. There are two ways of solving this problem. One is polymorphism, another is subtyping. In the first approach, we define noEff above with the polymorphic type:
noEff :: forall r. Exp r () noEff = return ()
This says that noEff can be used either in NoEffect or Effect contexts. Polymorphic terms can be regarded as `macros', at least conceptually, -- sort of as an abbreviation for the family of definitions noEff_1 :: Exp NoEffect () noEff_1 = return () noEff_2 :: Exp Effect () noEff_2 = return () When you use noEff in the program, the compiler chooses either noEff_1 or noEff_2 depending on the type required by the context. (GHC actually does that in some circumstances). Subtyping means defining a (partial) order among types T2 >= T1 and adding a subsumption rule to the type system e :: T1 T2 >= T1 ----------------- e :: T2 That is, if e has type T1 and T2 is at least as great, e can be given the type T2. Such a rule is very common in various object systems. Since we can't add new rules into the Haskell type system, we have to use a work-around, the explicit coercion. We introduce a function coerce :: T1 -> T2 (often an identity), which is a proof that it is really OK to use (e::T1) at the type T2. We have to explicitly write this coercion function:
hasEffect :: Exp Effect () hasEffect = do coerceEff noEff return ()
We are all familiar with this approach, explicitly writing 'return 1' to, say, return an integer result from a monadic function. Here, return is the explicit coercion, from 1::Int (the pure expression) to m Int (the potentially effectful expression). Other familiar example is newtype: newtype Speed = Speed{unSpeed :: Float} Then expressions (Speed 1.0) or (unSpeed x) / 10.0 etc. are all examples of explicit coercions (which are operationally identity). [Here were do want the coercions to be explicit, at least the Float->Speed coercion. The other could be implicit.] Haskell uses this approach for numeric literals. When we want to use an integer 1 where a rational number is required, we have to write fromInteger 1. Here fromInteger being the explicit coercion. Only we don't have to write 'fromInteger' because GHC inserts it implicitly. The latter example makes too points: explicit coercions are cumbersome to write and we'd rather had them out of sight. The second point is that the coercion is not a single function, but an overloaded function (e.g., return fromInteger). The coercions return and fromInteger are also not operationally identity, which actually do something at run-time. Let's go back to our example and change it to be more interesting, splitting Effect into Read and Write effects, with the order NoEffect < ReadEff < WriteEff. To witness the order, we define class Coerce t1 t2 where coerce :: Exp t1 a -> Exp t2 a instance Coerce NoEffect ReadEff where ... instance Coerce NoEffect WriteEff where ... instance Coerce ReadEffect WriteEff where ... so that we can define
noEff :: Exp NoEffect () noEff = return ()
and write (coerce noEff) if we want to use noEff in effectful situations. We observe that if we make Coerce reflexive, that is, add instance Coerce NoEffect NoEffect where coerce = id ... then we can write (coerce noEff) all the time. And if we do that, why not to fuse coerce into the definition of noEff:
noEff :: Coerce Noeff r => Exp r () noEff = coerce (return ())
We come the full circle to polymorphism -- although generally bounded polymorphism. (In noEff example above we can drop the Coerce constraint since Noeff can be coerced to any other effect. Not so for ReadEffect).
data Exp :: Eff -> * -> * where ReadAccount :: Exp NoEffect Int --ReadAccount has no effect Bind :: Effects m n r => Exp m a -> (a -> Exp n b) -> Exp r b ... hasEffect :: Exp Effect () hasEffect = ReadAccount >> (returnM () :: Exp Effect ())
This is working more or less, however I am obliged to put the type signature on the returnM (last line): why?
This is the infamous read-show problem. See for example http://book.realworldhaskell.org/read/using-typeclasses.html#typeclasses.wel...
eval :: Nomex r a -> State Game a eval a@ReadAccount = liftEval $ evalNoEffect a eval (WriteAccount a) = modify (\g -> g{account = a}) eval (SetVictory v) = modify (\g -> g{victory = v}) eval a@(Return _) = liftEval $ evalNoEffect a eval (Bind exp f) = eval exp >>= eval . f
This is a common pitfall. We should write
eval :: Nomex r a -> State Game a eval ReadAccount = liftEval $ evalNoEffect ReadAccount eval (Return x) = liftEval $ evalNoEffect (Return x) ...
It seems like a boilerplate: why do we have to write the same 'ReadAccount' on the left hand side and on the right-hand side (ditto for Return x). Can't we just share, like in the original code? The answer is no: The ReadAccount on the left hand side of the eval equation is different from ReadAccount on the right-hand side. They are spelled the same, but their types differ. On the left-hand-side, ReadAccount :: Nomex Effect (), but on the right-hand side, ReadAccount :: Nomex Effect (). This is a frequent problem with constants like [] which may have more than one type.