<div dir="ltr"><div style>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.</div><div><br></div><div>{-# LANGUAGE RankNTypes #-}</div>
<div>{-# LANGUAGE GeneralizedNewtypeDeriving #-}</div><div>module DSLEffects where</div><div><br></div><div>import Control.Monad.State</div><div>import Control.Monad.Reader</div><div><br></div><div>class Monad m => Nomex m where</div>
<div> readAccount :: m Int</div><div><br></div><div>class Nomex m => NomexEffect m where</div><div> writeAccount :: Int -> m ()</div><div> setVictory  :: (forall m. Nomex m => m Bool) -> m ()</div><div><br>
</div><div>data Game = Game { victory :: (forall m. Nomex m => m Bool)</div><div>Â Â Â Â Â Â Â Â Â , account :: Int</div><div>Â Â Â Â Â Â Â Â Â }</div><div><br></div><div>newtype Eval a = Eval { eval :: State Game a }</div>
<div>Â Â Â Â Â Â Â Â deriving Monad</div><div><br></div><div>instance Nomex Eval where</div><div>Â readAccount = Eval $ gets account</div><div><br></div><div>instance NomexEffect Eval where</div><div>Â writeAccount n = Eval . modify $ \game -> game { account = n }</div>
<div> setVictory  v = Eval . modify $ \game -> game { victory = v }</div><div><br></div><div>newtype EvalNoEffect a = EvalNoEffect { evalNoEffect :: Reader Game a }</div><div>            deriving Monad</div>
<div><br></div><div>instance Nomex EvalNoEffect where</div><div>Â readAccount = EvalNoEffect $ asks account</div><div><br></div><div>noEff :: Nomex m => m ()</div><div>noEff = return ()</div><div><br></div><div>hasEff :: NomexEffect m => m ()</div>
<div>hasEff = readAccount >>= writeAccount</div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Feb 6, 2014 at 12:47 PM, adam vogt <span dir="ltr"><<a href="mailto:vogt.adam@gmail.com" target="_blank">vogt.adam@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi Corentin,<br><br>You need change Effect to NoEffect to reuse the evalNoEffect:<br><br>> eval ReadAccount = liftEval $ evalNoEffect ReadAccount<br>
> eval (Return a)Â Â Â Â = liftEval $ evalNoEffect (Return a)<br>
<br>Or use a function like `unsafeCoerce :: Nomex Effect a -> Nomex NoEffect a`.<br><br>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:<br>
<br>> data Effects<br>>Â = HasBeenCombinedWithSomethingThatHasEffectsButICan'tBeSureItActuallyHasEffectsAllByItself<br>>Â Â | DefinitelyHasNoEffects<br>
<br><br>Regards,<br>Adam<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Feb 6, 2014 at 9:50 AM, Corentin Dupont <span dir="ltr"><<a href="mailto:corentin.dupont@gmail.com" target="_blank">corentin.dupont@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>Hi guys,<br></div>I'm still exploring some design space for DSLs, following our interesting discussion.<br>
<br></div>I'm trying to write the evaluator for the DSL (see below). <br></div>
For the general case, the evaluator looks like:<br><br><span style="font-family:courier new,monospace">eval :: Nomex r a -> State Game a </span><br><div><div><br></div><div>This eval function takes an expression (called Nomex), that can possibly have effects.<br>
</div><div>It returns a state monad, to allow you to modify the game state.<br><br></div><div>But for effectless instructions, it would be better to run the evaluator in the reader monad:<br><br><span style="font-family:courier new,monospace">evalNoEffect :: Nomex NoEffect a -> Reader Game a </span><br>
</div><div><br></div><div>So you can have additional guaranties that evaluating your expression will not have effects.<br></div><div><span style="font-family:courier new,monospace"><span style="font-family:arial,helvetica,sans-serif">I tried (see below), but it doesn't work for the moment: </span><br>
<br></span></div><div><span style="font-family:courier new,monospace"><br>> {-# LANGUAGE GADTs #-}<div><br>> {-# LANGUAGE KindSignatures, DataKinds, ScopedTypeVariables, <br></div><div>>Â Â MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}<br>
<br>> module DSLEffects where<br><br></div>> import Control.Monad.Error<br>> import Control.Monad.State<br>> import Control.Monad.Reader<br>> import Data.Typeable<br><br>This is the DSL:<br>Â Â Â <br>> data Effects = Effect | NoEffect<br>
<br>> data Nomex :: Effects -> * -> * where<br>>  ReadAccount :: Nomex r Int               --ReadAccount has no effect: it can be run in whatever monad<br>>  WriteAccount :: Int -> Nomex Effect () --WriteAccount has effect<br>
>  SetVictory  :: Nomex NoEffect Bool -> Nomex Effect () --SetVictory don't accept effectful computations<br>>  Bind        :: Nomex m a -> (a -> Nomex m b) -> Nomex m b<br>>  Return      :: a -> Nomex r a --wrapping a constant has no effect<br>
<br>> instance Monad (Nomex a) where<br>>Â Â return = Return<br>>Â Â (>>=) = Bind<br><br><br>> noEff :: Nomex NoEffect ()<br>> noEff = return ()<br><br>> hasEffect :: Nomex Effect ()<br>> hasEffect = do<br>
>   a <- ReadAccount<br>>   WriteAccount a<br><br>> data Game = Game { victory :: Nomex NoEffect Bool,<br>>                   account :: Int}<br><br><br>> eval :: Nomex r a -> State Game a <br>> eval a@ReadAccount   = liftEval $ evalNoEffect a<br>
> eval (WriteAccount a) = modify (\g -> g{account = a})<div><br>> eval (SetVictory v)Â Â = modify (\g -> g{victory = v})<br></div>> eval a@(Return _)Â Â Â Â = liftEval $ evalNoEffect a<br>> eval (Bind exp f)Â Â Â Â = eval exp >>= eval . f<br>
<br>> evalNoEffect :: Nomex NoEffect a -> Reader Game a<br>> evalNoEffect ReadAccount = asks account<br>> evalNoEffect (Return a)  = return a<br>> evalNoEffect (Bind exp f) = evalNoEffect exp >>= evalNoEffect . f<br>
<br>> liftEval :: Reader Game a -> State Game a<br>> liftEval r = get >>= return . runReader r <br></span><br><br></div><div>This is not compiling: <br><br></div><div>exceptEffect.lhs:60:15:<br>Â Â Â Couldn't match type 'NoEffect with 'Effect<br>
   Inaccessible code in<br>     a pattern with constructor<br>       WriteAccount :: Int -> Nomex 'Effect (),<br>     in an equation for `evalEffect'<br>   In the pattern: WriteAccount a<br>   In an equation for `evalEffect':<br>
       evalEffect (WriteAccount a) = modify (\ g -> g {account = a})<br><br></div><div>It seems that the type of effectless computations (NoEffect) leaks in the type of effectful ones (due to the pattern matching)...<br>
</div><div><br></div><div>Thanks,<br></div><div>Corentin<br><br></div></div></div><div><div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Feb 3, 2014 at 12:44 PM, Corentin Dupont <span dir="ltr"><<a href="mailto:corentin.dupont@gmail.com" target="_blank">corentin.dupont@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><div>I saw that to write liftQD you decontruct (unwrap) the type and reconstruct it. <br>
</div>I don't know if I can do that for my Exp (which is a full DSL)...<br><br></div>Anyway, there should be a way to encode the Effect/NoEffect semantic at type level...<br>
</div>Using Oleg's parametrized monad idea (<a href="http://hackage.haskell.org/package/monad-param-0.0.2/docs/Control-Monad-Parameterized.html" target="_blank">http://hackage.haskell.org/package/monad-param-0.0.2/docs/Control-Monad-Parameterized.html</a>), I tried:<br>
<br><span style="font-family:courier new,monospace">> {-# LANGUAGE KindSignatures, DataKinds, ScopedTypeVariables, GADTs<br>>Â Â MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}<br>
<br>> module DSLEffects where<br>> import Prelude hiding (return, (>>), (>>=))<br>> import Control.Monad.Parameterized</span><br><br>This data type will be promoted to kind level (thanks to DataKinds):<div>
<br>
<span style="font-family:courier new,monospace"><br>> data Eff = Effect | NoEffect</span><br><br></div>This class allows to specify the semantic on Effects (Effect + NoEffect = Effect):<br><span style="font-family:courier new,monospace"><br>
> class Effects (m :: Eff) (n::Eff) (r::Eff) | m n -> r<br>> instance Effects Effect n Effect<br>> instance Effects NoEffect n n</span><br><br>This is the DSL:<br><span style="font-family:courier new,monospace"><div>
<br>
> data Exp :: Eff -> * -> * where<br></div>>  ReadAccount :: Exp NoEffect Int     --ReadAccount has no effect<br>>  WriteAccount :: Int -> Exp Effect () --WriteAccount has effect<br>>  Const       :: a -> Exp r a<br>
>  Bind        :: Effects m n r => Exp m a -> (a -> Exp n b) -> Exp r b --Bind comes with a semantic on effects<br>>  Fmap        :: (a -> b) -> Exp m a -> Exp m b<br><br>> instance Functor (Exp r) where<br>
>Â Â fmap = Fmap<br><br>> instance Return (Exp r) where<br>>Â Â Â returnM = Const<br><br>> instance (Effects m n r) => Bind (Exp m) (Exp n) (Exp r) where<br>>Â Â Â (>>=) = Bind<br><br>> noEff :: Exp NoEffect ()<br>
> noEff = returnM ()<br><br>> hasEffect :: Exp Effect ()<br>> hasEffect = ReadAccount >> (returnM () :: Exp Effect ())</span><br><br></div>This is working more or less, however I am obliged to put the type signature on the returnM (last line): why?<br>
</div><span style="font-family:arial,helvetica,sans-serif">Furthermore, I cannot write</span><span style="font-family:courier new,monospace"><span style="font-family:arial,helvetica,sans-serif"> directly:</span><br></span><br>
<span style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> hasEffect :: Exp Effect ()<br></span>> hasEffect = ReadAccount</span><div><div><div><br><br></div><div>Do you have a better idea?<br>
<br></div></div></div></div><div><div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Feb 2, 2014 at 8:55 PM, Lindsey Kuper <span dir="ltr"><<a href="mailto:lindsey@composition.al" target="_blank">lindsey@composition.al</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>On Sun, Feb 2, 2014 at 2:42 PM, Corentin Dupont<br>
<<a href="mailto:corentin.dupont@gmail.com" target="_blank">corentin.dupont@gmail.com</a>> wrote:<br>
> you should be able to run an effectless monad in an effectful one.<br>
> How to encode this semantic?<br>
<br>
</div>In LVish we just have a `liftQD` operation that will let you lift a<br>
deterministic computation to a quasi-deterministic one (recall that<br>
deterministic computations can perform fewer effects):<br>
<br>
 liftQD :: Par Det s a -> Par QuasiDet s a<br>
<br>
So, analogously, you could have a `liftEff` and then write `liftEff<br>
noEff`. Â This is also a little bit ugly, but you may find you don't<br>
have to do it very often (we rarely use `liftQD`).<br>
<span><font color="#888888"><br>
Lindsey<br>
</font></span></blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div><br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>