Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет Journal de Chaource ([info]lj_chaource)
@ 2018-04-07 23:40:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
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?


(Читать комментарии) (Добавить комментарий)