2 ms·
A slightly more concrete version of this is data Predicate a = Predicate (a -> Bool) this naturally has a contravariant functor instance: if you can tell
by bollu 6y ago
A slightly more concrete version of this is
data Predicate a = Predicate (a -> Bool)
this naturally has a contravariant functor instance: if you can tell me whether something is true for "a", and you can convert "b -> a", then how do you tell me whether something is true for "b"? Convert the "b" to an "a" and see if it's true for "a".
Formally, you get the instance
contramap :: (b -> a) -> Predicate a -> Predicate b
contramap :: (b -> a) -> (a -> Bool) -> (b -> Bool)
The picture to have in mind is to imagine A as a space, and then to know that some things are true in A (color them green) while others are false (color them red). If you now want to color another space B using this space A, should you have A -> B, or B -> A?
some thought reveals that A -> B may tell us inconsistent colourings. For example, say we have a map {red, green} -> { b } where both "red" and "green" map to "b". So what color do we assign "b"? There is no reasonable choice.
On the other hand, say we have a function B -> A. Since each element in b maps to one element of A, we can say
color(b) = color of element that b maps to.
We need the fact that a function maps one value in the domain to exactly one value in the codomain for this to work.
I tend to imagine the function from B to A as threads, whose endpoints in A are soaked with dye. This dye "moves backwards" towards B. The uniqueness in colors assigned to B is given by the fact that we can only have one thread from each point in B.