On Fri, Dec 21, 2012 at 4:40 AM, Alexander Solla <alex.so...@gmail.com> wrote: > > > 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)
If you compute (f . g) . h, you'll get \x -> (f . g) (h x) = \x -> (\x -> f (g x)) (h x), whereas f . (g . h) produces \x -> f ((g . h) x) = \x -> f ((\x -> g (h x)) x). As raw lambda-terms, these are distinct. They are equal if you allow beta-reduction in bodies of abstractions. That's what I meant when I said that we probably wanted to consider equivalence classes modulo some equivalence relation. That hypothetical relation should obviously preserve beta-reduction in the sense (\x -> e) e' = [e'/x]e. When we do equational reasoning about Haskell code, we apply certain rules. I think what I'm asking for is an explicit complete set of such rules. Note that sometimes you can also hear that the category of Haskell is a suitable cpo category. However, this is an answer to a slightly different question: what is the categorical model of Haskell? That is, what kind of categories can Haskell programs be interpreted in. What I'm after is a kind of universal syntactic Haskell category. I expect the situation to be similar to the simply typed lambda-calculus but more technically involved. The simply typed lambda-calculus can be interpreted in any cartesian closed category, but it is also possible to construct a cartesian closed category out of the simply typed lambda-calculus. As someone coming to Haskell and functional programming from category theory background, I'm probably paying to much attention to details that don't concern most practicing functional programmers... Sasha -- Oleksandr Manzyuk http://oleksandrmanzyuk.wordpress.com _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
