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 category C has a terminal object T and a product diagram A ← A×B → B for any objects A,B∈C, then C has 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, C has a product of no objects, which is simply a terminal object T in C, as well as a product for any two objects.
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 category Hask is 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.
