[Haskell-cafe] category design approach for inconvenient concepts

[Oleksandr Manzyuk]

On Fri, Dec 21, 2012 at 4:40 AM, Alexander Solla <alex.solla at gmail.com> wrote:
>
>
> On Thu, Dec 20, 2012 at 12:53 PM, Oleksandr Manzyuk <manzyuk at 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