# Parametricity Tutorial: Contravariant functions

all coding

## 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.