[Haskell-cafe] manage effects in a DSL

[Corentin Dupont]

Thanks a lot Oleg. I finally had time to fully read and understand your
comments :)

>From all the comments I got, I put everything together in two blog posts:
http://www.corentindupont.info/blog/posts/2014-02-12-Effect-Class.html
Thanks!


On Thu, Feb 13, 2014 at 8:28 AM, <oleg at okmij.org> wrote:

>
> 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.
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140224/2eafe1b6/attachment.html>