Type signature in a where clause

Question

I've written a function similar to Data.Enumerator.List.map that makes an Iteratee compatible with an Enumerator that feeds a different Stream type.

import Data.Enumerator

test :: Monad m => (ao -> ai) -> Iteratee ai m b -> Iteratee ao m b
test f iter = go $$ iter
   where go (Continue k) = continue $
            \stream -> go $$ k (fmap f stream)
         go (Yield res _) = yield res EOF

If I omit the type signature for go, this will work just fine. However, I'd like to include it but I'm unable to determine what the correct signature should be. Here's what I think it should be:

go :: Monad m => Step ai m b -> Iteratee ao m b

but that doesn't work.
I need some advice on finding the correct type signature for go.

Christianly

Answer 1

You probably can't give go a type signature as-is.

The reason for this is that it makes use of polymorphic arguments bound by test. This means that, inside go, the identifier f has type (ao -> ai) for some specific, but unknown types ao and ai.

Type variables are generally only in scope for the single type signature where they're introduced, so when you give go its own type signature, the ao and ai there are new, polymorphic types, which of course causes a type error when trying to combine them with the similarly named, but fixed (and unknowable) types from test's signature.

The end result is that you can't write the type of go explicitly, which is not very satisfying. To solve this, GHC offers the ScopedTypeVariables extension, which allows bringing variables introduced in a type signature in scope inside the where clause of the function, among other things.

Note that if you only use the where clause to create an internal scope for definitions, and don't make use of identifiers bound by arguments to the outer function, you can write type signatures in the where clause just like you can for top level bindings. If you don't want to use GHC extensions, you can simply pass the parameters in redundantly. Something like this should work in that case:

test :: Monad m => (ao -> ai) -> Iteratee ai m b -> Iteratee ao m b
test f iter = go f $$ iter
  where go :: Monad m => (ao -> ai) -> Step ai m b -> Iteratee ao m b
        go f (Continue k) = continue $
             \stream -> go f $$ k (fmap f stream)
        go _ (Yield res _) = yield res EOF

Vaginal

@hammar: Thanks. I swear I make a dumb typo every time I put more than four lines of code in an answer without loading them in GHCi first. Sigh... – Vaginal

Answer 2

You probably want that type, but with the ScopedTypeVariables extension enabled and with the variables from test's type signature in scope:

{-# LANGUAGE ScopedTypeVariables #-}
import Data.Enumerator
test :: forall m ai ao b. Monad m => (ao -> ai) -> Iteratee ai m b -> Iteratee ao m b
test f iter = go $$ iter
   where go :: Step ai m b -> Iteratee ao m b
         go (Continue k) = continue $
            \stream -> go $$ k (fmap f stream)
         go (Yield res _) = yield res EOF

See the GHC documentation for more information.

Micro

N.B. -- Observe that there's no Monad m constraint here in go's type, unlike the proposed type in the question. This is important, because not only is the same m in scope, the class constraint is also still in scope. – Vaginal

...though it would probably work fine if you did add the constraint in. It would just be particularly easy for GHC to find an instance. – Micro

It does. You could also add Monad Maybe, m ~ m, or any other trivial constraint to the context, and GHC will accept it without complaint. It warns about (Monad m, Monad m, Monad m) => though. – Vaginal

Being new to ScopedTypeVariables, adding forall m ai ao b. to the outer function test was the critical part I was missing. Thanks! – Cropland