Exponential-polynomial functors, contrafunctors, and profunctors We are working in a Cartesian closed category, so that for any objects A and B we have A+B, A*B, and A->B. The "exponential type" A->B represents, for functional programming, the type of functions that take the (single) argument of type A and return a value of type B.
Exponential-polynomial ("exp-poly") type constructor is either
- a constant functor, F(t) = c for some fixed type c independent of t,
- the identity functor, F(t) = t,
- the product F * G of two exp-poly type constructors F and G,
- the co-product F + G of two exp-poly type constructors F and G,
- the exponential F -> G of two exp-poly type constructors F and G.
The algebraic notation for s->t is the "exponential" t
s. This is suggestive of algebraic identities such as
t
1 = t
t
0 = 1
(ab)
c = (a
c)(b
c)
a
(b+c) = (a
b)(a
c)
(a
b)
c = a
(bc)All these identities are also valid as isomorphisms of types. For example, 1 -> t is isomorphic to t, 0 -> t is isomorphic to 1 (there is a unique map 0->t for every t), etc.
However, exponential notation is limited: for instance, identities for 1
a or 0
a do not exist. So I will use the type theory/logic notation, a->b, for exponential type constructors.
Functors and contrafunctorsA type constructor F(t) is a functor when for every f: t->s we have fmap(f): F(t)->F(s) that satisfies suitable properties with respect to identity and composition. A contrafunctor has the reverse direction of the last arrow: for every f: t->s we have contrafmap(f): F(s)->F(t).
Unlike polynomial type constructors, which are always functors, exponential type constructors may be functors, contrafunctors, or neither. This is determined by the "covariance" of the type constructors with respect to their type variables.
Definition. An exponential-polynomial type constructor F(t) is
covariant in the argument t if one of the following holds:
- F(t) is any polynomial type constructor with respect to t.
- F(t) = A(t) -> B(t) where A(t) is contravariant in t and B(t) is covariant in t.
- F(t) = A(t)+B(t) or F(t) = A(t)*B(t) where A(t) and B(t) are covariant in t.
A type constructor F(t) is
contravariant in t if one of the following holds:
- F(t) = c (a constant, independent of t)
- F(t) = A(t) -> B(t) where A(t) is covariant and B(t) is contravariant in t.
- F(t) = A(t)+B(t) or F(t) = A(t)*B(t) where A(t) and B(t) are contravariant in t.
Each time the argument t is used in a function argument, its variance is flipped from co- to contravariant or back. So t-> c is contravariant in t, (t->c)->c is again covariant in t, etc.
Examples of covariant type constructors:
F(t) = 1+t*t*t
F(t) = 1+c -> 1+t
F(t) = c -> t*t
F(t) = (t -> c) -> t
F(t) = (t*t*t*c -> t -> c) -> t*t + (c->t)
Examples of contravariant type constructors:
F(t) = 1 + c (note that a constant type constructor is both covariant and contravariant)
F(t) = 1+t -> 1+c
F(t) = (c->t) -> (t->c)
F(t) = t*t*(c->t) -> (c->t) -> c
Examples of type constructors that are neither co- nor contravariant because "t" is used in both covariant and contravariant positions:
F(t) = t->t
F(t) = (c->t) -> t
F(t) = (c->t)*(t->c)
These type constructors are called
profunctors.
Definition. A type constructor F(t) is a
profunctor if for any f: t->s and g: s->t there is dimap(f,g): F(t)->F(s).
It is clear that functors are also profunctors, and contrafunctors are also profunctors.
We can show that exp-poly type constructors are functors precisely when they are covariant, contrafunctors precisely when they are contravariant, and that they are always profunctors.
Statement. An exp-poly type constructor is a functor if it is covariant, and a contrafunctor if it is contravariant. Any exp-poly type constructor F(t) (including those that contain "t" in both covariant and contravariant positions) is a profunctor.
Proof. We proceed by induction on the structure of F(t). The cases of polynomial or constant F(t), as well as F(t)=A+B, F(t)=A*B are straightforward. Consider the case of the exponential F(t) = A(t)->B(t). We assume that A(t) has been already shown to be a contrafunctor and B(t) has been shown to be a functor. So for any given f: t->s, we may assume that we already have fmap
A(f): A(s)->A(t) and contrafmap
B(f):B(t)->B(s), and we now need to construct fmap
F(f): F(t)->F(s) = (A(t)->B(t))->(A(s)->B(s)). This is straightforward: fmap
F(f) (g:A(t)->B(t)) = fmap
A(f) . g . contrafmap
B(f). The proof for contrafunctors and profunctors is similar.
So, we can say "exp-poly profunctor" instead of "exp-poly type constructor", without loss of generality.