Parametricity Tutorial: Contravariant functions

Contravariant functors

Contravariant functors, are defined in the contravariant package

class Contravariant f where
  contramap :: (a -> b) -> f b -> f a

The contravariant functor characterization

For cofunctions we can state a similar characterization as we did for (covariant) functors:

Characterization: Contravariant Functors.

Let F be a contravariant functor. Then for all relations a :: A ⇔ A', b :: B ⇔ B and functions f :: A -> B, f' :: A' -> B' such that f ℛ(a -> b) f':

forall xs :: F B, xs' :: F B'.
  if    xs ℛ(F b) xs'
  then  F f xs ℛ(F a) F f' xs'

Example

Let’s see an example. Let’s define

data F a = F (a -> Int)

instance Contravariant F where
  contramap f (F g) = F (g . f)

Let’s check that the contravariant functor characterization holds.

     forall xs :: F B, xs' :: F B'.
            xs ℛ(F b) xs'
       iff  F f xs ℛ(F a) F f' xs'
-- Unfolding defininitions
iff  forall g :: B -> Int, g' :: B' -> Int.
       if    g ℛ(b -> Int) g'
       then  (g . f) ℛ(a -> Int) (g' . f')

We can complete the proof at this point without getting lost in technical detail: the premise g ℛ(b -> Int) g' states that g and g' map b-related arguments to the same integer. We have to show that (g . f) and (g' . f') map a-related arguments to the same integer, which follows from the assumption that f and f' map a-related arguments to b-related arguments.

Respecting Contravariant

What does it mean for a relation f :: F ⇔ F' to “respect” Contravariant?

     contramap ℛ(∀ab. (a -> b) -> f b -> f a) contramap
-- Rule for polymorphism, twice
iff  forall A, A', a :: A ⇔ A', B, B', b :: B ⇔ B'.
        contramap@A,B ℛ((a -> b) -> f b -> f a) contramap@A',B'
-- Rule for functions, twice
iff  forall A, A', a :: A ⇔ A', B, B', b :: B ⇔ B'.
     forall g :: A -> B, g' :: A' -> B', xs :: F B, xs' :: F' B'.
        if    g ℛ(a -> b) g', xs ℛ(f b) xs'
        then  contramap g xs ℛ(f a) contramap g' xs'

Specializing to higher order functions

Let h :: F -> F' be a higher order function between F and F'; that is

h :: ∀ab. (a -> b) -> F a -> F' b

What does it mean for such a function h to respect contravariant?

iff  forall A, A', a :: A ⇔ A', B, B', b :: B ⇔ B'.
     forall g :: A -> B, g' :: A' -> B', xs :: F B, xs' :: F' B'.
        if    g ℛ(a -> b) g', xs ℛ(h b) xs'
        then  contramap g xs ℛ(h a) contramap g' xs'

As before, since this is a proof obligation it does not suffice to consider functions a and b, but we really have to consider the more general case with relations a and b.

But, as before, we can derive a useful special case. Let k :: forall a. F a -> F' a be some arbitrary polymorphic function, and define the relational action h by

h(b) = k ⚬ F(b)

where we use k also as a relation. Then

     xs ℛ(h b) xs'
iff  ∃i. xs ℛ(k) i and i ℛ(F(b)) xs'
-- k is a function
iff  k xs ℛ(F b) xs'
-- by the Contravariant Functor Characterization
iff  F g (k xs) ℛ(F a) F g' xs'
-- naturality
iff  k (F g xs) ℛ(F a) F g' xs'
-- use k as a relation again
iff  F g xs ℛ(k) k (F g xs) ℛ(F a) F g' xs'
-- pick k (F g xs) as the intermediate
then F g xs ℛ(h a) F g' xs'
-- if we assume that contramap is the "real" Contravariant instance
iff  contramap g xs ℛ(h a) contramap g' xs'

This means that any relational action h defined above automatically respect Contravariant, which makes it possible to derive special cases of various theorems in terms of polymorphic functions (with no side conditions), just like we did for functors.