On Thu, 20 Dec 2012, Oleksandr Manzyuk
the category of Haskell types and Haskell functions[1]
[1] Note that this may not actually work out to be a category, but the basic idea is sound.
I would be curious to see this example carefully worked out. I often hear that Haskell types and Haskell functions constitute a category, but I have seen no rigorous definition.
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?
Apparently, this (rather non-trivial) exercise has already been carried out for the simply typed lambda-calculus. I'd be curious to see how that generalizes to Haskell (or some equivalent formal system).
Sasha
Yes. It would be well worth carefully carrying out your program for some approximation of a large part of Haskell as she lives in GHC. As mentioned earlier, we should not ignore the distinctions between a. the text of a Haskell program b. the binary of the now compiled program c. the running of the program d. the input output behavior of the program Attempting to force the hoped for clarification to operate only on one part of the whole at least four part structure is likely to not give us what we, ah, I, really want to see. There is some work directly dealing with part of the program: http://www.haskell.org/haskellwiki/Hask oo--JS.
-- Oleksandr Manzyuk http://oleksandrmanzyuk.wordpress.com