Specifying a Function Type in a Where Clause
I have the following Monad instance based on the stuff in these slides :
{-# LANGUAGE InstanceSigs #-}
newtype Iter a = Iter { runIter :: Chunk -> Result a }
instance Monad Iter where
return = Iter . Done
(>>=) :: Iter a -> (a -> Iter b) -> Iter b
(Iter iter0) >>= fiter = Iter $ \chunk -> continue (iter0 chunk)
where continue :: Result a -> Result b
continue (Done x rest) = runIter (fiter x) rest
continue (NeedInput iter1) = NeedInput (iter1 >>= fiter)
continue (NeedIO ior) = NeedIO (liftM continue ior)
continue (Failed e) = Failed e
This will result in the following error:
β’ Couldn't match type βbβ with βb1β
βbβ is a rigid type variable bound by
the type signature for:
(>>=) :: forall a b. Iter a -> (a -> Iter b) -> Iter b
at Iteratee.hs:211:12
βb1β is a rigid type variable bound by
the type signature for:
continue :: forall a1 b1. Result a1 -> Result b1
at Iteratee.hs:214:23
Expected type: Result b1
Actual type: Result b
β’ In the expression: runIter (fiter x) rest
In an equation for βcontinueβ:
continue (Done x rest) = runIter (fiter x) rest
In an equation for β>>=β:
(Iter iter0) >>= fiter
= Iter $ \ chunk -> continue (iter0 chunk)
where
continue :: Result a -> Result b
continue (Done x rest) = runIter (fiter x) rest
continue (NeedInput iter1) = NeedInput (iter1 >>= fiter)
continue (NeedIO ior) = NeedIO (liftM continue ior)
continue (Failed e) = Failed e
β’ Relevant bindings include
continue :: Result a1 -> Result b1 (bound at Iteratee.hs:215:11)
fiter :: a -> Iter b (bound at Iteratee.hs:212:20)
(>>=) :: Iter a -> (a -> Iter b) -> Iter b
(bound at Iteratee.hs:212:3)
To add to my confusion, if I leave continue
undefined, but I will assign a type that the code compiles.
My guess is that this problem is caused by a continuation actually having the type
continue :: forall a1 b1. Result a1 -> Result b1
therefore, two a
and b
of the above types are actually different. But nevertheless, the continue
above must have a type. The question then becomes which is the type of this function assigned by the compiler when the types are omitted.
EDIT:
If the parameter is iter
explicitly passed, the code is compiled:
instance Monad Iter where
return = Iter . Done
(>>=) :: Iter a -> (a -> Iter b) -> Iter b
(Iter iter0) >>= fiter0 = Iter $ \chunk -> continue fiter0 (iter0 chunk)
where continue :: (a -> Iter b) -> Result a -> Result b
continue fiter (Done x rest) = runIter (fiter x) rest
continue fiter (NeedInput iter1) = NeedInput (iter1 >>= fiter)
continue fiter (NeedIO ior) = NeedIO (liftM (continue fiter) ior)
continue _ (Failed e) = Failed e
However, I wish I could not be able to pass this parameter explicitly, being able to specify the type continue
.
source to share
In basic Haskell, each type signature is implicitly quantified universally
foo :: Bool -> a -> a -> a
foo b x y = bar y
where bar :: a -> a
bar y | b = x
| otherwise = y
actually means:
foo :: forall a. Bool -> a -> a -> a
foo b x y = bar y
where bar :: forall a1. a1 -> a1
bar y | b = x
| otherwise = y
and won't compile because it x
doesn't have a type a1
.
Removing the type signature bar
makes it compile, and the compiler will associate to indicate the correct type a -> a
, where it is a
NOT universally quantified. Note that this is a type that the compiler can do, but that the user is prohibited from writing.
This is pretty awkward!
So the ScopedTypeVarables
GHC extension bypasses this by allowing you to write
foo :: forall a. Bool -> a -> a -> a
foo b x y = bar y
where bar :: a -> a
bar y | b = x
| otherwise = y
and here the first one forall a.
makes it a
available in internal declarations. In addition, the type bar
remains a -> a
and is not generic because a
it is now in scope. Hence, it compiles and the user can now write the annotation of the required type.
source to share