<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>