The following function implements the good old filter function from lists by using the recursionschemes 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:529
‘a’ is a rigid type variable bound by
the type signature for:
catafilter :: forall a. (a > Bool) > [a] > [a]
at src/cata.hs:3:139
• 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 typesignatureinawhereclause suggests to use the ScopedTypeVariables extension. The comment in the last answer to whyisitsouncommontousetypesignaturesinwhereclauses 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?
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:
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).ScopedTypeVariables
, the definition foo :: forall t. T t u ; foo = def
is handled as follows:
t
is universally quantified and brought in scope when type checking def
: type annotations in def
can refer to t
u
, if currently in scope, refers to the externally defined u
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)