[Haskell-cafe] Relevance and applicability of category theory

[Derek Elkins]

On Wed, 2008-01-30 at 16:23 -0800, aaltman at pdx.edu wrote:
> Category theory seems to have an inconsistent relationship to Haskell  
> - both documentation and the language's implementations of categorical  
> concepts.  I come from a math background that makes the Haskell's  
> tight coupling to its mathematical foundation very appealing.  But, I  
> may have found some inconsistencies.  Whether you agree or not I hope  
> we can get some discussion going that will clarify the wikibooks, etc.
> 
> My issues:
> 1. Are Haskell monads useful in a truly categorical sense?
> 2. Is Haskell's functor class misnamed?
> 3. Haskell arrows and Haskell monads have a misleading relationship
> 
> 1. Categorical monads are a class of functors, that is, morphisms on  
> Cat.  Haskell's monads are at least a bit closer to the categorical  
> idea than Haskell's functors by virtue of having the same domain and  
> codomain: Hask -> Hask.  I think applicability of Haskell monads  
> beyond sequencing computation, and the validity of their definition,  
> would be much more clear if someone explained the meaning of adjoint  
> functors to and from Hask.  In other words, provide the mathematical  
> characterization to make Haskell monads a precise representation of  
> categorical monads on Hask.

Adjunctions and monads are related, but you don't have to talk about
adjunctions to talk about monads.  There are potentially multiple
adjunctions that correspond to a monad.  At any rate, the definitions
for adjunction and monad aren't dependent on the category.  Once you
create a suitable Hask category (which takes some fudging or a bit of
care), the meaning of "monad" and "adjunction" are clear.  Given a
reasonable Hask category, Haskell Monads are categorical monads if they
satisfy the monad laws.  Haskell does not enforce those laws, but
otherwise, Haskell monads are monads.

> 
> 2. Functors are structure preserving maps in the category Cat.  The  
> Haskell Functor class represents structure preserving maps in the  
> category Hask, which seem to me more like the categorical notion of  
> arrows or the algebraic notion of homomorphisms.  If we talk about  
> functors relating to Haskell, it seems more likely we'd be referring  
> to functors to or from the category Hask than functions (or arrows or  
> whatever) between elements of Hask.  Maybe categorical functors are
> useful as an abstract characterization of programs themselves: a  
> program defines a functor from the problem domain into Hask, or from  
> Hask into output in a problem domain.  The name "Arrow" is already  
> taken; what about renaming Functor to Automorphism?

If you view Hask as a category of Haskell types and Haskell functions,
then a type constructor is the object mapping of a functor (possibly,
co-, contra-, in-, free-variant).  The Functor type class singles out
those that are covariant functors in their last type argument, except
again, Haskell doesn't enforce the functor laws.  Haskell Functors and
Monads do not capture the general notion of functor and monad, they only
deal with the special case of strong (endo)functors from Hask -> Hask.

> 3. I believe the documentation stating that Haskell arrows are a  
> generalization of Haskell monads, but arrows are a categorical thing  
> too and in that context bear a much more distant relationship to  
> monads.  Does a Haskell arrow have Hask as domain and codomain?  Or is  
> one particular element in Hask its domain and possibly another its  
> codomain?  Those are not at all the same thing.

The name "Arrow" is in reference to categorical arrows, but isn't trying
to be categorical arrows.  Haskell Arrows correspond to Freyd
categories.  The correspondence is pretty direct and intuitive.

> My guess is that the concept of Hask is too murky to be any use right  
> now.  The documentation may be more clear by avoiding it until we work  
> out a formal definition... or is there one already?

An accurate Hask category takes some care to define, but it isn't
conceptually murky.