
Hi Corentin,
Oleg's January 31 message has: `ReadAccount :: Exp r Int'. If you use that
version you can define that last `hasEffect :: Exp Effect ()'. Then bind
can just be:
Bind :: Exp m a -> (a -> Exp m b) -> Exp m b
And the `m' from a non-effectful thing (ReadAccount) will be set to Effect
when you bind it with an effectful computation. You can still have
operations that take arguments like `Exp NoEffect a', which will give you a
type error when you pass in a an argument tagged with Effect.
Adam
On Mon, Feb 3, 2014 at 6:44 AM, Corentin Dupont
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-Para...), 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
wrote: On Sun, Feb 2, 2014 at 2:42 PM, Corentin Dupont
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe