Re: [Haskell-cafe] Questions about the Functor class and it's use in "Data types à la carte"

[Dominic Steinitz]

Jonathan Cast wrote:
> On 16 Dec 2007, at 3:21 AM, Dominic Steinitz wrote:
> 
>>>> Do you have a counter-example of (.) not being function composition in
>>>> the categorical sense?
>>>
>>> Let bot be the function defined by
>>>
>>> bot :: alpha -> beta
>>> bot = bot
>>>
>>> By definition,
>>>
>>> (.) = \ f -> \ g -> \ x -> f (g x)
>>>
>>> Then
>>>
>>>    bot . id
>>> = ((\ f -> \ g -> \ x -> f (g x)) bot) id
>>> = (\ g -> \ x -> bot (g x)) id
>>> = \ x -> bot (g x)
>>
>> I didn't follow the reduction here. Shouldn't id replace g everywhere?
> 
> Yes, sorry.
> 
>> This would give
>>
>> = \x -> bot x
>>
>> and by eta reduction
> 
> This is the point --- by the existence of seq, eta reduction is unsound
> in Haskell.
> 

Am I correct in assuming that if my program doesn't contain seq then I
can reason using eta reduction?

>>
>> Why is seq introduced?
> 
> Waiting for computers to get fast enough to run Haskell got old.
> 

I'm guessing you were not being entirely serious here but I think that's
a good answer.

> Oh, you mean here?  Equality (=) for pickier Haskellers always means
> Leibnitz' equality:
> 
> Given x, y :: alpha
> 
> x = y if and only if for all functions f :: alpha -> (), f x = f y
> 
> f ranges over all functions definable in Haskell, (for some version of
> the standard), and since Haskell 98 defined seq, the domain of f
> includes (`seq` ()).  So since bot and (\ x -> bot x) give different
> results when handed to (`seq` ()), they must be different.
> 
> The `equational reasoning' taught in functional programming courses is
> unsound, for this reason.  It manages to work as long as everything
> terminates, but if you want to get picky you can find flaws in it (and
> you need to get picky to justify extensions to things like infinite lists).
> 

Reasoning as though you were in a category with a bottom should be ok as
long as seq isn't present? I'm recalling a paper by Freyd on CPO
categories which I can't lay my hands on at the moment or find via a
search engine. I suspect Haskell (without seq) is pretty close to a CPO
category.