# Parametricity Tutorial: Contravariant functions

(Not yet published), by Edsko de Vries.

Filed under 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.