haskellghcrecursion-schemescatamorphism

Specifying a function type signature in a where clause

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?

Solution

  • 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: