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