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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
