|
| |||
|
|
Some polynomial functors are not monads Working in a Cartesian closed category, we consider polynomial functors -- that is, functors built up from constant functors, the identity functor, product, and co-product operations. For functional programming, these functors are polynomial generic data types. These data types can be written in Haskell syntax like this, data P x = Empty | Two x x and this corresponds to the polynomial P(x) = 1 + x*x. Other standard examples are data Maybe x = Nothing | Just x -- Maybe(x) = 1 + x data Vec3 x = Vec3 x x x --- Vec3(x) = x*x*x From the mathematical point of view, these polynomials belong to a free commutative semi-ring with zero and one, generated by type symbols such as `x`, `y`, etc. The zero element corresponds to the `Void` type, the unit element to the `Unit` type. Subtraction and division are undefined. The semi-ring is "free" because there are no relations on `x`, `y`, etc. The only relations are those of the commutative semi-ring: x+y = y+x, x*y=y*x, (x+y)+z = x+(y+z) etc. The distributive law holds, x*(y+z) = x*y + x*z. So, any polynomial from this semi-ring, such as 1+1+x+x*x+x*x+x*x*y*y, corresponds to a data type parameterized by type variables `x`, `y`, etc. These are the "polynomial" data types. Now, all polynomial data types are functors. I believe it is an open question how to determine whether a given polynomial functor has the property of being a monad (in the sense of functional programming). A monad is defined as a functor F for which two natural transformations exist: point: x -> F(x) join: F(F(x)) -> F(x) such that one can define the Kleisli category on the functor F. The Kleisli category on F is defined as the category with the same objects (a, b, ..., x, ...) as the initial category, but with arrows of the form a -> F b instead of a -> b. The identity arrow is defined using `point` as id: a -> F(a) = point and the composition of two Kleisli arrows is defined using `join`: f : a -> F b g: b -> F c ---- f <∘> g : a -> F c The formula for f <∘> g is: f <∘> g = f ∘ F(g) ∘ join where F(f) is the lifting of a function f into the functor F, and p ∘ q is the function composition defined by (p ∘ q) (x) = q(p(x)) The requirement that the Kleisli category axioms (left identity, right identity, associativity of composition) should hold leads to the following three laws for `join` and `point`: F(point) ∘ point = id -- left identity point ∘ point = id -- right identity F(join) ∘ join = join ∘ join -- associativity Now, the question is which polynomial functors admit `point` and `join` with these properties. This seems to be an open question without an easy answer. In practice, it would be useful to have an algorithm that determines whether a given data type (say, dictated by the business requirements of a particular application) has a monad property. As an example, I have verified by hand that the type P defined above -- P(x) = 1 + x*x --- does not admit any definitions of `point` and `join` that satisfy the three laws. However, polynomial functors 1 + x, x + x, and x + x*x are monads - they all admit lawful definitions of `point` and `join`. Some further observations: 0. In an earlier post I showed that all polynomial functors F admit a natural transformation of type F(F(x)) -> F(x). However, I didn't check the laws back then. Now I found that some functors cannot have any such natural transformation that satisfies the required laws. 1. Some linear polynomials are monads: P(x) = a0 + a1*x where a0, a1 are constant types and a1 is a monoid type. We can also set a0=0 and/or a1=1 in this formula, to obtain some well-known standard monads. As a monoid type, we can always take a1 = 1 + 1 + ... + 1 for a finite and fixed number of units. The monoid operation is e.g. the "smallest" of the two values. 2. A product of two monads is a monad. 3. I am still not sure whether the co-product x + Q(x) can be always defined as a monad if Q(x) is a monad. There is still hope that this is true. The `point` method must be x -> x for this to work; checking associativity is somewhat cumbersome. I'm now developing some new mathematical notation that should help in writing natural transformations for polynomial functors and in checking their properties by hand. Update: I checked it; x + Q(x) is a monad when Q is a monad. How to recognize what polynomial functors are monads? How to formulate that property in the language of commutative semi-rings freely generated by a symbolic variable `x`? For example, it seems to me that 1 + x + x*x cannot be a monad; however 1 + x + x + x*x is a monad because it is isomorphic to (1+x)*(1+x), which is a product of monads. Is this true? It is very tedious to check by hand that a certain functor cannot have any implementations of `point` and `join` that would satisfy the required laws. I'd like to have a criterion that's easy to apply. The next question is about recursive polynomial functors, that is, functors defined by fixpoint equations F(x) = S(x, F(x)) or F(x) = Fix[y] S(x, y) where S(x,y) is a bifunctor, i.e. a functor in both x and y. The question is, for what bifunctors S do we obtain a fixpoint functor F that has the monad property? |
||||||||||||||