Re: [Haskell-cafe] category design approach for inconvenient concepts

On Fri, Dec 21, 2012 at 4:40 AM, Alexander Solla wrote:

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