There is a statement in the "Bridging the Gulf" paper of Shields, Peyton
Jones et al, that for a pointed codomain B the function space A -> B is
also pointed. This is also in their Figure 6 AFAIR.
I am curious where this statement comes from.
As I understand the sole purpose of values of the function space A -> B is
to be applied on some value of type A:
f: A -> B,
a: A
then
f a = _|_ for two reasons (if A is unpointed)
1) f = _|_
2) f ~= _|_ but the result of f applied on a is _|_
if A is pointed then a third possibility is that
3) f ~= _|_, f strict, a = _|_
Since we cannot pattern match on functional values, we cannot check for f
~~= _|_, so essentially 1) and 2) are not distinguishable in Haskell. So why
not go on and say that all function spaces are unpointed, and "blame" the
result of f where actually f is guilty?
There is also a remark in Corrigendum to "Bridging the Gulf" that in pre
1.3 versions of Haskell
undefined and \x.undefined were operationally equivalent. Why has this
changed?
I would be very pleased if someone could shed some light on these issues...
Thanks,
Gabor
