|
|
Пишет Journal de Chaource (![[info]](http://lj.rossia.org/img/syndicated.gif){kind=small} lj_chaource)@ 2018-10-09 23:37:00 |
 |
|
 |
|
|
|
|
|
|
 |
|
 |
Adjoint functors in functional programming (Выхожу изъ тюрьмы, политикой не занимаюсь...)
I've gone through a study group based on the series of blog posts on category theory for programmers. These blog posts are fascinating but not equally well adapted to programmer's needs. There are lots of books with expositions of various notions of category theory, but I'd like to see some program code that can be written after understanding this or that notion. Preferably, code should be "interesting" in the sense that one wouldn't be able to write that code without keeping category theory in mind. Indeed, interesting code follow from many constructions of category theory, such as Yoneda lemma or Kleisli categories. If category theory is "abstract nonsense", I'd like to see "concrete nonsense" instead.
One of the chapters of Milewski's blog is about adjunctions. Here's what I got out of it in terms of code.
Because programmers most often work in a category whose objects are types in the chosen programming language, an endofunctor will be a "type constructor" (i.e. a function from types to types). So, most of the time programmers will work with endofunctors (but call them "functors" for short).
This situation is actually quite similar to the relationship between the terminology in theoretical physics and mathematics. https://posic.livejournal.com/1833813.ht
Back to coding. Given a functor F, we can construct the left adjoint functor L(F) and the right adjoint functor R(F) using the so called "Kan extensions" or "ends" / "coends". Omitting all details about those constructions, the program code defining the types for L(F) and R(F) will look like this,
L(F) a ≡ ∀ i. (a -> F i) -> i
R(F) a ≡ ∃ i. i × (F i -> a)
The Yoneda and co-Yoneda lemmas mean that the adjoints of an identity functor is identity:
∀ i. (a -> i) -> i = a
∃ i. i × (i -> a) = a
Using these formulas, as well as the standard identities of functional type theory, such as
a × b -> z = a -> b -> z = a -> (b -> z)
z -> a × b = (z -> a) × (z -> b)
a = 1 -> a
a + b -> z = (a -> z) × (b -> z)
we can explicitly compute adjoints for some simple functors such as F a = z + a, F a = z × a, or F a = z -> a, etc.
Example 1.
An interesting example is F a = z + a. Let us compute the right adjoint, simplifying the resulting type constructor:
R(F) a = ∃ i. i × (z + i -> a) = ∃ i. i × (z -> a) × (i -> a) = a × (z -> a) = (1 + z) -> a
We can now compute the left adjoint of that:
L(R(F)) a = ∀ i. (a -> R(F) i) -> i = ∀ i. (a -> 1 + z -> i) -> i = ∀ i. (a × (1 + z) -> i) -> i = a × (1 + z)
Interestingly, the functor F has been changed from z + a to a × (1 + z) as we go in a circle from left to right adjoint and back. If we continue the same computation and again compute R() of this latest functor, we obtain again R(F) rather than a new functor:
R(L(R(F))) a = ∃ i. i × (i × (1 + z) -> a) = ∃ i. i × (i -> 1 + z -> a) = 1 + z -> a = R(F) a.
This is a curious situation. Starting with a functor F, we compute its right adjoint, then the left adjoint of that, then the right adjoint of that, etc., and we find that the sequence stabilizes.
Another interesting detail is that actually R(F) does not seem to be the correct right adjoint to F, because right adjoint implies the existence of a natural transformation F(R(F) a) -> a. But this natural transformation cannot exist for F a = z + a, because we cannot have a function of type z + ((1 + z) -> a) -> a.
However, once we have completed the circular computation, we obtain L(R(F)) and R(F), which admits the natural transformation L(R(F)) (R(F) a) -> a, of type
(1 + z -> a) × (1 + z) -> a =
a × (z -> a) × (1 + z) -> a.
To implement this transformation, we simply ignore the values of type (z -> a) × (1 + z).
We can show that a natural transformation L(R(F)) (R(F) a) -> a always exists for all F. Other properties of the adjunction will probably hold too.
Taking the left adjoint of F will actually not work:
L(F) a = ∀ i. (a -> z + i) -> i
because the resulting type is void: if we are given an arbitrary function of type a -> z + i, that function might always return z, and then we have no hope of producing any values of type i.
However, after "going full circle", L(L(R(F))) exists:
L(L(R(F))) a = ∀ i. (a -> i × (1 + z)) -> i = ∀ i. (a -> i) × (a -> 1 + z) -> i =
∀ i. (a -> 1 + z) -> (a -> i) -> i = (a -> 1 + z) -> a.
It appears that the "full circle" transformation, i.e. F -> L(R(F)) will automatically embellish a given functor with an additional structure necessary for the existence of adjoints. This is a very interesting construction because it is a canonically defined transformation of functors. Maybe it's even a functor of functors. And yet it yields nontrivial results, as in this example, transforming a + z into a × (1 + z). It is not obvious whether the transformed functor, viewed as a data structure in a programming language, is "better suited" for some applications. More examples are needed to see how to use this transformation.
Example 2.
Consider the functor F a = z × a and compute L(F) and R(F).
L(F) a = ∀ i. (a -> z × i) -> i = ∀ i. (a -> z) × (a -> i) -> i =
∀ i. (a -> z) -> (a -> i) -> i = (a -> z) -> a
R(F) a = ∃ i. i × (z × i -> a) = ∃ i. i × (i -> (z -> a)) = z -> a
Going "full circle" yields:
L(R(F)) a = ∀ i. (a -> (z -> i)) -> i = ∀ i. (a × z -> i) -> i = a × z = F a
No new functor is obtained via F -> L(R(F)). So, for this direction of adjunction, the "full circle" has been unnecessary. Consider the other direction:
R(L(F)) a = ∃ i. i × (((i -> z) -> i) -> a)
Now I'm actually not sure if this type can be simplified at all; it's weird because it's strictly positive in "a" but not strictly positive in "z", and there aren't such type expressions among the simple functors such as a × z. In any case, R(L(F)) is a new functor, not equivalent to F.
It seems that the only possible simplification is R(L(F)) a = ∃ i. i × ((z -> i) -> a), which works because we have an "i", and thus we have morphisms between z and i -> z. The loss of information due to hiding "i" is admissible because "i" is not observable anyway. But this simplification needs to be checked more rigorously.
I'm also not sure what these "embellished" functors mean, in terms of their use in programming. The main application of adjunctions so far is to construct monads and comonads, via the composition of two adjoint functors. Using the "full circle" transformation, we obtain a way of constructing monads and comonads as a "adjoint square" of an arbitrary functor F. It remains to be seen whether this construction is practically significant. Do the resulting monads and comonads retain some properties of the functor F? So far, we have seen that the functor F a = z + a would yield the state monad with the state type 1 + z. More examples are needed to clarify the relationship between F and the resulting monads.
I've gone through a study group based on the series of blog posts on category theory for programmers. These blog posts are fascinating but not equally well adapted to programmer's needs. There are lots of books with expositions of various notions of category theory, but I'd like to see some program code that can be written after understanding this or that notion. Preferably, code should be "interesting" in the sense that one wouldn't be able to write that code without keeping category theory in mind. Indeed, interesting code follow from many constructions of category theory, such as Yoneda lemma or Kleisli categories. If category theory is "abstract nonsense", I'd like to see "concrete nonsense" instead.
One of the chapters of Milewski's blog is about adjunctions. Here's what I got out of it in terms of code.
Because programmers most often work in a category whose objects are types in the chosen programming language, an endofunctor will be a "type constructor" (i.e. a function from types to types). So, most of the time programmers will work with endofunctors (but call them "functors" for short).
This situation is actually quite similar to the relationship between the terminology in theoretical physics and mathematics. https://posic.livejournal.com/1833813.ht
Back to coding. Given a functor F, we can construct the left adjoint functor L(F) and the right adjoint functor R(F) using the so called "Kan extensions" or "ends" / "coends". Omitting all details about those constructions, the program code defining the types for L(F) and R(F) will look like this,
L(F) a ≡ ∀ i. (a -> F i) -> i
R(F) a ≡ ∃ i. i × (F i -> a)
The Yoneda and co-Yoneda lemmas mean that the adjoints of an identity functor is identity:
∀ i. (a -> i) -> i = a
∃ i. i × (i -> a) = a
Using these formulas, as well as the standard identities of functional type theory, such as
a × b -> z = a -> b -> z = a -> (b -> z)
z -> a × b = (z -> a) × (z -> b)
a = 1 -> a
a + b -> z = (a -> z) × (b -> z)
we can explicitly compute adjoints for some simple functors such as F a = z + a, F a = z × a, or F a = z -> a, etc.
Example 1.
An interesting example is F a = z + a. Let us compute the right adjoint, simplifying the resulting type constructor:
R(F) a = ∃ i. i × (z + i -> a) = ∃ i. i × (z -> a) × (i -> a) = a × (z -> a) = (1 + z) -> a
We can now compute the left adjoint of that:
L(R(F)) a = ∀ i. (a -> R(F) i) -> i = ∀ i. (a -> 1 + z -> i) -> i = ∀ i. (a × (1 + z) -> i) -> i = a × (1 + z)
Interestingly, the functor F has been changed from z + a to a × (1 + z) as we go in a circle from left to right adjoint and back. If we continue the same computation and again compute R() of this latest functor, we obtain again R(F) rather than a new functor:
R(L(R(F))) a = ∃ i. i × (i × (1 + z) -> a) = ∃ i. i × (i -> 1 + z -> a) = 1 + z -> a = R(F) a.
This is a curious situation. Starting with a functor F, we compute its right adjoint, then the left adjoint of that, then the right adjoint of that, etc., and we find that the sequence stabilizes.
Another interesting detail is that actually R(F) does not seem to be the correct right adjoint to F, because right adjoint implies the existence of a natural transformation F(R(F) a) -> a. But this natural transformation cannot exist for F a = z + a, because we cannot have a function of type z + ((1 + z) -> a) -> a.
However, once we have completed the circular computation, we obtain L(R(F)) and R(F), which admits the natural transformation L(R(F)) (R(F) a) -> a, of type
(1 + z -> a) × (1 + z) -> a =
a × (z -> a) × (1 + z) -> a.
To implement this transformation, we simply ignore the values of type (z -> a) × (1 + z).
We can show that a natural transformation L(R(F)) (R(F) a) -> a always exists for all F. Other properties of the adjunction will probably hold too.
Taking the left adjoint of F will actually not work:
L(F) a = ∀ i. (a -> z + i) -> i
because the resulting type is void: if we are given an arbitrary function of type a -> z + i, that function might always return z, and then we have no hope of producing any values of type i.
However, after "going full circle", L(L(R(F))) exists:
L(L(R(F))) a = ∀ i. (a -> i × (1 + z)) -> i = ∀ i. (a -> i) × (a -> 1 + z) -> i =
∀ i. (a -> 1 + z) -> (a -> i) -> i = (a -> 1 + z) -> a.
It appears that the "full circle" transformation, i.e. F -> L(R(F)) will automatically embellish a given functor with an additional structure necessary for the existence of adjoints. This is a very interesting construction because it is a canonically defined transformation of functors. Maybe it's even a functor of functors. And yet it yields nontrivial results, as in this example, transforming a + z into a × (1 + z). It is not obvious whether the transformed functor, viewed as a data structure in a programming language, is "better suited" for some applications. More examples are needed to see how to use this transformation.
Example 2.
Consider the functor F a = z × a and compute L(F) and R(F).
L(F) a = ∀ i. (a -> z × i) -> i = ∀ i. (a -> z) × (a -> i) -> i =
∀ i. (a -> z) -> (a -> i) -> i = (a -> z) -> a
R(F) a = ∃ i. i × (z × i -> a) = ∃ i. i × (i -> (z -> a)) = z -> a
Going "full circle" yields:
L(R(F)) a = ∀ i. (a -> (z -> i)) -> i = ∀ i. (a × z -> i) -> i = a × z = F a
No new functor is obtained via F -> L(R(F)). So, for this direction of adjunction, the "full circle" has been unnecessary. Consider the other direction:
R(L(F)) a = ∃ i. i × (((i -> z) -> i) -> a)
Now I'm actually not sure if this type can be simplified at all; it's weird because it's strictly positive in "a" but not strictly positive in "z", and there aren't such type expressions among the simple functors such as a × z. In any case, R(L(F)) is a new functor, not equivalent to F.
It seems that the only possible simplification is R(L(F)) a = ∃ i. i × ((z -> i) -> a), which works because we have an "i", and thus we have morphisms between z and i -> z. The loss of information due to hiding "i" is admissible because "i" is not observable anyway. But this simplification needs to be checked more rigorously.
I'm also not sure what these "embellished" functors mean, in terms of their use in programming. The main application of adjunctions so far is to construct monads and comonads, via the composition of two adjoint functors. Using the "full circle" transformation, we obtain a way of constructing monads and comonads as a "adjoint square" of an arbitrary functor F. It remains to be seen whether this construction is practically significant. Do the resulting monads and comonads retain some properties of the functor F? So far, we have seen that the functor F a = z + a would yield the state monad with the state type 1 + z. More examples are needed to clarify the relationship between F and the resulting monads.
