Specifying a function type signature in a where clause

Question

The following function implements the good old filter function from lists by using the recursion-schemes library.

import Data.Functor.Foldable 

catafilter :: (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg 
  where
    -- alg :: ListF a [a] -> [a]
    alg  Nil  =  []
    alg  (Cons x xs) = if (p x) then x : xs else xs

It compiles and a short test like catafilter odd [1,2,3,4] is successful. However, if I uncomment the type signature for alg I get the following error:

src/cata.hs:8:30: error:
    • Couldn't match expected type ‘a’ with actual type ‘a1’
      ‘a1’ is a rigid type variable bound by
        the type signature for:
          alg :: forall a1. ListF a1 [a1] -> [a1]
        at src/cata.hs:6:5-29
      ‘a’ is a rigid type variable bound by
        the type signature for:
          catafilter :: forall a. (a -> Bool) -> [a] -> [a]
        at src/cata.hs:3:1-39
    • In the first argument of ‘p’, namely ‘x’
      In the expression: (p x)
      In the expression: if (p x) then x : xs else xs
    • Relevant bindings include
        xs :: [a1] (bound at src/cata.hs:8:18)
        x :: a1 (bound at src/cata.hs:8:16)
        alg :: ListF a1 [a1] -> [a1] (bound at src/cata.hs:7:5)
        p :: a -> Bool (bound at src/cata.hs:4:12)
        catafilter :: (a -> Bool) -> [a] -> [a] (bound at src/cata.hs:4:1)
  |
8 |     alg  (Cons x xs) = if (p x) then x : xs else xs
  |                              ^

The answer to the SO question type-signature-in-a-where-clause suggests to use the ScopedTypeVariables extension. The comment in the last answer to why-is-it-so-uncommon-to-use-type-signatures-in-where-clauses suggests to use a forall quantification.

So I added:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}

at the top of my module and tried different type signatures for alg like: alg :: forall a. ListF a [a] -> [a] or alg :: forall b. ListF b [b] -> [b] or adding a forall to the catalist type signature. Nothing compiled!

Question: Why I'm not able to specify a type signature for alg?

Answer 1

Without extensions, the original uncommented code

catafilter :: (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg 
  where
    alg :: ListF a [a] -> [a]
    alg  Nil  =  []
    alg  (Cons x xs) = if (p x) then x : xs else xs

is equivalent, after enabling ScopedTypeVariables, to explicitly quantifying all the type variables, as follows:

catafilter :: forall a. (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg 
  where
    alg :: forall a. ListF a [a] -> [a]
    alg  Nil  =  []
    alg  (Cons x xs) = if (p x) then x : xs else xs

This in turn is equivalent to (by alpha converting the quantified variables)

catafilter :: forall a. (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg 
  where
    alg :: forall b. ListF b [b] -> [b]
    alg  Nil  =  []
    alg  (Cons x xs) = if (p x) then x : xs else xs

and this triggers a type error since p wants an a argument, but p x passes a b argument.

The point is, with the extension enabled, a function starting with forall b. ... is promising that it can work with any choice of b. This promise is too strong for alg, which only works on the same a of catafilter.

So, the solution is the following. The type of catafilter can promise to work with any a its caller might choose: we can add forall a. there. Instead, alg must promise only to work with the same a of catafilter, so we reuse the type variable a without adding another forall.

catafilter :: forall a. (a -> Bool) -> [a] -> [a] 
catafilter p = cata alg 
  where
    alg :: ListF a [a] -> [a]
    alg  Nil  =  []
    alg  (Cons x xs) = if (p x) then x : xs else xs

this compiles since ScopedTypeVariables sees that a is in scope, and does not add an implicit forall in alg (as it would happen without th extension).

Summary:

• Without ScopedTypeVariables, every type annotation has its own implicit forall ... on top, quantifying all the variables. No annotation can refer to variables of other annotations (you can reuse the same name, but it is not considered the same variable).
• With ScopedTypeVariables, the definition foo :: forall t. T t u ; foo = def is handled as follows:
  • the type variable t is universally quantified and brought in scope when type checking def: type annotations in def can refer to t
  • the type variable u, if currently in scope, refers to the externally defined u
  • the type variable u, if not in scope, is universally quantified but not brought in scope when type checking def (for compatibility, here we follow the same behavior without the extension)