I am starting to play around with the Haskell programming language, it is based off of category theory (well very loosely). There are a few questions I have for any Haskell gurus and category theory mathematicians, namely with regards to the existence of a terminal object in **Hask** (the category of Haskell data types and programs).

The underlying aim, I must confess, is to write up some abstract algebra in Haskell. For the scheme of things, I must give a reference:

- Saunders Mac Lane,
*Categories for the Working Mathematician*, Springer-Verlag (2000).

First let us review some concepts from category theory (and a little Haskell), then we will dive into my rambling questions.

### Review Of Category Theory

To repent for my sins, I will review category theory first before launching into my twisted approach to Haskell.

Let us review two propositions, the first from chapter III "Universals and Limits, section 5 "Categories with Finite Products":

Proposition.If a categoryChas a terminal objectTand a product diagramA←A×B→Bfor any objectsA,B∈C, thenChas all finite products.

For an introduction to category theory in Haskell syntax, the reader is referred to:

- Alpheccar's Blog, "Category Theory and the category of Haskell programs", Part I June 18, 2007; Part II June 24, 2007; Part III: Algebras and Monads July 02, 2007.

There are a few reservations I have about those series of blog posts, for example in Part I the author states "In Haskell, a terminal object may be a phantom type: `data T`

since `T`

is containing only the element undefined." There is a different way to present the terminal object, it's the unit object `()`

.

In fact, now that I think of it, the unit object `()`

as the terminal object is more in line with category theory than the phantom type. If we refer to part II, we have the product correspond to `(A,B)`

. If we use Mac Lane's insight:

In particular,Chas a product of no objects, which is simply a terminal objectTinC, as well as a product for any two objects.

*Categories for the Working Mathematician*

Chapter III Universals and Limits, Section 5 "Categories with Finite Products".

It would follow that the terminal object would correspond to the unit object. Well, to be strict, it would be `(,)`

which is isomorphic to `()`

.

We use Mac Lane's other insight about monoids and groups from Chapter III, section 6 "Groups in Categories", which boils down to this: a monoid in **C** is a triple (*C*, μ:*C*×*C*→*C*, η:*T*→*C*) where *T* is the terminal object of **C**, μ is multiplication, and η is the "identity element" of *C*.

Using the jargon of "stuff, structure, and properties", we have the stuff be *C* an object of a category, the structure be two morphisms μ and η, and the properties be diagrams.

A group in **C** is a monoid (*C*, μ, η) together with a morphism ζ:*C*→*C* which makes a diagram commute (intuitively it sends each element of *C* to its (right) inverse).

Now for something slightly different: if we take the product of two objects `A`

and `B`

in **Hask** to be `(A,B)`

, then **Hask** is closed under finite products.

Conjecture.The categoryHaskis closed under finite products.

### Haskell Question

Now, we have precisely enough knowledge to consider the questions relevant to abstract algebraic Haskell programming.

Naively, I would want to say that in Haskell typeclasses are structure-types. That is, we can write

TerminalObject :: () class Monoid C where mu :: C -> C -> C eta :: TerminalObject -> C

However, we cannot specify anything about the implementation of `class Monoid`

. It is frustratingly close, we have the stuff `C`

, we have the structure, but alas no properties!

Question 1: Is there any way around this or am I doomed? More precisely, is there any way to specify behavior without specifying implementation?

Now, consider the following additional code snippet:

class (Monoid C) => Group C where zeta :: C -> C

Question 2: Can I specify the behavior of `zeta`

without specifying implementation, while assuming that `mu`

and `eta`

have been implemented already?

Haskell is so frustratingly close to being a good language, but it fails at some of these key things.

## No comments:

## Post a Comment