Aug. 16th, 2015

juan_gandhi: (VP)
This has been dragging forever. Let me cover it, shedding light to the dark corners, ok?

Introduction



First, definitions. I'll try to use, as much as possible, Scala notation, and, basically, Scala terms.

A category consists of types and functions; a function is from one type to another; some functions can compose (if one starts where the other ends), composition is associative, and there's an identity function for each type.

There's more than one category in this (kind of) world. Given two categories, C and D, we can build a product category, C × D, consisting of pairs of types and pairs of functions.

Some categories have a special type called unit; every type has exactly one function to unit. Functions from unit to a type are called points or instances. Instead of writing a:1⇒A we use to write a shortcut, a:A This is just a syntactic sugar.

Another syntactic sugar is this: if we have a point a:A, its composition with a function f:A⇒B is usually thought of as an "application" of f to a, and is written as f(a):B; but remember, it is just a composition of two functions.

It is good to know what instances a type has, but, in general settings, not all properties of a type are defined by the "set" of its instances. If they are, the category is called well-pointed. Remember this word, it's important.

In the case of a well-pointed category a function f:A⇒B is fully defined by its "application" to points of A. It is important to remember that it is not always the same thing. Not every category is well-pointed.

A category may have cartesian product defined, for a couple of types, A and B, one defines A×B, with two projection functions, to A and B, such that having a function C ⇒ A×B is the same as having a pair of functions, C⇒A and C⇒B; projections provide this one-to-one correspondence.

Note, for instance, that having a couple of points, a:A and b:B is the same as having a point c=(a,b):A×B. So some people believe that a cartesian product is just a "set" of pairs.

A functor F is mapping of types from one category to types of another, and of functions of one category to functions of another, with clearly defined rules (f:A⇒B maps to F[f]:F[A]⇒F[B], composition and identity are preserved. The action of a functor on a function, F[f] is often denoted as map[F](f). Of course map[F](f) is a function from F[A] to F[B].

Note, not every category is a category of sets. For instance the category of all categories is not a category of sets. The category of monoids is not a category of sets. It is important to remember that not everything is a set. For instance, a category of sets is not (usually) a set.

Even if you think you are dealing with the category of sets, it is important to remember that there is no such thing. One can always ask "which one?", and learn that you cannot enumerate categories of sets. We know some, and many more are still hiding, nobody knows how many. We should thank Goedel for this interesting fact of life.

Also, in case you somehow did not know, axioms of any theory, including a theory of sets, are not Eternal Truths Known To The Scientists. They are just assumptions under which a theory is being developed and applied. The same is true about (a) category theory. We do not insist on associativity of functions composition. We just say that in a category, composition is associative.

All this sounds extremely trivial, so it is very frequently forgotten.

Monad


A monad is a any functor M from a category C to itself with two properties:

  • there is a unit aka "pure" function u[X]: X⇒M[X], for every X and this function behaves (commutes with other functions etc)

  • there is a monad multiplication aka flatten function flatten:M[M[X]]⇒M[X] for each X, with good properties: a) it is associative, b) unit is left and right unit for this multiplication



I'm not going into deeper details, you can find them everywhere. Just remember this funny thing, that both unit and flatten are defined for each type, and are defined naturally, so a function from A to B combines seamlessly with these.

Being a functor, a monad has map, but there's more.

def flatMap[F,A,B](f:A=>F[B]) = map[F](f).flatten

This function, flatMap, can be used to define flatten, and it satisfies the right rules, which are harder to formulate for flatMap than for flatten.

There's a belief, in Haskell circles, that each monad is also an applicative functor (defined below). This belief has just one foundation: it's based on the belief that every category is well-pointed.

Applicative Functor



There's more than one definition; I'll use the one that does not require anything else except what was defined above.

Applicative functor, aka lax monoidal functor is such a functor F that has


  • zip[A,B]: F[A]×F[B] ⇒ F[A×B] defined for all A and B, having natural properties and behaving consistently if we have three types, A, B and C;

  • pure[A]: A ⇒ F[A] that is natural and combines well with zip


There are variants of this definition, where functor strength is defined differently; this one is pretty popular in comp sci, so there.

How can it possibly be related to monads? Here is the way Haskell and Scala people define strength for any monad, just from the definition of monad:

Say we have a monad T, and a couple of types, A and B, there's a trick that produces T[A]×T[B] ⇒ T[A×B]. How? Here's the trick.

1. Define a coupler function, A ⇒ B ⇒ A×B, like


coupler: A ⇒ B ⇒ A×B = a ⇒ (b: B) ⇒ (a, b)


There’s something fishy in this definition. First, It is not a function in our category. We have a function from type A to what? To functions from B to A×B. Funny, the collection of these functions does not belong to our category. We could introduce such a type, X⇒Y, every instance of which is a function from X to Y, or we could, if possible, the sum of units indexed by functions from X to Y. In both cases we will have a type in our category, but remember, they may be distinct. Second, even if our types were covered with instances, like in a well-pointed category, it is still not always so that defining mappings on instances gives us a legitimate function (check out topological spaces, groups, etc).

We map with T, getting a function


couplerT: T[A] ⇒ T[B ⇒ A×B]


For each instance tb:T[B] we canb uild another function, lifter(tb), that takes any function B ⇒ A×B and produces an instance of T[B]:

lifter(tb): (B ⇒ A×B) => T[A×B]

lifter(tb) takes a function f from B to A×B and produces an instance tab:T[A×B] by applying map[T](f) to tb.

See, it's just a special case of map; if you are a Haskell programmer, you would think this is the same as map. Not so from categorical point of view, for a couple of reasons.

Again, this is fishy. We suddenly talk about instances of T[B] as if they are all that we need to define a function. They are not, in general settings where the category is not well-pointed. More, the mapping is from functions to a type; each function gives an instance of a type; it is not even a function in our category.

If we map lifter with map[T] (call it lifterT), we get a function from T[B ⇒ A×B] to T[T[A×B]].

Now, given a couple of instances, ta:T[A] and tb:T[B], from the first we get an instance of T[B⇒A×B], and from this instance and from tb we get an instance of T[T[A×B]]; flatten it, and voila, an instance of T[A×B].

See, we relied on well-pointedness of our category? So many times we relied on the fact that since an A can be covered by its instances, an A×B can be covered by B.

This trick does not work if our category is not well-pointed, as well as in many other occasions. E.g. it is a category of sets on which some group, or a monoid is acting. Or if we are dealing with sets that change in time. Or a category of topological spaces.



This was the first part. Next I'll write about some specific monads and non-monads.

If you want to see an example of a monad that is not strong (that is, not an applicative functor), see the bottom of this: http://mathoverflow.net/questions/85391/any-example-of-a-non-strong-monad/86914#86914

Profile

juan_gandhi: (Default)
Juan-Carlos Gandhi

August 2025

S M T W T F S
      12
3456789
10 11 12 13141516
171819 20212223
24252627282930
31      

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Aug. 24th, 2025 09:14 am
Powered by Dreamwidth Studios