[Haskell-cafe] Why does disambiguation in RebindableSyntax sometimes requires type signatures?
Jan Bracker
jan.bracker at googlemail.com
Mon Nov 2 18:06:43 UTC 2015
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 <lambda.fairy at gmail.com>:
> 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-monomorphism-restriction/
>
> 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.
>
> On Wed, Oct 28, 2015 at 3:14 AM, Jan Bracker <jan.bracker at googlemail.com>
> wrote:
> > 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
> 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 at 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 <lambda.fairy at gmail.com>:
> 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-monomorphism-restriction/
>
> 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.
>
> On Wed, Oct 28, 2015 at 3:14 AM, Jan Bracker <jan.bracker at googlemail.com>
> wrote:
> > 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
> 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 at 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20151102/c81882e0/attachment.html>
More information about the Haskell-Cafe
mailing list