Roberto Zunino wrote:
Dominic Steinitz wrote:
This would give
= \x -> bot x
and by eta reduction
This is the point: eta does not hold if seq exists.
undefined `seq` 1 == undefined (\x -> undefined x) `seq` 1 == 1
Ok I've never used seq and I've never used unsavePerformIO. Provided my program doesn't contain these then can I assume that eta reduction holds and that (.) is categorical composition?
The "(.) does not form a category" argument should be something like:
id . undefined == (\x -> id (undefined x)) /= undefined
where the last inequation is due to the presence of seq. That is, without seq, there is no way to distinguish between undefined and (const undefined), so you could use a semantic domain where they coincide. In that case, eta does hold.
It would be a pretty odd semantic domain where 1 == undefined. Or perhaps, I should say not a very useful one.