[Haskell-cafe] manage effects in a DSL

[oleg at okmij.org]

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.wellknown.read

> eval :: Nomex r a -> State Game a
> eval a at 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.