Lambda the Ultimate

This's so much clearer than the other category-theory things I've been reading. I think that target audience is well stated -- "what's under the hood with all this weird stuff?" being the driving question for the audience.

... then it's no surprise that you're not impressed w/ the other paper. For at least some of us neophytes, however, the Lattice-theoretic treatment is opaque as obsidian.

It was not my intent that anyone, let alone "neophytes!", should read that particular thesis (however, it is interesting if you are interested). If I ever do write that article, the only mention of the thesis would probably be in a footnote or just a reference in the bibliography, and the target audience, for that section at least, would not be "beginners".



My main complaint with this paper, especially given the degree it emphasizes the category theory, is that it is just: "we all know monads come from category theory, but let's prove it... okay, now that that's outta the way, where were we...". It, and most of the more "theoretical" introductions/tutorials/etc., are like that. They build up this foundation, then immediately ignore it. Now that you now explicitly know how the definitions mesh (pretty much trivially) what are you going to do with it? Nothing! My point is that is does not need to be this way; that there is potential benefit in understanding, manipulation, and implementation that can be derived from the category theory. It is not necessary that all of the formalism be introduced or used in such an introduction, but the resulting ideas and intuitions should be there. But if you're not going to do this, don't bother providing the formalism at all. I have no issue with "practical" introductions that essentially ignore the CT.



Finally I should note, many of the theoretical papers are not like this, and, in my opinion, if you are interested in the theory they make much better and more useful introductions or resources. E.g. Moggi's original Notions of Computation and Monads.



As an example, the monad for free algebras, and a free (finitary) algebra construction in Haskell (unfortunately untested):

data FreeMonad sig a 
  = Return a 
  | Expr (sig (FreeMonad sig a))

foldFM ret expr (Return a) = ret a
foldFM ret expr (Expr e)
  = expr (fmap (foldFM ret expr) e)

instance Functor sig => Functor (FreeMonad sig) where
    fmap f = foldFM (Return . f) Expr

instance Functor sig => Monad (FreeMonad sig) where
    return = Return
    fm >>= f = foldFM f Expr fm

-- examples

-- Maybe is
data MaybeSig x = Nothing

-- Tree (NonDet) is
data NonDetSig x = Fail | Amb x x

-- Either s is
data EitherSig s x = Error s

Already this is a simple example of what I was talking about. We have three monads completely defined with no effort. We can clearly see the relations, and there is an intuitive base for the ideas. It interesting to note that I have never seen this anywhere for Haskell despite that most of the ideas (e.g. "signatures") are used and understood in other contexts (e.g. fold algebras). Incidentally, I should point out that this isn't some deep insight, but the most obvious first thing to do.

Why walk when you can take the tube? PDF an incomprehensible little paper that uses exactly this free monad construction.

It gives me 403 Forbidden.

Indeed, Conor's entire site is giving a 403 now for some reason. Here's the surprisingly readable google cache HTML version of the paper. (Or just google "Why walk when you can take the tube".)

http://www.cs.nott.ac.uk/~wss/Publications/DataTypesALaCarte.pdf

Unimo has some interesting work in this line.

Also at the end of the Haskell Workshop talk, Beauty in the Beast: A Functional Semantics of the Awkward Squad, there was an excellent question and an excellent answer. Someone asked why a free term representation was being used. The answer was, since free constructions are left adjoints (a well known fact in category theory) and all left adjoints are cocontinuous (preserve colimits and thus specifically coproducts/sums, another well known fact in category theory) this implied that the coproduct of (way of combining) two free monads is just the free monad on the coproduct of term algebras, but this latter coproduct is easily directly represented in Haskell.

However, it is stated earlier that each object (such as Int for Haskell) must have a unique identity morphism.

Note that id is parameterized over all types. The simplest way to think about this is to consider it a family of functions (morphisms) with the same name, one for each type (each object of the Haskell category).

Another way to think about it is to consider id to include an implicit functor application that maps the type of its argument to the appropriate identity morphism for that object before applying it.

In categorical notation, the identity morphism for an object A can be written id_A. Thus, "id" can be thought of as an operation that maps an object (A) to its identity morphism (id_A).

In Haskell, the full type of id is ∀a.a→a. This can be interpreted as saying that id takes two arguments, a type, a, and a value of type a. In lower-level languages like System F (used internally by GHC) and the lambda cube (used by JHC), this can be written λa:★. λx:a. x (where ★ is the kind of types). In those languages, id Int corresponds to id_Int.

id must further have the property that for all other arrows, id . f = f and f . id = f. No other choice will accomplish this.

When we choose Haskell functions as the morphisms of the set M_H, is it the abstract syntax of the functions that we use as elements?

If so, then id . f and f have different abstract syntaxes for any f. So by itself, . cannot be the category composition function. Maybe something like a big-step evaluator is needed? But then, what would happen to repeat?

The Haskell syntax is (implicitly) being interpreted via, say, a denotational semantics (big step semantics), so that A -f-> B is more like [[A]] -[[f]]-> [[B]]. So we only need id and (.) to be appropriate in the semantic domain, i.e. id and (.) are the set identity function and composition which does satisfy the laws. Incidentally, id being unique is a result not an assumption (axiom), id must be unique if it and (.) satisfy the category theory axioms. What the semantics is is irrelevant. Except, insofar as we are using Haskell syntax to specify arrows, [[id]] must interpret as id. We don't need to worry about (the categorical) (.) since it isn't an arrow.

You could use the HTML special characters to write the notation. Here's a couple of them based on your descriptions.

∀ → For All
∃ → Exists
∈ → Element of

I think rather than element he meant:
⊆ → is a (not necessarily proper) subset of

There's a pretty good collection of these on Wikipedia.