|
|
Пишет Journal de Chaource (![[info]](http://lj.rossia.org/img/syndicated.gif){kind=small} lj_chaource)@ 2017-03-11 07:53:00 |
 |
|
 |
|
|
|
|
|
|
 |
|
 |
Exponential-polynomial applicative functors
Applicative functors (also known as monoidal functors) are among the most useful constructions in functional programming. They represent data containers whose elements can be combined with elements from other containers of the same shape. Alternatively, applicative functors can be seen as holding "values in a context" such that two independent contexts can be combined via a monoidal operation. The main property that makes this possible is the distributivity with respect to the product:
A s × A t ~> A (s × t).
The second property required of applicative functors is the "point" transformation: Id ~> A.
These transformations should commute and satisfy the obvious associativity properties.
Exp-polynomial functors are easy to visualize: they are data types built using products, sums, and function types. Which exp-polynomial functors are applicative?
Lemma A. Functors built recursively using any of the following 5 rules are applicative:
1. Constant functor A t = c where c is a monoid type (having a selected "zero" value pointed by 1 -> c and a binary operation c × c -> c)
2. Identity functor A t = t
3. Product of two applicative functors: F t = A t × B t
4. Sum of an applicative functor and identity functor: F t = A t + t
5. Function from a distributive contrafunctor to an applicative functor: F t = C t -> A t. A contrafunctor C is distributive if there exists a natural transformation C(s × t) ~> C s × C t with the obvious associativity property.
It remains to be seen whether there exist other subsets of exp-polynomial functors that are either applicative or monadic but are not covered by the constructions shown above.
Applicative functors (also known as monoidal functors) are among the most useful constructions in functional programming. They represent data containers whose elements can be combined with elements from other containers of the same shape. Alternatively, applicative functors can be seen as holding "values in a context" such that two independent contexts can be combined via a monoidal operation. The main property that makes this possible is the distributivity with respect to the product:
A s × A t ~> A (s × t).
The second property required of applicative functors is the "point" transformation: Id ~> A.
These transformations should commute and satisfy the obvious associativity properties.
Exp-polynomial functors are easy to visualize: they are data types built using products, sums, and function types. Which exp-polynomial functors are applicative?
Lemma A. Functors built recursively using any of the following 5 rules are applicative:
1. Constant functor A t = c where c is a monoid type (having a selected "zero" value pointed by 1 -> c and a binary operation c × c -> c)
2. Identity functor A t = t
3. Product of two applicative functors: F t = A t × B t
4. Sum of an applicative functor and identity functor: F t = A t + t
5. Function from a distributive contrafunctor to an applicative functor: F t = C t -> A t. A contrafunctor C is distributive if there exists a natural transformation C(s × t) ~> C s × C t with the obvious associativity property.
Proof. The "point" transformations are easy to find for each case. Therefore we concentrate on the distributivity.
1. The constant functor is applicative because c × c ~> c and 1 ~> c are available (by assumption that c is a monoid type).
2. The identity functor is trivially applicative.
3. The product is applicative because of the type isomorphism A s × B s × A t × B t = A s × A t × B s × B t, which allows us now to use the applicative transformations for A and B.
4. Adding the identity functor does not present difficulties since (A s + s)×(A t + t) can be decomposed into the sum of four terms,
A s × A t + s × A t + A s × t + s × t.
For any functor A we have p × A q ~> A(p × q). Therefore, each term of the sum above can be mapped to A(s × t) + s × t.
5. We need to produce a natural transformation
(C s -> A s) × (C t -> A t) ~> C (s × t) -> A (s × t).
We can curry this into (C s -> A s) × (C t -> A t) × C (s × t) ~> A (s × t).
By assumption, we have C(s × t) ~> C s × C t. Hence, we can produce values of types A s and A t. Finally, we use the distributivity of A to obtain A (s × t).
Q.E.D.
Examples of exp-polynomial applicative functors:
A t = t*t*t.
A t = <any polynomial functor with monoid coefficients> since such a polynomial functor can be constructed from rules 1-4.
A t = a -> t where a is a fixed type (not necessarily a monoid type). This is so since the constant functor S t = a is a contrafunctor (as well as a functor).
A t = (t -> a) -> b -> t.
An example of exp-polynomial functors that are not applicative is a sum of two exp-poly functors that do not satisfy rule 4 in Lemma A. For instance, the functor
F t = (b -> t) + (c -> t),
where b and c are fixed types, is not applicative -- even though both b -> t and c -> t are applicative.
To see that F t is not applicative, let us try to produce a natural transformation F s × F t ~> F (s × t):
(b ->s + c -> s)×(b ->t + c -> t) ~> (b -> s × t) + (c -> s × t).
We should be able to map any of the summands in the left-hand side into one of the summands in the right-hand side.
For instance, we should be able to map (b -> s)×(c -> t) either into a function of type b -> s × t or into a function of type c -> s × t. This is obviously impossible, since e.g. b -> s × t does not give us any values of type c, which we need in order to produce any value of type t.
The subset of exp-polynomial functors that are applicative is somewhat similar to the exp-polynomial functors that are monadic; except that monadic exp-poly functors do not require constant types to be monoids or the contrafunctor C to be distributive. However, there is one more way of building an exp-polynomial applicative functor that monads do not allow:
Statement. If A and B are applicative functors, and additionally if B is A-modular, then the functor F t = A t + B t is applicative.
A functor B is A-modular if there exists a natural transformation A s × B t ~> B(s × t) with the obvious associativity property.
Proof. We need to transform F s × F t ~> F (s × t):
(A s + B s) × (A t + B t) ~> A (s × t) + B(s × t).
Transforming A s × A t is easy. To transform terms such as A s × B t, we use the modularity property to get B(s × t).
Q.E.D.
1. The constant functor is applicative because c × c ~> c and 1 ~> c are available (by assumption that c is a monoid type).
2. The identity functor is trivially applicative.
3. The product is applicative because of the type isomorphism A s × B s × A t × B t = A s × A t × B s × B t, which allows us now to use the applicative transformations for A and B.
4. Adding the identity functor does not present difficulties since (A s + s)×(A t + t) can be decomposed into the sum of four terms,
A s × A t + s × A t + A s × t + s × t.
For any functor A we have p × A q ~> A(p × q). Therefore, each term of the sum above can be mapped to A(s × t) + s × t.
5. We need to produce a natural transformation
(C s -> A s) × (C t -> A t) ~> C (s × t) -> A (s × t).
We can curry this into (C s -> A s) × (C t -> A t) × C (s × t) ~> A (s × t).
By assumption, we have C(s × t) ~> C s × C t. Hence, we can produce values of types A s and A t. Finally, we use the distributivity of A to obtain A (s × t).
Q.E.D.
Examples of exp-polynomial applicative functors:
A t = t*t*t.
A t = <any polynomial functor with monoid coefficients> since such a polynomial functor can be constructed from rules 1-4.
A t = a -> t where a is a fixed type (not necessarily a monoid type). This is so since the constant functor S t = a is a contrafunctor (as well as a functor).
A t = (t -> a) -> b -> t.
An example of exp-polynomial functors that are not applicative is a sum of two exp-poly functors that do not satisfy rule 4 in Lemma A. For instance, the functor
F t = (b -> t) + (c -> t),
where b and c are fixed types, is not applicative -- even though both b -> t and c -> t are applicative.
To see that F t is not applicative, let us try to produce a natural transformation F s × F t ~> F (s × t):
(b ->s + c -> s)×(b ->t + c -> t) ~> (b -> s × t) + (c -> s × t).
We should be able to map any of the summands in the left-hand side into one of the summands in the right-hand side.
For instance, we should be able to map (b -> s)×(c -> t) either into a function of type b -> s × t or into a function of type c -> s × t. This is obviously impossible, since e.g. b -> s × t does not give us any values of type c, which we need in order to produce any value of type t.
The subset of exp-polynomial functors that are applicative is somewhat similar to the exp-polynomial functors that are monadic; except that monadic exp-poly functors do not require constant types to be monoids or the contrafunctor C to be distributive. However, there is one more way of building an exp-polynomial applicative functor that monads do not allow:
Statement. If A and B are applicative functors, and additionally if B is A-modular, then the functor F t = A t + B t is applicative.
A functor B is A-modular if there exists a natural transformation A s × B t ~> B(s × t) with the obvious associativity property.
Proof. We need to transform F s × F t ~> F (s × t):
(A s + B s) × (A t + B t) ~> A (s × t) + B(s × t).
Transforming A s × A t is easy. To transform terms such as A s × B t, we use the modularity property to get B(s × t).
Q.E.D.
It remains to be seen whether there exist other subsets of exp-polynomial functors that are either applicative or monadic but are not covered by the constructions shown above.
