On Thu, Dec 20, 2012 at 12:53 PM, Oleksandr Manzyuk <manz...@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)
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
