[Haskell-cafe] Why does disambiguation in RebindableSyntax sometimes requires type signatures?
Chris Wong
lambda.fairy at gmail.com
Wed Oct 28 02:31:24 UTC 2015
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
More information about the Haskell-Cafe
mailing list