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

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

Hi guys, I'm still exploring some design space for DSLs, following our interesting discussion. I'm trying to write the evaluator for the DSL (see below). For the general case, the evaluator looks like: eval :: Nomex r a -> State Game a This eval function takes an expression (called Nomex), that can possibly have effects. It returns a state monad, to allow you to modify the game state. But for effectless instructions, it would be better to run the evaluator in the reader monad: evalNoEffect :: Nomex NoEffect a -> Reader Game a So you can have additional guaranties that evaluating your expression will not have effects. I tried (see below), but it doesn't work for the moment:

{-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures, DataKinds, ScopedTypeVariables, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}

module DSLEffects where

import Control.Monad.Error import Control.Monad.State import Control.Monad.Reader import Data.Typeable

This is the DSL:

data Effects = Effect | NoEffect

data Nomex :: Effects -> * -> * where ReadAccount :: Nomex r Int --ReadAccount has no effect: it can be run in whatever monad WriteAccount :: Int -> Nomex Effect () --WriteAccount has effect SetVictory :: Nomex NoEffect Bool -> Nomex Effect () --SetVictory don't accept effectful computations Bind :: Nomex m a -> (a -> Nomex m b) -> Nomex m b Return :: a -> Nomex r a --wrapping a constant has no effect

instance Monad (Nomex a) where return = Return (>>=) = Bind

noEff :: Nomex NoEffect () noEff = return ()

hasEffect :: Nomex Effect () hasEffect = do a <- ReadAccount WriteAccount a

data Game = Game { victory :: Nomex NoEffect Bool, account :: Int}

eval :: Nomex r a -> State Game a eval a@ReadAccount = liftEval $ evalNoEffect a eval (WriteAccount a) = modify (\g -> g{account = a}) eval (SetVictory v) = modify (\g -> g{victory = v}) eval a@(Return _) = liftEval $ evalNoEffect a eval (Bind exp f) = eval exp >>= eval . f

evalNoEffect :: Nomex NoEffect a -> Reader Game a evalNoEffect ReadAccount = asks account evalNoEffect (Return a) = return a evalNoEffect (Bind exp f) = evalNoEffect exp >>= evalNoEffect . f

liftEval :: Reader Game a -> State Game a liftEval r = get >>= return . runReader r

This is not compiling: exceptEffect.lhs:60:15: Couldn't match type 'NoEffect with 'Effect Inaccessible code in a pattern with constructor WriteAccount :: Int -> Nomex 'Effect (), in an equation for `evalEffect' In the pattern: WriteAccount a In an equation for `evalEffect': evalEffect (WriteAccount a) = modify (\ g -> g {account = a}) It seems that the type of effectless computations (NoEffect) leaks in the type of effectful ones (due to the pattern matching)... Thanks, Corentin On Mon, Feb 3, 2014 at 12:44 PM, Corentin Dupont 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-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

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. {-# LANGUAGE RankNTypes #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} module DSLEffects where import Control.Monad.State import Control.Monad.Reader class Monad m => Nomex m where readAccount :: m Int class Nomex m => NomexEffect m where writeAccount :: Int -> m () setVictory :: (forall m. Nomex m => m Bool) -> m () data Game = Game { victory :: (forall m. Nomex m => m Bool) , account :: Int } newtype Eval a = Eval { eval :: State Game a } deriving Monad instance Nomex Eval where readAccount = Eval $ gets account instance NomexEffect Eval where writeAccount n = Eval . modify $ \game -> game { account = n } setVictory v = Eval . modify $ \game -> game { victory = v } newtype EvalNoEffect a = EvalNoEffect { evalNoEffect :: Reader Game a } deriving Monad instance Nomex EvalNoEffect where readAccount = EvalNoEffect $ asks account noEff :: Nomex m => m () noEff = return () hasEff :: NomexEffect m => m () hasEff = readAccount >>= writeAccount On Thu, Feb 6, 2014 at 12:47 PM, adam vogt wrote:

Hi Corentin,

You need change Effect to NoEffect to reuse the evalNoEffect:

...

eval ReadAccount = liftEval $ evalNoEffect ReadAccount eval (Return a) = liftEval $ evalNoEffect (Return a)

Or use a function like `unsafeCoerce :: Nomex Effect a -> Nomex NoEffect a`.

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:

...

data Effects = HasBeenCombinedWithSomethingThatHasEffectsButICan'tBeSureItActuallyHasEffectsAllByItself | DefinitelyHasNoEffects

Regards, Adam

On Thu, Feb 6, 2014 at 9:50 AM, Corentin Dupont

...

wrote:

...

Hi guys, I'm still exploring some design space for DSLs, following our interesting discussion.

I'm trying to write the evaluator for the DSL (see below). For the general case, the evaluator looks like:

eval :: Nomex r a -> State Game a

This eval function takes an expression (called Nomex), that can possibly have effects. It returns a state monad, to allow you to modify the game state.

But for effectless instructions, it would be better to run the evaluator in the reader monad:

evalNoEffect :: Nomex NoEffect a -> Reader Game a

So you can have additional guaranties that evaluating your expression will not have effects. I tried (see below), but it doesn't work for the moment:

...

{-# LANGUAGE GADTs #-}

...

{-# LANGUAGE KindSignatures, DataKinds, ScopedTypeVariables, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}

...

module DSLEffects where

...

import Control.Monad.Error import Control.Monad.State import Control.Monad.Reader import Data.Typeable

This is the DSL:

...

data Effects = Effect | NoEffect

...

data Nomex :: Effects -> * -> * where ReadAccount :: Nomex r Int --ReadAccount has no effect: it can be run in whatever monad WriteAccount :: Int -> Nomex Effect () --WriteAccount has effect SetVictory :: Nomex NoEffect Bool -> Nomex Effect () --SetVictory don't accept effectful computations Bind :: Nomex m a -> (a -> Nomex m b) -> Nomex m b Return :: a -> Nomex r a --wrapping a constant has no effect

...

instance Monad (Nomex a) where return = Return (>>=) = Bind

...

noEff :: Nomex NoEffect () noEff = return ()

...

hasEffect :: Nomex Effect () hasEffect = do a <- ReadAccount WriteAccount a

...

data Game = Game { victory :: Nomex NoEffect Bool, account :: Int}

...

eval :: Nomex r a -> State Game a eval a@ReadAccount = liftEval $ evalNoEffect a eval (WriteAccount a) = modify (\g -> g{account = a})

...

eval (SetVictory v) = modify (\g -> g{victory = v}) eval a@(Return _) = liftEval $ evalNoEffect a eval (Bind exp f) = eval exp >>= eval . f

...

evalNoEffect :: Nomex NoEffect a -> Reader Game a evalNoEffect ReadAccount = asks account evalNoEffect (Return a) = return a evalNoEffect (Bind exp f) = evalNoEffect exp >>= evalNoEffect . f

...

liftEval :: Reader Game a -> State Game a liftEval r = get >>= return . runReader r

This is not compiling:

exceptEffect.lhs:60:15: Couldn't match type 'NoEffect with 'Effect Inaccessible code in a pattern with constructor WriteAccount :: Int -> Nomex 'Effect (), in an equation for `evalEffect' In the pattern: WriteAccount a In an equation for `evalEffect': evalEffect (WriteAccount a) = modify (\ g -> g {account = a})

It seems that the type of effectless computations (NoEffect) leaks in the type of effectful ones (due to the pattern matching)...

Thanks, Corentin

On Mon, Feb 3, 2014 at 12:44 PM, 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-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

That is really interesting. In fact, I didn't have the time to experiment with it, but I definitely want to (have to find some spare time!). I must say I am less used to type classes. At first, my concern with the technique was that two things that belong together, "ReadAccount" and "WriteAccount", are separated. I was also confused that the evaluator is wrapped in a newtype, and that it is an instance of Nomex. Beside, I suppose it is possible to factorize EvalNoEffect with Eval? Maybe using liftEval anyway... On Mon, Feb 10, 2014 at 8:46 AM, Dominique Devriese < dominique.devriese@cs.kuleuven.be> wrote:

Fully agree with Jake. Corentin's effect system is rather simple so that indexed monads are overkill here and Jake's solution is simpler.

I just want to point out that the key component of Jake's proposed solution is not really type classes, but rather an (underappreciated) pattern that I call /effect polymorphism/: monadic computations that are polymorphic over the monad in which they produce effects:

...

noEff :: Nomex m => m () noEff = return ()

hasEff :: NomexEffect m => m () hasEff = readAccount >>= writeAccount

I would say that type classes are not the key here, since you could use the same pattern, but replace type classes with dictionaries and get the same benefits, although with a bit more administration to be done by the user.

Such computations have many useful properties, thanks to the parametricity of the polymorphic quantification. This has been well explained by Voigtlaender: http://wwwtcs.inf.tu-dresden.de/~voigt/icfp09.pdf. Effect polymorphism has also been used by Oliveira, Schrijvers and Cook in a model of (among other features) aspect composition: http://users.ugent.be/~tschrijv/Research/papers/jfp_mri.pdf.

Note by the way that Jake's proposal is still compatible with the previously suggested solutions based on indexed monads, since you can write:

instance Nomex (Exp r) where readAccount = ReadAccount

instance NomexEffect (Exp Effect) where ...

Regards, Dominique

...

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

...

liftEval function.

{-# LANGUAGE RankNTypes #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} module DSLEffects where

import Control.Monad.State import Control.Monad.Reader

class Monad m => Nomex m where readAccount :: m Int

class Nomex m => NomexEffect m where writeAccount :: Int -> m () setVictory :: (forall m. Nomex m => m Bool) -> m ()

data Game = Game { victory :: (forall m. Nomex m => m Bool) , account :: Int }

newtype Eval a = Eval { eval :: State Game a } deriving Monad

instance Nomex Eval where readAccount = Eval $ gets account

instance NomexEffect Eval where writeAccount n = Eval . modify $ \game -> game { account = n } setVictory v = Eval . modify $ \game -> game { victory = v }

newtype EvalNoEffect a = EvalNoEffect { evalNoEffect :: Reader Game a } deriving Monad

instance Nomex EvalNoEffect where readAccount = EvalNoEffect $ asks account

On Thu, Feb 6, 2014 at 12:47 PM, adam vogt wrote:

...

Hi Corentin,

You need change Effect to NoEffect to reuse the evalNoEffect:

...

eval ReadAccount = liftEval $ evalNoEffect ReadAccount eval (Return a) = liftEval $ evalNoEffect (Return a)

Or use a function like `unsafeCoerce :: Nomex Effect a -> Nomex NoEffect a`.

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:

...

data Effects =

HasBeenCombinedWithSomethingThatHasEffectsButICan'tBeSureItActuallyHasEffectsAllByItself

...

| DefinitelyHasNoEffects

Regards, Adam

On Thu, Feb 6, 2014 at 9:50 AM, Corentin Dupont wrote:

...

Hi guys, I'm still exploring some design space for DSLs, following our

interesting

...

discussion.

I'm trying to write the evaluator for the DSL (see below). For the general case, the evaluator looks like:

eval :: Nomex r a -> State Game a

This eval function takes an expression (called Nomex), that can

...

...

...

have effects. It returns a state monad, to allow you to modify the game state.

But for effectless instructions, it would be better to run the evaluator in the reader monad:

evalNoEffect :: Nomex NoEffect a -> Reader Game a

So you can have additional guaranties that evaluating your expression will not have effects. I tried (see below), but it doesn't work for the moment:

...

{-# LANGUAGE GADTs #-}

...

{-# LANGUAGE KindSignatures, DataKinds, ScopedTypeVariables, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}

...

module DSLEffects where

...

import Control.Monad.Error import Control.Monad.State import Control.Monad.Reader import Data.Typeable

This is the DSL:

...

data Effects = Effect | NoEffect

...

data Nomex :: Effects -> * -> * where ReadAccount :: Nomex r Int --ReadAccount has no effect: it can be run in whatever monad WriteAccount :: Int -> Nomex Effect () --WriteAccount has effect SetVictory :: Nomex NoEffect Bool -> Nomex Effect () --SetVictory don't accept effectful computations Bind :: Nomex m a -> (a -> Nomex m b) -> Nomex m b Return :: a -> Nomex r a --wrapping a constant has no effect

...

instance Monad (Nomex a) where return = Return (>>=) = Bind

...

noEff :: Nomex NoEffect () noEff = return ()

...

hasEffect :: Nomex Effect () hasEffect = do a <- ReadAccount WriteAccount a

...

data Game = Game { victory :: Nomex NoEffect Bool, account :: Int}

...

eval :: Nomex r a -> State Game a eval a@ReadAccount = liftEval $ evalNoEffect a eval (WriteAccount a) = modify (\g -> g{account = a})

...

eval (SetVictory v) = modify (\g -> g{victory = v}) eval a@(Return _) = liftEval $ evalNoEffect a eval (Bind exp f) = eval exp >>= eval . f

...

evalNoEffect :: Nomex NoEffect a -> Reader Game a evalNoEffect ReadAccount = asks account evalNoEffect (Return a) = return a evalNoEffect (Bind exp f) = evalNoEffect exp >>= evalNoEffect . f

...

liftEval :: Reader Game a -> State Game a liftEval r = get >>= return . runReader r

This is not compiling:

exceptEffect.lhs:60:15: Couldn't match type 'NoEffect with 'Effect Inaccessible code in a pattern with constructor WriteAccount :: Int -> Nomex 'Effect (), in an equation for `evalEffect' In the pattern: WriteAccount a In an equation for `evalEffect': evalEffect (WriteAccount a) = modify (\ g -> g {account = a})

It seems that the type of effectless computations (NoEffect) leaks in

2014-02-06 21:35 GMT+01:00 Jake McArthur : that possibly the

...

...

...

type of effectful ones (due to the pattern matching)...

Thanks, Corentin

On Mon, Feb 3, 2014 at 12:44 PM, Corentin Dupont 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-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

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Mon, Feb 10, 2014 at 5:33 AM, Dominique Devriese < dominique.devriese@cs.kuleuven.be> wrote:

Local instances were already considered by Wadler when he proposed type classes, but they are problematic to combine with type inference

Local instances have a bigger problem: you can use them to trivially violate invariants. Consider a local replacement for Ord on a Data.Map. They're not going to happen. -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

Hi Dominique, On Mon, Feb 10, 2014 at 04:55:52PM +0100, Dominique Devriese wrote:

Hm. Interesting point, I guess this is the same problem as the whole orphan instances debate... I didn't think of the connection to that problem. Still, I'm convinced there are situations where local instances are *exactly* what we need, so there must be some way to avoid this problem...

If a type class has a clear semantical meaning, what should then be the point of having multiple instances for the same data type? A clear semantical meaning contradicts multiple instances, they would only make reasoning about your code harder. The few use cases where it might be nice to be able to define a new instance aren't IMHO worth the drawbacks. You would just open Haskell for Ruby like monkey patching. Greetings, Daniel

On Mon, Feb 10, 2014 at 11:26 AM, Dominique Devriese < dominique.devriese@cs.kuleuven.be> wrote:

I disagree. Just think about the Ord type class. A decidable order relation for a type is definitely something I would consider a clear semantical meaning, but different sensible instances can be defined for many types... The same thing goes for Eq or Monoid or MonadState or...

Sure... but now you have to make sure everything agrees about it. The way you do this in Haskell is to give your custom instance a distinct type to go with it. (Now go look at the Sum and Product monoids). -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

Am 10.02.2014 um 17:26 schrieb Dominique Devriese :

I disagree. Just think about the Ord type class. A decidable order relation for a type is definitely something I would consider a clear semantical meaning ...

Why shouldn't be the kind of ordering part of the semantical meaning of Ord? Otherwise what could you then say about the result of the 'sort' function? sort :: Ord a => [a] -> [a] My gut feeling is, that if the effective range of the active instance is too narrow, then it's not very useful, but if you widen it, then you're getting all of the possible drawbacks. Greetings, Daniel

Roman, 2014-02-10 18:22 GMT+01:00 Roman Cheplyaka :

* Daniel Trstenjak [2014-02-10 17:10:01+0100]

...

On Mon, Feb 10, 2014 at 04:55:52PM +0100, Dominique Devriese wrote:

...

Hm. Interesting point, I guess this is the same problem as the whole orphan instances debate... I didn't think of the connection to that problem. Still, I'm convinced there are situations where local instances are *exactly* what we need, so there must be some way to avoid this problem...

If a type class has a clear semantical meaning, what should then be the point of having multiple instances for the same data type?

A clear semantical meaning contradicts multiple instances, they would only make reasoning about your code harder.

The few use cases where it might be nice to be able to define a new instance aren't IMHO worth the drawbacks.

You would just open Haskell for Ruby like monkey patching.

How about a compromise. We already have a way to introduce fresh type names: using existential types. They look like good candidates for local instances (by definition, they can't have global instances, because the names themselves are necessarily local). Of course, you can define an instance only once, as for usual types.

This would cover the case when "dynamic" instances are needed without compromising soundness. Example:

data IsoInt = forall a . IsoInt (Int -> a) (a -> Int)

foo modulus = case IsoInt id id of IsoInt (fromInt :: Int -> a) toInt -> let eqMod x1 x2 = (toInt x1 - toInt x2) `mod` modulus == 0

-- note: a is rigid here instance Eq a where (==) = eqMod in ...

Just a note that your proposal seems very related to what Kiselyov and Shan propose in their paper on "Implicit Configurations" (http://dl.acm.org/citation.cfm?id=1017481). Anyway, I still think that there are cases where I want to say that I want to use "real" local instances. Another interesting example by the way is instancing MonadState for IO. Consider how every IORef a can be used to build a MonadState a instance for IO: data MonadStateD a m = MonadStateD { putM :: a -> m (), getM :: m a } ioRefStateD :: IORef a -> MonadStateD a IO ioRefStateD ref = MonadStateD (writeIORef ref) (readIORef ref) I have the feeling that Brandon's argument (that multiple instances cannot be permitted because, for example, Data.Map should only be used with a single Ord instance) in some way comes down to solving a lack for an ML-like module system by imposing an otherwise artificial restriction on type classes: to enforce that a type class instance is unique within a module parameterised by it, we simply require that the instance be globally unique... That being said, Brendan is clearly right that we can't just drop a guarantee that is widely relied upon. Regards, Dominique

Hi guys, so I tried to implement fully the proposition (see below). It works well. However I find it a bit redundant. Can we reduce the repetitions? Perhaps I didn't understand how to write the evaluation... {-# LANGUAGE RankNTypes #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} module Main where import Control.Monad.State import Control.Monad.Reader class Monad m => Nomex m where readAccount :: m Int class Nomex m => NomexEffect m where writeAccount :: Int -> m () setVictory :: (forall n. Nomex n => n Bool) -> m () data Exp a where ReadAccount :: Exp Int WriteAccount :: Int -> Exp () SetVictory :: (forall m. Nomex m => m Bool) -> Exp () Bind :: Exp a -> (a -> Exp b) -> Exp b Return :: a -> Exp a instance Monad Exp where return = Return (>>=) = Bind instance Nomex Exp where readAccount = ReadAccount instance NomexEffect Exp where writeAccount = WriteAccount setVictory = SetVictory data Game = Game { victory :: (forall m. Nomex m => m Bool) , account :: Int } instance Nomex (State Game) where readAccount = gets account instance NomexEffect (State Game) where writeAccount n = modify $ \game -> game { account = n } setVictory v = modify $ \game -> game { victory = v } instance Nomex (Reader Game) where readAccount = asks account evaluate :: Exp a -> State Game a evaluate (WriteAccount i) = writeAccount i evaluate ReadAccount = readAccount evaluate (SetVictory v) = setVictory v evaluate (Return a) = return a evaluate (Bind a f) = (evaluate a) >>= evaluate . f evalNoEff :: Exp a -> Reader Game a evalNoEff ReadAccount = readAccount evalNoEff (Return a) = return a evalNoEff (Bind a f) = (evalNoEff a) >>= evalNoEff . f isVictory :: Game -> Bool isVictory g = runReader (evalNoEff (victory g)) g incrAccount :: NomexEffect m => m () incrAccount = readAccount >>= writeAccount . (+101) winOnBigMoney :: NomexEffect m => m () winOnBigMoney = setVictory $ do i <- readAccount --writeAccount 100 return (i > 100) play = do winOnBigMoney incrAccount initGame = Game (return False) 0 main = do let g = execState (evaluate jeu) initGame putStrLn $ show $ isVictory g On Mon, Feb 10, 2014 at 11:33 AM, Dominique Devriese < dominique.devriese@cs.kuleuven.be> wrote:

Corentin,

2014-02-10 10:48 GMT+01:00 Corentin Dupont :

...

That is really interesting. In fact, I didn't have the time to experiment with it, but I definitely want to (have to find some spare time!). I must say I am less used to type classes. At first, my concern with the technique was that two things that belong together, "ReadAccount" and "WriteAccount", are separated.

Yes, this separation of ReadAccount and WriteAccount into Nomex vs NomexEffect is how the two parts (read-only vs read-write) of the DSL are distinguished in this approach..

...

I was also confused that the evaluator is wrapped in a newtype, and that it is an instance of Nomex.

That is non-essential. You can also use

instance Nomex (State Game) where

but it's just cleaner with a newtype...

...

Beside, I suppose it is possible to factorize EvalNoEffect with Eval? Maybe using liftEval anyway...

If I understand correctly, you're asking about how to remove the duplication between EvalNoEffect and Eval?

This is a very good question. My answer is basically that Haskell is missing some type-class-related features to allow for the perfect solution, specifically a form of local instances.

The long story is that instead of the above instances of Nomex and NomexEffect for Eval and EvalNoEffect separately, we would like to be able to write the following instances:

instance MonadReader Game m => Nomex m where readAccount = asks account

instance (MonadReader Game m, MonadState Game m) => NomexEffect m where writeAccount n = modify $ \game -> game { account = n } setVictory v = modify $ \game -> game { victory = v }

and then we can declare newtype Eval a = Eval { eval :: State Game a } deriving (Monad, MonadState Game, MonadReader Game)

newtype EvalNoEffect a = EvalNoEffect { evalNoEffect :: Reader Game a } deriving (Monad, MonadReader Game)

and reuse the single implementation of Nomex for both Eval and EvalNoEffect. However, there are various problems with this solution:

* the instances are not permitted without UndecidableInstances (which I recommend against), * the derivation of MonadReader from State won't work because MonadReader is not treated as a superclass of MonadState in Haskell, despite the fact that functionality-wise it is.

What is needed to solve these problems is a feature that is in my opinion strongly missing in Haskell: a form of local instances. This means that we would be able to explicitly specify what implementation of a certain type class should be used to satisfy a certain type class constraint, e.g.

sort :: Ord a => [a] -> [a] sortBy :: forall a. (a -> a -> Bool) -> [a] -> [a] sortBy f = let instance ordDict :: Ord.Dict a ordDict = constructOrdDict f in sort :: Ord a => [a] -> [a]

Local instances were already considered by Wadler when he proposed type classes, but they are problematic to combine with type inference. However, it seems likely that this is not an issue if we require sufficiently informative type annotations.

For the problem above, this would allow to construct, use and lift (together with newtype coercions) a MonadReader dictionary for the State monad without necessarily having it derived automatically if this is not desired. Also, this would allow to write the undecidable instances as normal functions that need to be explicitly invoked instead of inferred by type inference, avoiding the UndecidableInstances problem.

Regards Dominique

As Chris says, you no longer need the GADT at all. {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleInstances #-} import Control.Monad.Identity import Control.Monad.State import Control.Monad.Reader class Monad m => Nomex m where readAccount :: m Int class Nomex m => NomexEffect m where writeAccount :: Int -> m () setVictory :: (forall n. Nomex n => n Bool) -> m () data Game = Game { victory :: (forall m. Nomex m => m Bool) , account :: Int } instance Nomex (State Game) where readAccount = gets account instance NomexEffect (State Game) where writeAccount n = modify $ \game -> game { account = n } setVictory v = modify $ \game -> game { victory = v } instance Nomex (Reader Game) where readAccount = asks account isVictory :: Game -> Bool isVictory = join (runReader . victory) incrAccount :: NomexEffect m => m () incrAccount = readAccount >>= writeAccount . (+101) winOnBigMoney :: NomexEffect m => m () winOnBigMoney = setVictory $ do i <- readAccount --writeAccount 100 return (i > 100) play :: StateT Game Identity () play = do winOnBigMoney incrAccount initGame :: Game initGame = Game (return False) 0 main :: IO () main = do let g = execState play initGame putStrLn $ show $ isVictory g On Wed, Feb 12, 2014 at 11:44 AM, Corentin Dupont

wrote:

Hi guys, so I tried to implement fully the proposition (see below). It works well. However I find it a bit redundant. Can we reduce the repetitions? Perhaps I didn't understand how to write the evaluation...

{-# LANGUAGE RankNTypes #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} module Main where

import Control.Monad.State import Control.Monad.Reader

class Monad m => Nomex m where readAccount :: m Int

class Nomex m => NomexEffect m where writeAccount :: Int -> m () setVictory :: (forall n. Nomex n => n Bool) -> m ()

data Exp a where ReadAccount :: Exp Int WriteAccount :: Int -> Exp () SetVictory :: (forall m. Nomex m => m Bool) -> Exp () Bind :: Exp a -> (a -> Exp b) -> Exp b

Return :: a -> Exp a

instance Monad Exp where

return = Return (>>=) = Bind

instance Nomex Exp where readAccount = ReadAccount

instance NomexEffect Exp where writeAccount = WriteAccount setVictory = SetVictory

data Game = Game { victory :: (forall m. Nomex m => m Bool) , account :: Int }

instance Nomex (State Game) where readAccount = gets account

instance NomexEffect (State Game) where

writeAccount n = modify $ \game -> game { account = n } setVictory v = modify $ \game -> game { victory = v }

instance Nomex (Reader Game) where readAccount = asks account

evaluate :: Exp a -> State Game a evaluate (WriteAccount i) = writeAccount i evaluate ReadAccount = readAccount evaluate (SetVictory v) = setVictory v evaluate (Return a) = return a evaluate (Bind a f) = (evaluate a) >>= evaluate . f

evalNoEff :: Exp a -> Reader Game a evalNoEff ReadAccount = readAccount evalNoEff (Return a) = return a evalNoEff (Bind a f) = (evalNoEff a) >>= evalNoEff . f

isVictory :: Game -> Bool isVictory g = runReader (evalNoEff (victory g)) g

incrAccount :: NomexEffect m => m () incrAccount = readAccount >>= writeAccount . (+101)

winOnBigMoney :: NomexEffect m => m () winOnBigMoney = setVictory $ do i <- readAccount --writeAccount 100 return (i > 100)

play = do winOnBigMoney incrAccount

initGame = Game (return False) 0

main = do let g = execState (evaluate jeu) initGame putStrLn $ show $ isVictory g

On Mon, Feb 10, 2014 at 11:33 AM, Dominique Devriese < dominique.devriese@cs.kuleuven.be> wrote:

...

Corentin,

2014-02-10 10:48 GMT+01:00 Corentin Dupont :

...

That is really interesting. In fact, I didn't have the time to experiment with it, but I definitely want to (have to find some spare time!). I must say I am less used to type classes. At first, my concern with the technique was that two things that belong together, "ReadAccount" and "WriteAccount", are separated.

Yes, this separation of ReadAccount and WriteAccount into Nomex vs NomexEffect is how the two parts (read-only vs read-write) of the DSL are distinguished in this approach..

...

I was also confused that the evaluator is wrapped in a newtype, and that it is an instance of Nomex.

That is non-essential. You can also use

instance Nomex (State Game) where

but it's just cleaner with a newtype...

...

Beside, I suppose it is possible to factorize EvalNoEffect with Eval? Maybe using liftEval anyway...

If I understand correctly, you're asking about how to remove the duplication between EvalNoEffect and Eval?

This is a very good question. My answer is basically that Haskell is missing some type-class-related features to allow for the perfect solution, specifically a form of local instances.

The long story is that instead of the above instances of Nomex and NomexEffect for Eval and EvalNoEffect separately, we would like to be able to write the following instances:

instance MonadReader Game m => Nomex m where readAccount = asks account

instance (MonadReader Game m, MonadState Game m) => NomexEffect m where writeAccount n = modify $ \game -> game { account = n } setVictory v = modify $ \game -> game { victory = v }

and then we can declare newtype Eval a = Eval { eval :: State Game a } deriving (Monad, MonadState Game, MonadReader Game)

newtype EvalNoEffect a = EvalNoEffect { evalNoEffect :: Reader Game a } deriving (Monad, MonadReader Game)

and reuse the single implementation of Nomex for both Eval and EvalNoEffect. However, there are various problems with this solution:

* the instances are not permitted without UndecidableInstances (which I recommend against), * the derivation of MonadReader from State won't work because MonadReader is not treated as a superclass of MonadState in Haskell, despite the fact that functionality-wise it is.

What is needed to solve these problems is a feature that is in my opinion strongly missing in Haskell: a form of local instances. This means that we would be able to explicitly specify what implementation of a certain type class should be used to satisfy a certain type class constraint, e.g.

sort :: Ord a => [a] -> [a] sortBy :: forall a. (a -> a -> Bool) -> [a] -> [a] sortBy f = let instance ordDict :: Ord.Dict a ordDict = constructOrdDict f in sort :: Ord a => [a] -> [a]

Local instances were already considered by Wadler when he proposed type classes, but they are problematic to combine with type inference. However, it seems likely that this is not an issue if we require sufficiently informative type annotations.

For the problem above, this would allow to construct, use and lift (together with newtype coercions) a MonadReader dictionary for the State monad without necessarily having it derived automatically if this is not desired. Also, this would allow to write the undecidable instances as normal functions that need to be explicitly invoked instead of inferred by type inference, avoiding the UndecidableInstances problem.

Regards Dominique

Sorry for the very late and probably no longer relevant reply.

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?

This is a very, very common problem. We have an expression e of type T1, and we want to use it in the context that requires the type T2 (e.g., we want to pass 'e' to a function whose argument type is T2). We feel that we ought to be able to do that. One example is the one you cited: a computation that performs no effect can be regarded as a computation that _may_ perform an effect, and so we should be able to use a non-effectful expression in an effectful context. Another example is numerics: natural numbers are subset of rationals; so it should be morally OK to use a natural number where a rational is required. There are two ways of solving this problem. One is polymorphism, another is subtyping. In the first approach, we define noEff above with the polymorphic type:

noEff :: forall r. Exp r () noEff = return ()

This says that noEff can be used either in NoEffect or Effect contexts. Polymorphic terms can be regarded as `macros', at least conceptually, -- sort of as an abbreviation for the family of definitions noEff_1 :: Exp NoEffect () noEff_1 = return () noEff_2 :: Exp Effect () noEff_2 = return () When you use noEff in the program, the compiler chooses either noEff_1 or noEff_2 depending on the type required by the context. (GHC actually does that in some circumstances). Subtyping means defining a (partial) order among types T2 >= T1 and adding a subsumption rule to the type system e :: T1 T2 >= T1 ----------------- e :: T2 That is, if e has type T1 and T2 is at least as great, e can be given the type T2. Such a rule is very common in various object systems. Since we can't add new rules into the Haskell type system, we have to use a work-around, the explicit coercion. We introduce a function coerce :: T1 -> T2 (often an identity), which is a proof that it is really OK to use (e::T1) at the type T2. We have to explicitly write this coercion function:

hasEffect :: Exp Effect () hasEffect = do coerceEff noEff return ()

We are all familiar with this approach, explicitly writing 'return 1' to, say, return an integer result from a monadic function. Here, return is the explicit coercion, from 1::Int (the pure expression) to m Int (the potentially effectful expression). Other familiar example is newtype: newtype Speed = Speed{unSpeed :: Float} Then expressions (Speed 1.0) or (unSpeed x) / 10.0 etc. are all examples of explicit coercions (which are operationally identity). [Here were do want the coercions to be explicit, at least the Float->Speed coercion. The other could be implicit.] Haskell uses this approach for numeric literals. When we want to use an integer 1 where a rational number is required, we have to write fromInteger 1. Here fromInteger being the explicit coercion. Only we don't have to write 'fromInteger' because GHC inserts it implicitly. The latter example makes too points: explicit coercions are cumbersome to write and we'd rather had them out of sight. The second point is that the coercion is not a single function, but an overloaded function (e.g., return fromInteger). The coercions return and fromInteger are also not operationally identity, which actually do something at run-time. Let's go back to our example and change it to be more interesting, splitting Effect into Read and Write effects, with the order NoEffect < ReadEff < WriteEff. To witness the order, we define class Coerce t1 t2 where coerce :: Exp t1 a -> Exp t2 a instance Coerce NoEffect ReadEff where ... instance Coerce NoEffect WriteEff where ... instance Coerce ReadEffect WriteEff where ... so that we can define

noEff :: Exp NoEffect () noEff = return ()

and write (coerce noEff) if we want to use noEff in effectful situations. We observe that if we make Coerce reflexive, that is, add instance Coerce NoEffect NoEffect where coerce = id ... then we can write (coerce noEff) all the time. And if we do that, why not to fuse coerce into the definition of noEff:

noEff :: Coerce Noeff r => Exp r () noEff = coerce (return ())

We come the full circle to polymorphism -- although generally bounded polymorphism. (In noEff example above we can drop the Coerce constraint since Noeff can be coerced to any other effect. Not so for ReadEffect).

...

data Exp :: Eff -> * -> * where ReadAccount :: Exp NoEffect Int --ReadAccount has no effect Bind :: Effects m n r => Exp m a -> (a -> Exp n b) -> Exp r b ... 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?

This is the infamous read-show problem. See for example http://book.realworldhaskell.org/read/using-typeclasses.html#typeclasses.wel...

eval :: Nomex r a -> State Game a eval a@ReadAccount = liftEval $ evalNoEffect a eval (WriteAccount a) = modify (\g -> g{account = a}) eval (SetVictory v) = modify (\g -> g{victory = v}) eval a@(Return _) = liftEval $ evalNoEffect a eval (Bind exp f) = eval exp >>= eval . f

This is a common pitfall. We should write

eval :: Nomex r a -> State Game a eval ReadAccount = liftEval $ evalNoEffect ReadAccount eval (Return x) = liftEval $ evalNoEffect (Return x) ...

It seems like a boilerplate: why do we have to write the same 'ReadAccount' on the left hand side and on the right-hand side (ditto for Return x). Can't we just share, like in the original code? The answer is no: The ReadAccount on the left hand side of the eval equation is different from ReadAccount on the right-hand side. They are spelled the same, but their types differ. On the left-hand-side, ReadAccount :: Nomex Effect (), but on the right-hand side, ReadAccount :: Nomex Effect (). This is a frequent problem with constants like [] which may have more than one type.

So finally, I think there are really 3 solutions to the problem of representing the semantic of effects/no effects (effect-less instructions can be run in effect-full context, but not the opposite). We can encode this semantic at: - value level - type level - typeclass level At value level, the semantic is encoded by a DSL instruction 'NoEff' that wraps an effect-less instruction into an effect-full one: NoEff :: Nomex NoEffect a -> Nomex Effect a See https://github.com/cdupont/Nomyx-design/blob/master/TypeParamEffect-Concrete... At type level, the semantic is encoded by using a polymorphic type parameter that can take two concrete type, 'Effect' or 'NoEffect': ReadAccount :: Nomex r Int See https://github.com/cdupont/Nomyx-design/blob/master/TypeParamEffect-Polymorp... At typeclass level, the semantic is encoded by the hierarchy of classes: class Nomex m => NomexEffect m where... See https://github.com/cdupont/Nomyx-design/blob/master/TypeClassEffect.hs Now I have to choose one :)) On Mon, Feb 24, 2014 at 12:18 PM, Corentin Dupont

wrote:

Thanks a lot Oleg. I finally had time to fully read and understand your comments :)

From all the comments I got, I put everything together in two blog posts: http://www.corentindupont.info/blog/posts/2014-02-12-Effect-Class.html Thanks!

On Thu, Feb 13, 2014 at 8:28 AM, wrote:

...

Sorry for the very late and probably no longer relevant reply.

...

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?

This is a very, very common problem. We have an expression e of type T1, and we want to use it in the context that requires the type T2 (e.g., we want to pass 'e' to a function whose argument type is T2). We feel that we ought to be able to do that. One example is the one you cited: a computation that performs no effect can be regarded as a computation that _may_ perform an effect, and so we should be able to use a non-effectful expression in an effectful context. Another example is numerics: natural numbers are subset of rationals; so it should be morally OK to use a natural number where a rational is required.

There are two ways of solving this problem. One is polymorphism, another is subtyping. In the first approach, we define noEff above with the polymorphic type:

...

noEff :: forall r. Exp r () noEff = return ()

This says that noEff can be used either in NoEffect or Effect contexts. Polymorphic terms can be regarded as `macros', at least conceptually, -- sort of as an abbreviation for the family of definitions

noEff_1 :: Exp NoEffect () noEff_1 = return ()

noEff_2 :: Exp Effect () noEff_2 = return ()

When you use noEff in the program, the compiler chooses either noEff_1 or noEff_2 depending on the type required by the context. (GHC actually does that in some circumstances).

Subtyping means defining a (partial) order among types T2 >= T1 and adding a subsumption rule to the type system

e :: T1 T2 >= T1 ----------------- e :: T2

That is, if e has type T1 and T2 is at least as great, e can be given the type T2. Such a rule is very common in various object systems. Since we can't add new rules into the Haskell type system, we have to use a work-around, the explicit coercion. We introduce a function coerce :: T1 -> T2 (often an identity), which is a proof that it is really OK to use (e::T1) at the type T2. We have to explicitly write this coercion function:

...

hasEffect :: Exp Effect () hasEffect = do coerceEff noEff return ()

We are all familiar with this approach, explicitly writing 'return 1' to, say, return an integer result from a monadic function. Here, return is the explicit coercion, from 1::Int (the pure expression) to m Int (the potentially effectful expression).

Other familiar example is newtype: newtype Speed = Speed{unSpeed :: Float} Then expressions (Speed 1.0) or (unSpeed x) / 10.0 etc. are all examples of explicit coercions (which are operationally identity). [Here were do want the coercions to be explicit, at least the Float->Speed coercion. The other could be implicit.]

Haskell uses this approach for numeric literals. When we want to use an integer 1 where a rational number is required, we have to write fromInteger 1. Here fromInteger being the explicit coercion.

Only we don't have to write 'fromInteger' because GHC inserts it implicitly. The latter example makes too points: explicit coercions are cumbersome to write and we'd rather had them out of sight. The second point is that the coercion is not a single function, but an overloaded function (e.g., return fromInteger). The coercions return and fromInteger are also not operationally identity, which actually do something at run-time.

Let's go back to our example and change it to be more interesting, splitting Effect into Read and Write effects, with the order NoEffect < ReadEff < WriteEff. To witness the order, we define

class Coerce t1 t2 where coerce :: Exp t1 a -> Exp t2 a

instance Coerce NoEffect ReadEff where ... instance Coerce NoEffect WriteEff where ... instance Coerce ReadEffect WriteEff where ...

so that we can define

...

noEff :: Exp NoEffect () noEff = return ()

and write (coerce noEff) if we want to use noEff in effectful situations. We observe that if we make Coerce reflexive, that is, add

instance Coerce NoEffect NoEffect where coerce = id ...

then we can write (coerce noEff) all the time. And if we do that, why not to fuse coerce into the definition of noEff:

...

noEff :: Coerce Noeff r => Exp r () noEff = coerce (return ())

We come the full circle to polymorphism -- although generally bounded polymorphism. (In noEff example above we can drop the Coerce constraint since Noeff can be coerced to any other effect. Not so for ReadEffect).

...

...

data Exp :: Eff -> * -> * where ReadAccount :: Exp NoEffect Int --ReadAccount has no effect Bind :: Effects m n r => Exp m a -> (a -> Exp n b) -> Exp r b ... 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?

This is the infamous read-show problem. See for example

http://book.realworldhaskell.org/read/using-typeclasses.html#typeclasses.wel...

...

eval :: Nomex r a -> State Game a eval a@ReadAccount = liftEval $ evalNoEffect a eval (WriteAccount a) = modify (\g -> g{account = a}) eval (SetVictory v) = modify (\g -> g{victory = v}) eval a@(Return _) = liftEval $ evalNoEffect a eval (Bind exp f) = eval exp >>= eval . f

This is a common pitfall. We should write

...

eval :: Nomex r a -> State Game a eval ReadAccount = liftEval $ evalNoEffect ReadAccount eval (Return x) = liftEval $ evalNoEffect (Return x) ...

It seems like a boilerplate: why do we have to write the same 'ReadAccount' on the left hand side and on the right-hand side (ditto for Return x). Can't we just share, like in the original code? The answer is no: The ReadAccount on the left hand side of the eval equation is different from ReadAccount on the right-hand side. They are spelled the same, but their types differ. On the left-hand-side, ReadAccount :: Nomex Effect (), but on the right-hand side, ReadAccount :: Nomex Effect (). This is a frequent problem with constants like [] which may have more than one type.