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

[Jonathan Cast]

On 16 Dec 2007, at 9:47 AM, Dominic Steinitz wrote:

> 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?

Yes.

>>>
>>> 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.

Not quite --- not if by `a category with bottom' you mean the  
standard category of pointed CPOs and strict functions, because  
Haskell functions aren't necessarily strict.

In the actual category Hask, you don't even have finite products,  
because surjective pairing still fails (seq can be defined in the  
special case of pairs directly in Haskell).

The usual solution is to ensure that everything terminates (more  
precisely, that everythin is total).  In that case, you can pretend  
you're in a nice, neat purely set-theoretic model most of the time,  
and only worry about CPOs when you need to do fixed-point or partial- 
list induction or something like that.

jcc