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.
Fbe a contravariant functor. Then for all relations
a :: A ⇔ A',
b :: B ⇔ Band 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'
Let’s see an example. Let’s define
data F a = F (a -> Int) instance Contravariant F where F g) = F (g . f) contramap f (
Let’s check that the contravariant functor characterization holds.
forall xs :: F B, xs' :: F B'. F b) xs' xs ℛ(F f xs ℛ(F a) F f' xs' iff -- Unfolding defininitions forall g :: B -> Int, g' :: B' -> Int. iff 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
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
a-related arguments to
What does it mean for a relation
f :: F ⇔ F' to “respect”
∀ab. (a -> b) -> f b -> f a) contramap contramap ℛ(-- Rule for polymorphism, twice forall A, A', a :: A ⇔ A', B, B', b :: B ⇔ B'. iff @A,B ℛ((a -> b) -> f b -> f a) contramap@A',B' contramap-- Rule for functions, twice forall A, A', a :: A ⇔ A', B, B', b :: B ⇔ B'. iff 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
h :: F -> F' be a higher order function between
F'; that is
h :: ∀ab. (a -> b) -> F a -> F' b
What does it mean for such a function
h to respect contravariant?
forall A, A', a :: A ⇔ A', B, B', b :: B ⇔ B'. iff 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
b, but we really have to consider the more general case with relations
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
= k ⚬ F(b)h(b)
where we use
k also as a relation. Then
xs ℛ(h b) xs'∃i. xs ℛ(k) i and i ℛ(F(b)) xs' iff -- k is a function F b) xs' iff k xs ℛ(-- by the Contravariant Functor Characterization F g (k xs) ℛ(F a) F g' xs' iff -- naturality F g xs) ℛ(F a) F g' xs' iff k (-- use k as a relation again F g xs ℛ(k) k (F g xs) ℛ(F a) F g' xs' iff -- 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.