[Haskell-cafe] manage effects in a DSL

Dominique Devriese dominique.devriese at cs.kuleuven.be
Mon Feb 10 07:46:58 UTC 2014


Fully agree with Jake.  Corentin's effect system is rather simple so that
indexed monads are overkill here and Jake's solution is simpler.

I just want to point out that the key component of Jake's proposed
solution is not
really type classes, but rather an (underappreciated) pattern that I
call /effect polymorphism/: monadic computations that are polymorphic
over the monad in which they produce effects:

> noEff :: Nomex m => m ()
> noEff = return ()
>
> hasEff :: NomexEffect m => m ()
> hasEff = readAccount >>= writeAccount

I would say that type classes are not the key here, since you could
use the same pattern, but replace type classes with dictionaries and
get the same benefits, although with a bit more administration to be
done by the user.

Such computations have many useful properties, thanks to the
parametricity of the polymorphic quantification.   This has been well
explained by Voigtlaender:
http://wwwtcs.inf.tu-dresden.de/~voigt/icfp09.pdf.  Effect
polymorphism has also been used by Oliveira, Schrijvers and Cook in a
model of (among other features) aspect composition:
http://users.ugent.be/~tschrijv/Research/papers/jfp_mri.pdf.

Note by the way that Jake's proposal is still compatible with the
previously suggested solutions based on indexed monads, since you can
write:

instance Nomex (Exp r) where
  readAccount = ReadAccount

instance NomexEffect (Exp Effect) where
  ...

Regards,
Dominique

2014-02-06 21:35 GMT+01:00 Jake McArthur <jake.mcarthur at gmail.com>:
> I still think GADTs are a bit too much for this problem. Just using type
> classes provides all the safety you need and even avoids the need for that
> liftEval function.
>
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE GeneralizedNewtypeDeriving #-}
> module DSLEffects where
>
> import Control.Monad.State
> import Control.Monad.Reader
>
> class Monad m => Nomex m where
>   readAccount :: m Int
>
> class Nomex m => NomexEffect m where
>   writeAccount :: Int -> m ()
>   setVictory   :: (forall m. Nomex m => m Bool) -> m ()
>
> data Game = Game { victory :: (forall m. Nomex m => m Bool)
>                  , account :: Int
>                  }
>
> newtype Eval a = Eval { eval :: State Game a }
>                deriving Monad
>
> instance Nomex Eval where
>   readAccount = Eval $ gets account
>
> instance NomexEffect Eval where
>   writeAccount n = Eval . modify $ \game -> game { account = n }
>   setVictory   v = Eval . modify $ \game -> game { victory = v }
>
> newtype EvalNoEffect a = EvalNoEffect { evalNoEffect :: Reader Game a }
>                        deriving Monad
>
> instance Nomex EvalNoEffect where
>   readAccount = EvalNoEffect $ asks account
>
>
>
>
> On Thu, Feb 6, 2014 at 12:47 PM, adam vogt <vogt.adam at gmail.com> wrote:
>>
>> Hi Corentin,
>>
>> You need change Effect to NoEffect to reuse the evalNoEffect:
>>
>> > eval ReadAccount = liftEval $ evalNoEffect ReadAccount
>> > eval (Return a)     = liftEval $ evalNoEffect (Return a)
>>
>> Or use a function like `unsafeCoerce :: Nomex Effect a -> Nomex NoEffect
>> a`.
>>
>> If you rename the types that tag effects to something that describes
>> exactly what the tags actually represent, maybe the above definition will be
>> more satisfying:
>>
>> > data Effects
>> >  =
>> > HasBeenCombinedWithSomethingThatHasEffectsButICan'tBeSureItActuallyHasEffectsAllByItself
>> >   | DefinitelyHasNoEffects
>>
>>
>> Regards,
>> Adam
>>
>>
>> On Thu, Feb 6, 2014 at 9:50 AM, Corentin Dupont
>> <corentin.dupont at gmail.com> wrote:
>>>
>>> Hi guys,
>>> I'm still exploring some design space for DSLs, following our interesting
>>> discussion.
>>>
>>> I'm trying to write the evaluator for the DSL (see below).
>>> For the general case, the evaluator looks like:
>>>
>>> eval :: Nomex r a -> State Game a
>>>
>>> This eval function takes an expression (called Nomex), that can possibly
>>> have effects.
>>> It returns a state monad, to allow you to modify the game state.
>>>
>>> But for effectless instructions, it would be better to run the evaluator
>>> in the reader monad:
>>>
>>> evalNoEffect :: Nomex NoEffect a -> Reader Game a
>>>
>>> So you can have additional guaranties that evaluating your expression
>>> will not have effects.
>>> I tried (see below), but it doesn't work for the moment:
>>>
>>>
>>> > {-# LANGUAGE GADTs #-}
>>>
>>> > {-# LANGUAGE KindSignatures, DataKinds, ScopedTypeVariables,
>>> >   MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
>>> > UndecidableInstances #-}
>>>
>>> > module DSLEffects where
>>>
>>> > import Control.Monad.Error
>>> > import Control.Monad.State
>>> > import Control.Monad.Reader
>>> > import Data.Typeable
>>>
>>> This is the DSL:
>>>
>>> > data Effects = Effect | NoEffect
>>>
>>> > data Nomex :: Effects -> * -> * where
>>> >   ReadAccount  :: Nomex r Int                --ReadAccount has no
>>> > effect: it can be run in whatever monad
>>> >   WriteAccount :: Int -> Nomex Effect ()  --WriteAccount has effect
>>> >   SetVictory   :: Nomex NoEffect Bool -> Nomex Effect () --SetVictory
>>> > don't accept effectful computations
>>> >   Bind         :: Nomex m a -> (a -> Nomex m b) -> Nomex m b
>>> >   Return       :: a -> Nomex r a  --wrapping a constant has no effect
>>>
>>> > instance Monad (Nomex a) where
>>> >   return = Return
>>> >   (>>=) = Bind
>>>
>>>
>>> > noEff :: Nomex NoEffect ()
>>> > noEff = return ()
>>>
>>> > hasEffect :: Nomex Effect ()
>>> > hasEffect = do
>>> >    a <- ReadAccount
>>> >    WriteAccount a
>>>
>>> > data Game = Game { victory :: Nomex NoEffect Bool,
>>> >                    account :: Int}
>>>
>>>
>>> > 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
>>>
>>> > evalNoEffect :: Nomex NoEffect a -> Reader Game a
>>> > evalNoEffect ReadAccount  = asks account
>>> > evalNoEffect (Return a)   = return a
>>> > evalNoEffect (Bind exp f) = evalNoEffect exp >>= evalNoEffect . f
>>>
>>> > liftEval :: Reader Game a -> State Game a
>>> > liftEval r = get >>= return . runReader r
>>>
>>>
>>> This is not compiling:
>>>
>>> exceptEffect.lhs:60:15:
>>>     Couldn't match type 'NoEffect with 'Effect
>>>     Inaccessible code in
>>>       a pattern with constructor
>>>         WriteAccount :: Int -> Nomex 'Effect (),
>>>       in an equation for `evalEffect'
>>>     In the pattern: WriteAccount a
>>>     In an equation for `evalEffect':
>>>         evalEffect (WriteAccount a) = modify (\ g -> g {account = a})
>>>
>>> It seems that the type of effectless computations (NoEffect) leaks in the
>>> type of effectful ones (due to the pattern matching)...
>>>
>>> Thanks,
>>> Corentin
>>>
>>>
>>>
>>> On Mon, Feb 3, 2014 at 12:44 PM, Corentin Dupont
>>> <corentin.dupont at gmail.com> wrote:
>>>>
>>>> I saw that to write liftQD you decontruct (unwrap) the type and
>>>> reconstruct it.
>>>> I don't know if I can do that for my Exp (which is a full DSL)...
>>>>
>>>> Anyway, there should be a way to encode the Effect/NoEffect semantic at
>>>> type level...
>>>> Using Oleg's parametrized monad idea
>>>> (http://hackage.haskell.org/package/monad-param-0.0.2/docs/Control-Monad-Parameterized.html),
>>>> I tried:
>>>>
>>>> > {-# LANGUAGE KindSignatures, DataKinds, ScopedTypeVariables, GADTs
>>>> >   MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances,
>>>> > UndecidableInstances #-}
>>>>
>>>> > module DSLEffects where
>>>> > import Prelude hiding (return, (>>), (>>=))
>>>> > import Control.Monad.Parameterized
>>>>
>>>> This data type will be promoted to kind level (thanks to DataKinds):
>>>>
>>>>
>>>> > data Eff = Effect | NoEffect
>>>>
>>>> This class allows to specify the semantic on Effects (Effect + NoEffect
>>>> = Effect):
>>>>
>>>> > class Effects (m :: Eff) (n::Eff) (r::Eff) | m n -> r
>>>> > instance Effects Effect n Effect
>>>> > instance Effects NoEffect n n
>>>>
>>>> This is the DSL:
>>>>
>>>> > data Exp :: Eff -> * -> * where
>>>> >   ReadAccount  :: Exp NoEffect Int      --ReadAccount has no effect
>>>> >   WriteAccount :: Int -> Exp Effect ()  --WriteAccount has effect
>>>> >   Const        :: a -> Exp r a
>>>> >   Bind         :: Effects m n r => Exp m a -> (a -> Exp n b) -> Exp r
>>>> > b --Bind comes with a semantic on effects
>>>> >   Fmap         :: (a -> b) -> Exp m a -> Exp m b
>>>>
>>>> > instance Functor (Exp r) where
>>>> >   fmap = Fmap
>>>>
>>>> > instance Return (Exp r) where
>>>> >    returnM = Const
>>>>
>>>> > instance (Effects m n r) => Bind (Exp m) (Exp n) (Exp r) where
>>>> >    (>>=) = Bind
>>>>
>>>> > noEff :: Exp NoEffect ()
>>>> > noEff = returnM ()
>>>>
>>>> > 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?
>>>> Furthermore, I cannot write directly:
>>>>
>>>> > hasEffect :: Exp Effect ()
>>>> > hasEffect = ReadAccount
>>>>
>>>>
>>>> Do you have a better idea?
>>>>
>>>>
>>>>
>>>> On Sun, Feb 2, 2014 at 8:55 PM, Lindsey Kuper <lindsey at composition.al>
>>>> wrote:
>>>>>
>>>>> On Sun, Feb 2, 2014 at 2:42 PM, Corentin Dupont
>>>>> <corentin.dupont at gmail.com> wrote:
>>>>> > you should be able to run an effectless monad in an effectful one.
>>>>> > How to encode this semantic?
>>>>>
>>>>> In LVish we just have a `liftQD` operation that will let you lift a
>>>>> deterministic computation to a quasi-deterministic one (recall that
>>>>> deterministic computations can perform fewer effects):
>>>>>
>>>>>   liftQD :: Par Det s a -> Par QuasiDet s a
>>>>>
>>>>> So, analogously, you could have a `liftEff` and then write `liftEff
>>>>> noEff`.  This is also a little bit ugly, but you may find you don't
>>>>> have to do it very often (we rarely use `liftQD`).
>>>>>
>>>>> Lindsey
>>>>
>>>>
>>>
>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>


More information about the Haskell-Cafe mailing list