[Haskell-cafe] category design approach for inconvenient concepts

[Oleksandr Manzyuk]

> 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