Hi Chris, thanks for your answer! I checked both of your solutions and when I apply either I still get errors. If I add arguments to my local definitions I get the following errors: Main.hs:27:3: Couldn't match kind ‘*’ with ‘[*]’ When matching types m0 :: * -> * -> * State :: [*] -> * -> * Expected type: m0 f0 Bool -> (Bool -> m0 (E.Unit m0) (Either Tree [Int])) -> State '["flatten" :-> (Bool :! 'R)] (Either Tree [Int]) Actual type: m0 f0 Bool -> (Bool -> m0 (E.Unit m0) (Either Tree [Int])) -> m0 (E.Plus m0 f0 (E.Unit m0)) (Either Tree [Int]) Relevant bindings include return :: forall a. a -> m0 (E.Unit m0) a (bound at Main.hs:35:9) In a stmt of a 'do' block: flatten <- get (Var :: Var "flatten") In the expression: do { flatten <- get (Var :: Var "flatten"); if flatten then return $ Right [i] else return $ Left $ Leaf i } In an equation for ‘process’: process (Leaf i) = do { flatten <- get (Var :: Var "flatten"); if flatten then return $ Right [...] else return $ Left $ Leaf i } where (>>=) m f = (E.>>=) m f (>>) m n = (E.>>) m n return = E.return fail = E.fail Main.hs:35:18: No instance for (E.Effect m0) arising from a use of ‘E.return’ In the expression: E.return In an equation for ‘return’: return = E.return In an equation for ‘process’: process (Leaf i) = do { flatten <- get (Var :: Var "flatten"); if flatten then return $ Right [...] else return $ Left $ Leaf i } where (>>=) m f = (E.>>=) m f (>>) m n = (E.>>) m n return = E.return fail = E.fail Main.hs:47:18: No instance for (E.Effect m1) arising from a use of ‘E.return’ In the expression: E.return In an equation for ‘return’: return = E.return In an equation for ‘process’: process (Branch tl tr) = do { eitherL <- process tl; eitherR <- process tr; case (eitherL, eitherR) of { (Left l, Left r) -> return $ Left $ Branch l r (Right l, Right r) -> return $ Right $ l ++ r } } where (>>=) m f = (E.>>=) m f (>>) m n = (E.>>) m n return = E.return fail = E.fail Which again I can't explain for myself. If I add NoMonomorphismRestriction, I get the following errors: Main.hs:27:3: Couldn't match kind ‘*’ with ‘[*]’ When matching types m0 :: * -> * -> * State :: [*] -> * -> * Expected type: m0 f0 Bool -> (Bool -> m0 (E.Unit m0) (Either Tree [Int])) -> State '["flatten" :-> (Bool :! 'R)] (Either Tree [Int]) Actual type: m0 f0 Bool -> (Bool -> m0 (E.Unit m0) (Either Tree [Int])) -> m0 (E.Plus m0 f0 (E.Unit m0)) (Either Tree [Int]) In a stmt of a 'do' block: flatten <- get (Var :: Var "flatten") In the expression: do { flatten <- get (Var :: Var "flatten"); if flatten then return $ Right [i] else return $ Left $ Leaf i } In an equation for ‘process’: process (Leaf i) = do { flatten <- get (Var :: Var "flatten"); if flatten then return $ Right [...] else return $ Left $ Leaf i } where (>>=) = (E.>>=) (>>) = (E.>>) return = E.return fail = E.fail This seems as if data kinds is not able to infer the proper kinds for the involved types without type signatures. So adding NoMonomorphismRestriction does seem to solve some problems, but adding parameters does not seem to be a solution to the problems related to the monomorphism restriction. Any advice? Best, Jan 2015-10-28 2:31 GMT+00:00 Chris Wong :

Hi Jan,

Looks like the monomorphism restriction to me. This article [1] is a great explanation of this quirk.

[1] http://lambda.jstolarek.com/2012/05/towards-understanding-haskells-monomorph...

There are two solutions:

1. Add {-# LANGUAGE NoMonomorphismRestriction #-} to your code.

2. Give each binding explicit arguments:

process = ... -- as before where m >>= k = m E.>>= k m >> n = m E.>> n return x = E.return x

Since the monomorphism restriction doesn't apply to declarations with arguments, this change should make the bindings polymorphic again.

Hope this helps.

...

Hello,

I am currently playing around with RebindableSyntax and having several bind/return/sequence functions in scope at the same time. I thought that it would be enough to just pick the right one to use in each do-block by using a "where" or a "let". Surprisingly, I get some type related issues I can only fix by adding in some type signatures, but I don't understand why these signatures are actually necessary.

Here is my example program:

{-# LANGUAGE RebindableSyntax #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-}

import Prelude import qualified Prelude as P import qualified Control.Effect as E import Control.Effect.State

ifThenElse :: Bool -> a -> a -> a ifThenElse True t e = t ifThenElse False t e = e

main :: IO () main = do return () where return = P.return

data Tree = Leaf Int | Branch Tree Tree

process :: Tree -> State '[ "flatten" :-> Bool :! 'R ] (Either Tree [Int]) process (Leaf i) = do flatten <- get (Var :: (Var "flatten")) if flatten then return $ Right [i] else return $ Left $ Leaf i where --(>>=) :: (E.Inv State f g) => State f a -> (a -> State g b) -> State (E.Plus State f g) b (>>=) = (E.>>=) (>>) :: (E.Inv State f g) => State f a -> State g b -> State (E.Plus State f g) b (>>) = (E.>>) return = E.return fail = E.fail process (Branch tl tr) = do eitherL <- process tl eitherR <- process tr case (eitherL, eitherR) of (Left l, Left r) -> return $ Left $ Branch l r (Right l, Right r) -> return $ Right $ l ++ r where (>>=) :: (E.Inv State f g) => State f a -> (a -> State g b) -> State (E.Plus State f g) b (>>=) = (E.>>=) (>>) :: (E.Inv State f g) => State f a -> State g b -> State (E.Plus State f g) b (>>) = (E.>>) return = E.return fail = E.fail

The program uses the "effect-monad" package in version 0.6.1.

1) The type signatures in the "where" following each do-block of the "process" function are required. If I remove the type signature of the sequence functions I get a type error of the following nature:

examples/effect/Test.hs:33:16: Could not deduce (E.Inv m0 f0 g0) arising from a use of ‘E.>>’ Relevant bindings include (>>) :: m0 f0 a -> m0 g0 b -> m0 (E.Plus m0 f0 g0) b (bound at examples/effect/Test.hs:33:9) In the expression: (E.>>) In an equation for ‘>>’: (>>) = (E.>>) In an equation for ‘process’: process (Leaf i) = do { flatten <- get (Var :: Var "flatten"); if flatten then return $ Right [...] else return $ Left $ Leaf i } where (>>=) = (E.>>=) (>>) = (E.>>) return = E.return fail = E.fail

examples/effect/Test.hs:33:16: No instance for (E.Effect m0) arising from a use of ‘E.>>’ In the expression: (E.>>) In an equation for ‘>>’: (>>) = (E.>>) In an equation for ‘process’: process (Leaf i) = do { flatten <- get (Var :: Var "flatten"); if flatten then return $ Right [...] else return $ Left $ Leaf i } where (>>=) = (E.>>=) (>>) = (E.>>) return = E.return fail = E.fail

Which I interpret as the inability to infer the "E.Effect" and "E.Inv" constraints that are implied by the use of "E.>>". But why can't those constraints be inferred correctly? Shouldn't a definition like "(>>) = (E.>>)" just propagate the type signature and specialize it as needed?

2) If I remove the type signature for the bind operation, I get the following type error:

examples/effect/Test.hs:38:3: Couldn't match type ‘'["flatten" :-> (Bool :! 'R)]’ with ‘'[]’ Expected type: State '["flatten" :-> (Bool :! 'R)] (Either Tree [Int]) -> (Either Tree [Int] -> State '[] (Either Tree [Int])) -> State '[] (Either Tree [Int]) Actual type: State '["flatten" :-> (Bool :! 'R)] (Either Tree [Int]) -> (Either Tree [Int] -> State '[] (Either Tree [Int])) -> State (E.Plus State '["flatten" :-> (Bool :! 'R)] '[]) (Either Tree [Int]) In a stmt of a 'do' block: eitherR <- process tr In the expression: do { eitherL <- process tl; eitherR <- process tr; case (eitherL, eitherR) of { (Left l, Left r) -> return $ Left $ Branch l r (Right l, Right r) -> return $ Right $ l ++ r } } In an equation for ‘process’: process (Branch tl tr) = do { eitherL <- process tl; eitherR <- process tr; case (eitherL, eitherR) of { (Left l, Left r) -> return $ Left $ Branch l r (Right l, Right r) -> return $ Right $ l ++ r } } where (>>=) = (E.>>=) (>>) :: (E.Inv State f g) => State f a -> State g b -> State (E.Plus State f g) b (>>) = (E.>>) return = E.return

Which tells me that GHC is expecting the wrong type, but inferring the correct type. Again I don't see why this wrong type is expected and the right type is ignored.

In either case, why does adding or removing the type signature for the local definitions make a difference at all? I suspect the issue has to do with

On Wed, Oct 28, 2015 at 3:14 AM, Jan Bracker wrote: the

...

language extensions I enabled or the type-level computations that are done by the "effect-monad" package, but I cannot find a satisfying answer. Does anybody have a good explanation?

I am working with GHC 7.10.2.

Best, Jan

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

-- Chris Wong (https://lambda.xyz)

"I fear that Haskell is doomed to succeed." -- Tony Hoare

2015-10-28 2:31 GMT+00:00 Chris Wong :

Hi Jan,

Looks like the monomorphism restriction to me. This article [1] is a great explanation of this quirk.

[1] http://lambda.jstolarek.com/2012/05/towards-understanding-haskells-monomorph...

There are two solutions:

1. Add {-# LANGUAGE NoMonomorphismRestriction #-} to your code.

2. Give each binding explicit arguments:

process = ... -- as before where m >>= k = m E.>>= k m >> n = m E.>> n return x = E.return x

Since the monomorphism restriction doesn't apply to declarations with arguments, this change should make the bindings polymorphic again.

Hope this helps.

...

Hello,

I am currently playing around with RebindableSyntax and having several bind/return/sequence functions in scope at the same time. I thought that it would be enough to just pick the right one to use in each do-block by using a "where" or a "let". Surprisingly, I get some type related issues I can only fix by adding in some type signatures, but I don't understand why these signatures are actually necessary.

Here is my example program:

{-# LANGUAGE RebindableSyntax #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-}

import Prelude import qualified Prelude as P import qualified Control.Effect as E import Control.Effect.State

ifThenElse :: Bool -> a -> a -> a ifThenElse True t e = t ifThenElse False t e = e

main :: IO () main = do return () where return = P.return

data Tree = Leaf Int | Branch Tree Tree

process :: Tree -> State '[ "flatten" :-> Bool :! 'R ] (Either Tree [Int]) process (Leaf i) = do flatten <- get (Var :: (Var "flatten")) if flatten then return $ Right [i] else return $ Left $ Leaf i where --(>>=) :: (E.Inv State f g) => State f a -> (a -> State g b) -> State (E.Plus State f g) b (>>=) = (E.>>=) (>>) :: (E.Inv State f g) => State f a -> State g b -> State (E.Plus State f g) b (>>) = (E.>>) return = E.return fail = E.fail process (Branch tl tr) = do eitherL <- process tl eitherR <- process tr case (eitherL, eitherR) of (Left l, Left r) -> return $ Left $ Branch l r (Right l, Right r) -> return $ Right $ l ++ r where (>>=) :: (E.Inv State f g) => State f a -> (a -> State g b) -> State (E.Plus State f g) b (>>=) = (E.>>=) (>>) :: (E.Inv State f g) => State f a -> State g b -> State (E.Plus State f g) b (>>) = (E.>>) return = E.return fail = E.fail

The program uses the "effect-monad" package in version 0.6.1.

1) The type signatures in the "where" following each do-block of the "process" function are required. If I remove the type signature of the sequence functions I get a type error of the following nature:

examples/effect/Test.hs:33:16: Could not deduce (E.Inv m0 f0 g0) arising from a use of ‘E.>>’ Relevant bindings include (>>) :: m0 f0 a -> m0 g0 b -> m0 (E.Plus m0 f0 g0) b (bound at examples/effect/Test.hs:33:9) In the expression: (E.>>) In an equation for ‘>>’: (>>) = (E.>>) In an equation for ‘process’: process (Leaf i) = do { flatten <- get (Var :: Var "flatten"); if flatten then return $ Right [...] else return $ Left $ Leaf i } where (>>=) = (E.>>=) (>>) = (E.>>) return = E.return fail = E.fail

examples/effect/Test.hs:33:16: No instance for (E.Effect m0) arising from a use of ‘E.>>’ In the expression: (E.>>) In an equation for ‘>>’: (>>) = (E.>>) In an equation for ‘process’: process (Leaf i) = do { flatten <- get (Var :: Var "flatten"); if flatten then return $ Right [...] else return $ Left $ Leaf i } where (>>=) = (E.>>=) (>>) = (E.>>) return = E.return fail = E.fail

Which I interpret as the inability to infer the "E.Effect" and "E.Inv" constraints that are implied by the use of "E.>>". But why can't those constraints be inferred correctly? Shouldn't a definition like "(>>) = (E.>>)" just propagate the type signature and specialize it as needed?

2) If I remove the type signature for the bind operation, I get the following type error:

examples/effect/Test.hs:38:3: Couldn't match type ‘'["flatten" :-> (Bool :! 'R)]’ with ‘'[]’ Expected type: State '["flatten" :-> (Bool :! 'R)] (Either Tree [Int]) -> (Either Tree [Int] -> State '[] (Either Tree [Int])) -> State '[] (Either Tree [Int]) Actual type: State '["flatten" :-> (Bool :! 'R)] (Either Tree [Int]) -> (Either Tree [Int] -> State '[] (Either Tree [Int])) -> State (E.Plus State '["flatten" :-> (Bool :! 'R)] '[]) (Either Tree [Int]) In a stmt of a 'do' block: eitherR <- process tr In the expression: do { eitherL <- process tl; eitherR <- process tr; case (eitherL, eitherR) of { (Left l, Left r) -> return $ Left $ Branch l r (Right l, Right r) -> return $ Right $ l ++ r } } In an equation for ‘process’: process (Branch tl tr) = do { eitherL <- process tl; eitherR <- process tr; case (eitherL, eitherR) of { (Left l, Left r) -> return $ Left $ Branch l r (Right l, Right r) -> return $ Right $ l ++ r } } where (>>=) = (E.>>=) (>>) :: (E.Inv State f g) => State f a -> State g b -> State (E.Plus State f g) b (>>) = (E.>>) return = E.return

Which tells me that GHC is expecting the wrong type, but inferring the correct type. Again I don't see why this wrong type is expected and the right type is ignored.

In either case, why does adding or removing the type signature for the local definitions make a difference at all? I suspect the issue has to do with

On Wed, Oct 28, 2015 at 3:14 AM, Jan Bracker wrote: the

...

language extensions I enabled or the type-level computations that are done by the "effect-monad" package, but I cannot find a satisfying answer. Does anybody have a good explanation?

I am working with GHC 7.10.2.

Best, Jan

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

-- Chris Wong (https://lambda.xyz)

"I fear that Haskell is doomed to succeed." -- Tony Hoare

Hi Henning, but with type signatures the errors do not occure. My best guess for that one is that inferring the correct kinds for lifted data types is not done properly. Best, Jan 2015-11-02 18:20 GMT+00:00 Henning Thielemann

:

On Mon, 2 Nov 2015, Jan Bracker wrote:

If I add arguments to my local definitions I get the following errors:

...

Main.hs:27:3: Couldn't match kind ‘*’ with ‘[*]’ When matching types m0 :: * -> * -> * State :: [*] -> * -> *

That sounds like a serious type mismatch that cannot simply be avoided by adding type signatures or type extensions.