On Thu, Dec 20, 2012 at 12:53 PM, Oleksandr Manzyuk
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)