[Haskell-cafe] manage effects in a DSL

[Corentin Dupont]

So finally, I think there are really 3 solutions to the problem of
representing the semantic of effects/no effects (effect-less instructions
can be run in effect-full context, but not the opposite).
We can encode this semantic at:
- value level
- type level
- typeclass level

At value level, the semantic is encoded by a DSL instruction 'NoEff' that
wraps an effect-less instruction into an effect-full one:
NoEff        :: Nomex NoEffect a -> Nomex Effect a
See
https://github.com/cdupont/Nomyx-design/blob/master/TypeParamEffect-Concrete.hs

At type level, the semantic is encoded by using a polymorphic type
parameter that can take two concrete type, 'Effect' or 'NoEffect':
ReadAccount  :: Nomex r Int
See
https://github.com/cdupont/Nomyx-design/blob/master/TypeParamEffect-Polymorphic.hs

At typeclass level, the semantic is encoded by the hierarchy of classes:
class Nomex m => NomexEffect m where...
See https://github.com/cdupont/Nomyx-design/blob/master/TypeClassEffect.hs

Now I have to choose one :))




On Mon, Feb 24, 2014 at 12:18 PM, Corentin Dupont <corentin.dupont at gmail.com
> wrote:

> 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/20140225/a6b59628/attachment.html>