the category of Haskell types and Haskell functions[1]
[1] Note that this may not actually work out to be a category, but the basic idea is sound.
I would be curious to see this example carefully worked out. I often hear that Haskell types and Haskell functions constitute a category, but I have seen no rigorous definition. I have no problems with the statement "Objects of the category Hask are Haskell types." Types are well-defined syntactic entities. But what is a morphism in the category Hask from a to b? Commonly, people say "functions from a to b" or "functions a -> b", but what does that mean? What is a function as a mathematical object? It is a plausible idea to say that a function from a to b is a closed term of type a -> b (and terms are again well-defined syntactic entities). How do we define composition? Presumably, by f . g = \x -> f (g x) This however already presupposes that we are dealing not with raw terms, but with their alpha-equivalence classes (otherwise the above is not well-defined as it depends on the choice of the variable x). Even if we mod out alpha-equivalence, so defined composition fails to be associative on the nose, up to equality of (alpha-equivalence classes of) terms. Apparently, we want to consider equivalence classes of terms modulo some finer equivalence relation. What is this equivalence relation? Some kind of definitional equality? Apparently, this (rather non-trivial) exercise has already been carried out for the simply typed lambda-calculus. I'd be curious to see how that generalizes to Haskell (or some equivalent formal system). Sasha -- Oleksandr Manzyuk http://oleksandrmanzyuk.wordpress.com