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)

Answer 2

This works

{-# Language ScopedTypeVariables #-}

import Data.Functor.Foldable 

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

---

If you omit the forall, these are completely different as (even though syntactically they are the same).

Because of implicit quantification, your uncommented version is taken to be

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

This explains your error message:

Couldn't match expected type ‘a’ with actual type ‘a1’

The predicate (p :: a -> Bool) expects an argument of type a but it was given x :: a1 from Cons x xs :: ListF a1 [a1]!

See if the explicitly quantified version makes sense given the bindings from the error message:

xs         :: [a1] 
x          :: a1
alg        :: ListF a1 [a1] -> [a1] 
p          :: a -> Bool 
catafilter :: (a -> Bool) -> [a] -> [a]

Answer 3

This works, and avoids all that counter-intuitive mucking around with foralls

{-# LANGUAGE ScopedTypeVariables #-}

import Data.Functor.Foldable 

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

On the alg Nil equation I could actually use tyvar a: I used aa merely to show they're distinct bindings. Because aa appears on a pattern, the compiler unifies it with a from the signature for catafilter.

You could also/instead put the type annotations on the alg Cons equation.

I understand @Jogger's confusion as to why ghc is so fussy about the position of the forall; and the nervousness that a forall perhaps indicates RankNTypes.

Answer 4

The problem is that alg depends on an external p, so alg's type can't be simply polymorphic.

One simple way around it is to make it independent of any external entities by passing them in as the function arguments, so that the function can have its simply polymorphic type as expected:

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

This doesn't need any language extensions.