Add type signature for a helper function inside

Question

First I define the following data type

data Supply s a = S (Stream s -> (a, Stream s))
data Stream a = Cons a (Stream a)

Then I want to implement a function which maps to a Supply with the following type signature:

mapSupply :: (a -> b) -> Supply s a -> Supply s b

And here is my implementation: (which compiles with no problem)

mapSupply :: (a -> b) -> Supply s a -> Supply s b
mapSupply mapFunc (S supFuncA) = S supFuncB where
    supFuncB strm = let (la, strms) = supFuncA strm in 
        ((mapFunc la), strms)

Then I met a problem when I tried to write down the type signature for the helper function named supFuncB which I defined inside mapSupply.

The type signature for supFuncB is very simple and should be:

supFuncB :: Stream s -> (b, Stream s)

However when I tried to add the type signature in the code, I got a compiler error. The code looks like this

mapSupply :: (a -> b) -> Supply s a -> Supply s b
mapSupply mapFunc (S supFuncA) = S supFuncB where
    supFuncB :: Stream s -> (b, Stream s)
    supFuncB strm = let (la, strms) = supFuncA strm in 
        ((mapFunc la), strms)

And then compiler complained:

• Couldn't match type ‘s1’ with ‘s’
  ‘s1’ is a rigid type variable bound by
    the type signature for:
      supFuncB :: forall s1 b1. Stream s1 -> (b1, Stream s1)
    at Main.hs:58:5-41
  ‘s’ is a rigid type variable bound by
    the type signature for:
      mapSupply :: forall a b s. (a -> b) -> Supply s a -> Supply s b
    at Main.hs:56:1-49
  Expected type: Stream s1
    Actual type: Stream s
• In the expression: strms
  In the expression: ((mapFunc la), strms)
  In the expression:
    let (la, strms) = supFuncA strm in ((mapFunc la), strms)

I'm very new to Haskell and I don't understand why the compile would fail? And what should be the correct type signature if I were to add it in the code.

This is a result of the monomorphism restriction: wiki.haskell.org/Monomorphism_restriction — Willem Van Onsem
@WillemVanOnsem At a glance, this looks more like a ScopedTypeVariables kind of issue than a monomorphism restriction one -- there are no constraints to make the monomorphism restriction kick in. — duplode
With ScopedTypeVariables you'd also need an explicit forall to put the type variables into scope. see this answer (I'm not 100% sure this is an actual duplicate) — Mor A.
Isn't mapSupply just fmap if you define type Supply s a = State s a? — chepner

duplode duplode · Accepted Answer · 2019-05-31T22:22:49

To begin from the end, the solution is turning on ScopedTypeVariables and using an explicit forall in the mapSupply signature, like this:

{-# LANGUAGE ScopedTypeVariables #-}  -- Put this at the top of your file.

mapSupply :: forall a b s. (a -> b) -> Supply s a -> Supply s b
mapSupply mapFunc (S supFuncA) = S supFuncB where
    supFuncB :: Stream s -> (b, Stream s)
    supFuncB strm = let (la, strms) = supFuncA strm in 
        ((mapFunc la), strms)

What follows is an explanation of why that is necessary.

When you write a signature like this:

mapSupply :: (a -> b) -> Supply s a -> Supply s b

GHC actually sees this:

mapSupply :: forall a b s. (a -> b) -> Supply s a -> Supply s b

The forall, which normally can be left implicit, says that a, b and s can be anything -- mapSupply is a polymorphic function, and so whoever uses it is free to choose any concrete types for the three type variables. Writing the foralls explicitly, your second definition would look like this:

mapSupply :: forall a b s. (a -> b) -> Supply s a -> Supply s b
mapSupply mapFunc (S supFuncA) = S supFuncB where
    supFuncB :: forall s b. Stream s -> (b, Stream s)
    supFuncB strm = let (la, strms) = supFuncA strm in 
        ((mapFunc la), strms)

According to it, a, b and s in mapSupply can be anything, and the same goes for s and b in supFuncB. That is a problem, though. For instance, the definition involves strms, whose type is s... except that s, which shows up because you are using supFuncA, is not the one from the supFuncB signature, but rather the one from the mapSupply signature. While the s from mapSupply can, in principle, be anything, as I noted before, once you actually choose an s by using mapSupply, the s from supFuncB must match it. That being so, the forall in the supFuncB signature is out of place, as its type variables can't really be anything. It becomes easier to see if we rename the type variables from supFuncB so that their names don't clash with those from mapSupply (given the forall, it should be a valid move to do that):

mapSupply :: forall a b s. (a -> b) -> Supply s a -> Supply s b
mapSupply mapFunc (S supFuncA) = S supFuncB where
    supFuncB :: forall s1 b1. Stream s1 -> (b1, Stream s1)
    supFuncB strm = let (la, strms) = supFuncA strm in 
        ((mapFunc la), strms)

(GHC does that internally, which explains why the error message you got mentioned an s1 type variable.)

This problem only happened because of the signature added to supFuncB, which introduced an implicit forall. Without the signature, GHC does what you want by not generalising the types from supFuncB -- in that case, it is not polymorphic, but rather monomorphic in the type variables a, b and s, which are borrowed from mapSupply. The ScopedTypeVariables extension makes it possible to recover that behaviour while writing a type signature for supFuncB. When it is enabled, using an explicit forall for the type variables in a signature will make any type variables with the same name in the corresponding definition refer to the same thing (as long as they aren't also under a forall in their own signatures). In other words, by doing that it becomes possible to refer to the variables from the outer signature anywhere within the scope of the corresponding definition, which justifies the name of the extension.

Add type signature for a helper function inside

1 Answers