newbie

[Frank Atanassow]

Lars Henrik Mathiesen wrote (on 10-03-01 20:35 -0000):
> However, in some expositions of category theory, the usefulness of
> monads is justified because they 'belong' to a certain adjunction.

You can regard a monad as arising from a particular adjunction but, although
every adjunction determines a unique monad, the converse is not true. In fact,
the collection of resolutions for a monad forms a category with adjunctions as
objects and certain functors as arrows. The adjunction which gives rise to the
Kleisli category is initial in this category. The terminal object is called
the Eilenberg-Moore category and it has as objects M-algebras, like your `xi',
and as arrows M-algebra homomorphisms.

> In Haskell you can't express the adjunction, only the monad, which may
> take a little getting used to.

I've been looking at this recently to find some canonical way to express how
to `deconstruct' monadic terms (i.e., how to run them). The idea is that you
build up monadic terms in the Kleisli category, somehow describe a resolution,
then use the initiality property of the Kleisli category to map the terms to
the category of the resolution, where you can use the adjunction to
destructure them.

> But how about the related concept of an M-algebra? That is, a type T
> and a function 'xi :: M T -> T' so that these laws hold:
> 	 xi . eta       === id
> 	 xi . (fmap xi) === xi . mu

If you reverse the sense of the last equation and regard the monad primitives
as constructors:

  xi (Eta x) = x
  xi (Mu m)  = xi (fmap xi m)

then this starts to look like a pattern-matching definition for folding a
monad regarded as an algebra. In fact, you can express the operators this way
in Haskell if you use are willing to use a nested datatype:

  data M a = Eta a | Mu (M (M a))

> Would it be useful to have functions that were polymorphic over
> List-algebras? (Not that I have any idea how that might be possible to
> express in Haskell).

I dunno if it is useful for List-algebras, but if you take your monad M as the
substitution monad generated by a term signature, then the the resolutions of
the monad can be regarded as a way of factoring M into a composition of
signatures which (I think) represent the values and redexes of the term
language. The Kleisli and E-M categories are extremal cases. In the Kleisli
category the redex functor is trivial; I think this is this is why you can use
it to pass around computations.

In the E-M category, the value functor is trivial, but I'm not sure what this
means precisely yet. For intermediate cases, you get a particular choice of
normal forms.  What I'm thinking is that an M-algebra for a language M gives
you a way of extending a denotational description of the normal forms to one
for the entire language, which is automatically sound for the equational
theory.

Which sounds useful to me for writing interpreters.

-- 
Frank Atanassow, Information & Computing Sciences, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 253-3261 Fax +31 (030) 251-379