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