[Haskell-cafe] Why does disambiguation in RebindableSyntax sometimes requires type signatures?
Jan Bracker
jan.bracker at googlemail.com
Tue Oct 27 14:14:00 UTC 2015
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20151027/4a471617/attachment.html>
More information about the Haskell-Cafe
mailing list