Re: [Haskell-cafe] Questions about the Functor class and it's use in "Data types à la carte"
Dominic Steinitz
dominic.steinitz at blueyonder.co.uk
Sun Dec 16 12:47:16 EST 2007
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.
More information about the Haskell-Cafe
mailing list