[Haskell-cafe] category design approach for inconvenient concepts

[wren ng thornton]

On 12/21/12 3:27 AM, Oleksandr Manzyuk wrote:
> On Fri, Dec 21, 2012 at 4:40 AM, Alexander Solla <alex.solla at gmail.com> wrote:
>> 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.

Surely if we have any interest in the semantics of Haskell, we should be 
considering things modulo the usual relations. Of course, this takes us 
directly to the question of what semantics we're actually trying to capture?

Considering terms modulo alpha is obvious. N.B., alpha just refers to 
locally bound variables, not to definitions. We can define multiple 
copies of "the same" type with different names for the data and type 
constructors, and Haskell will hold these things distinct. If they truly 
are "the same" then they'll be isomorphic in the category, which is 
something we deal with all the time.

Considering things modulo delta is also pretty obvious. That is, 
inlining (or outlining) of definitions shouldn't have any semantic 
effect. If it does, then referential transparency fails, and that's one 
of the things we've sworn to uphold.

When we turn to beta (and iota, sigma,...), things start getting 
complicated. On the one hand, we'd like to include beta since it's 
standard in PL semantics. Moreover, since GHC does a certain amount of 
beta at compile time, we sorta can't get away from including it--- if we 
want to believe that (modulo bugs) GHC is semantics preserving. However, 
on the other hand, that means we can't have our semantics say too much 
about the operational differences between Haskell terms. Again, this is 
standard in denotational semantics; but there are reasons to be 
interested in operational semantics as well...

Turning thence to eta, I'm not sure how things stand. It's known that 
eta breaks certain nice properties about type inference/checking, 
especially once you're in the land of full dependent types, but I don't 
recall whether there are any *semantic* issues to be worried about. 
Haskell98 isn't subject to the issues dependent types have, but modern 
GHC is perilously close. E.g., older implementations of GADTs did 
occasionally require outlining in order to provide the necessary type 
signatures, but that's been fixed IIRC. In any case, we do certainly 
need to be careful about the phrasing of eta, since seq can distinguish 
f from (\x -> f x) if f happens to be bottom. So we don't get full eta, 
but how much of it can we salvage? Does it matter for the categorical 
treatment?

-- 
Live well,
~wren