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?
I know you can replace the type signature of noEff by:

> noEff :: Exp r ()

But I don't find it so elegant...

I suppose you have to encode the semantic in the Bind of the Monad instance:

> data Exp :: Eff -> * -> * where
>   ...
>   Bind1        :: Exp NoEffect a -> (a -> Exp r b) -> Exp r b
>   Bind2        :: Exp Effect a -> (a -> Exp r b) -> Exp Effect b

> instance Monad (Exp r) where
>    return = Const
>    (a :: Exp NoEffect a) >>= f = a `Bind1` f
>    (a :: Exp Effect a)   >>= f = a `Bind2` f

But this doesn't work:
Couldn't match type `r' with 'NoEffect
      `r' is a rigid type variable

Thanks a lot for the help :) all this thread helped me a lot!!

Corentin


On Thu, Jan 30, 2014 at 8:53 PM, Corentin Dupont <corentin.dupont@gmail.com> wrote:


Oleg: Very interresting, thanks. I have some questions:
- What do you mean by "The type Cont Int a describes an impure computation, which may abort with an Int value, for example".
Aborting with an Int value is akin to exceptions?
- for me it's not clear when to choose an "applicative" or a "monadic" DSL? Betsides, what's the rational behind the name "let_" (never seen it before)?


Linsey, Jacques: Thanks for the pointer! I learned about data kinds.
I tried to apply your suggestions to add a phantom type parameter to Exp.
I came up to (I dropped the Free monad idea, which seems unrelated to the problem):


 
> data Eff = Effect | NoEffect

> -- first type parameter is used to track effects
> data Exp :: Eff -> * -> * where
>   ReadAccount  :: Exp r Int  --ReadAccount can be used in whatever monad (with or without effect)
>   WriteAccount :: Exp NoEffect Int -> Exp Effect ()  --WriteAccount takes an effect-less expression, and returns an effectfull expression
>   SetVictory   :: Exp NoEffect Bool -> Exp Effect ()  -- same for SetVictory
>   OnTimer      :: Exp Effect () -> Exp Effect () --OnTime can program whatever expression to be triggered every minutes, in particular effectful ones
>   Return       :: a -> Exp r a
>   Bind         :: Exp r a -> (a -> Exp r b) -> Exp r b

This is the (simplified) game state:


> data Game = Game { bankAccount :: Int,
>                    victory     :: Exp NoEffect Bool,
>                    timerEvent  :: Exp Effect ()}

> -- victory when account > 100
> victoryRule' :: Exp Effect ()

> victoryRule' = SetVictory $ do
>   m <- readAccount
>   --WriteAccount (return $ m + 1) --won't compile (good)

>   return (m > 100)

> --increase my bank account by 1 every minute
> myTimer :: Exp Effect ()
> myTimer = OnTimer $ do
>   m <- readAccount

>   writeAccount (return $ m + 1)


Do you have a better name suggestion for Eff? Other pointers where this idiom is realised??
Thanks!!
Corentin