Adjoint functors in functional programming II. Polynomial functors
Выхожу изъ тюрьмы, политикой не занимаюсь... Гляжу - Трампъ подписалъ новый законъ о копирайтѣ. Тутъ одинъ такой въ штатскомъ подходитъ и спрашиваетъ - вы не слышали, а что это за законъ Трампъ подписалъ. Я говорю - кому надо, тому и подписалъ... Выхожу изъ тюрьмы, политикой не занимаюсь...

In a programmer's language, a "category" is "cartesian closed category with a final object".

In Part I I showed that some adjunctions are obtained via the "adjunction completion". However, it remains unclear which functors have non-void completions.

To gather intuition, I limited my consideration to polynomial functors F and their transformations L(F) and R(F), defined by

L(F) a ≡ ∀ i. (a -> F i) -> i

R(F) a ≡ ∃ i. i × (F i -> a)


Polynomial functors are generally of the form

F a = c_0 + c_1 × a + c_2 × a × a + ... + c_N × a × ... × a.

We can rewrite this identically as

F a = c_0 + c_1 × a + c_2 × (2 -> a) + ... + c_N × (N -> a).

Here by "2", ..., "N" we denote the types 1 + 1, ..., 1 + ... + 1, and we use the standard identities

1 -> a = a
x + y -> a = (x -> a) × (y -> a)

The first remark is that L(F) is void for F x = c + G x for any G and a constant type c. Indeed:

L(F) a = ∀ i. (a -> c_0 + G i) -> i

This type is void (i.e. L(F) a = 0) since it cannot produce an arbitrary "i" from a function of type a -> c_0 + G i, which might return always a "c_0", with no hope of getting any values of type "i". More formally, we may substitute i = 0 into ∀ i. (a -> F i) -> i and get (a -> F 0) -> 0. If the constant type a -> F 0 is not void, say it is equal to some b ≠ 0, we have

L(F) a = b -> 0 = 0.

Therefore, L(F) is not void only when F 0 = 0, which means c_0 must be absent (c_0 = 0) and the functor F must have the form

F a = (k -> a) × (c_k + G a)

for some functor G and some natural k ≠ 0.

Substituting this F into L(F), we find

L(F) a = ∀ i. (a -> (k -> i) × (c_k + G i)) -> i = ∀ i. (k × a -> i) × (a -> c_k + G i) -> i.

How could we implement a value of this type? One of the arguments is a function of type a -> c_k+ G i. This function could always return c_k for all "a", and so it can't be helpful for computing an "i". Therefore, all implementations of L(F) a must be functions that ignore the argument of type a -> c_k + G i. But then these implementations are equivalent to implementations of the type ∀ i. (k × a -> i) -> i, which is equivalent to just k × a.

Therefore, L(F) a = k × a where k is the lowest available power of "a" in the polynomial F. If that power is zero, we have L(F) a = 0.

Viewed as a function on polynomials, L(F) a = a × (d ln F(x) / d ln x) at x = 0.

Consider now R(F). By definition,

R(F) a = ∃ i. i × (F i -> a) = ∃ i. i × ( (c_0 + c_1 × i + c_2 × (2 -> i) + ... + c_N × (N -> i) ) -> a)

If we could simplify this into the form ∃ i. i × (i -> Q a) for some functor Q, we would obtain R(F) a = Q a.

We have

( c_0 + c_1 × i + c_2 × (2 -> i) + ... + c_N × (N -> i) ) -> a =
(c_0 -> a) × (c_1 × i -> a) × (c_2 × (2 -> i) -> a) × ... =
(c_0 -> a) × (i -> c_1 -> a) × ((2 -> i) -> c_2 -> a) × ...

We have the product of all terms of the form (k -> i) -> c_k -> a for all k from 0 to N.
Each of these terms can be simplified as (k -> i) -> c_k -> a = (i × ... × i) -> (c_k -> a).
Consider what an implementation of this type must look like. It is a function that produces c_k -> a out of "k" copies of i. Since all these copies have the same type "i", the code of that function will work if given just one copy of "i". Also note that the type contains only one fixed value of type "i" as ∃ i. i × (...), so all copies of "i" will have the same value when substituted into the function (i × ... × i) -> (c_k -> a). Therefore, the type is equivalent to that where we only have one copy of "i" in each term, i -> (c_k -> a). Hence

R(F) a = ∃ i. i × (c_0 -> a) × (i -> c_1 -> a) × (i -> c_2 -> a) × ...
= (c_0 -> a) × ∃ i. i × (i -> (c_1 -> a) × (c_2 -> a) × ... × (c_N -> a))
= (c_0 -> a) × ... × (c_N -> a) = c_0 + c_1 + ... + c_N -> a.

Viewed as a function on polynomials, R(F) a = (F 1) -> a.

Now it is clear that computing L(R(F)), L(R(L(R(F)))), ... will yield a looping sequence after the first iteration, when F is a polynomial functor.

If we first compute L(F) then we will always obtain a linear functor, L(F) a = a × k, for some natural-number constant "k". Computing R(L(F)) yields k -> a, which is a monomial of degree "k". Computing L() of that polynomial will again yield a × k.

If we first compute R(F) then we will always obtain a functor of the form c -> a for some constant type c = F(1). Computing L(c -> a) yields c × a. Evaluating this at a = 1 will give "c", so R(L(c -> a)) is again c -> a.

The conclusion is that the transformations L() and R() will always modify polynomial functors into functors F of the form c × a and c -> a for some constant types "c". These two functors are adjoint. But the original functors F may not have an adjoint, at least among the endofunctors.