On Thu, Dec 20, 2012 at 12:53 PM, Oleksandr Manzyuk <manzyuk@gmail.com> wrote:
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?

I don't see how associativity fails, if we mod out alpha-equivalence.  Can you give an example?  (If it involves the value "undefined", I'll have something concrete to add vis a vis "moral" equivalence)