Re: [Haskell-cafe] Questions about the Functor class and it's use in "Data types à la carte"
Jonathan Cast
jonathanccast at fastmail.fm
Sun Dec 16 06:35:51 EST 2007
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.
>
> = bot
>
>>
>> which /= bot since (seq bot () = bot) but (seq (\ x -> M) () = ())
>> regardless of what expression we substitute for M.
>>
>
> Why is seq introduced?
Waiting for computers to get fast enough to run Haskell got old.
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).
jcc
More information about the Haskell-Cafe
mailing list