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 <corentin.dupont@gmail.com> wrote:

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-Parameterized.html), 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 <lindsey@composition.al> wrote:

On Sun, Feb 2, 2014 at 2:42 PM, Corentin Dupont
<corentin.dupont@gmail.com> 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