John Hughes mentioned a deficiency of Haskell:
OK, so it's not the exponential of a CCC --- but
Haskell's tuples aren't the product either, and I note the proposal to
change that has fallen by the wayside.
and Phil Wadler urged to either lift BOTH products and functions,
or none of them.
My two pence:
If functions/products are not products and exponentials of a CCC, you
should aim for the next best thing: an MCC, a monoidal closed category.
But Haskell's product isn't even monoidal:
There is no type I such that A*I and A are isomorphic.
The obvious candidate (in a lazy language) would be
the empty type 0, but A*0 is not isomorphic to A but to the lifting of A.
Another problem: the function space A*B -> C should be naturally
isomorphic to A -> (B -> C). What does the iso look like?
One half is the obvious curry function:
curry f x y = f(x,y)
But what is the other half? Apparently, it should be either
uncurry1 f (x,y) = f x y
or
uncurry2 f (~(x,y)) = f x y
Which one is right depends on which one establishes
the isomorphism. Consider the definition
f1 (x,y) = ()
Now:
uncurry1 (curry f1) undef =
undef =
f1 undef
while on the other hand:
uncurry2 (curry f1) undef =
curry f1 (p1 undef, p2 undef) =
f1(p1 undef,p2 undef) =
() =/=
f1 undef
This suggests that uncurry2 is wrong and uncurry1 is right, but for
f2 (~(x,y)) = ()
the picture is just the other way around.
BTW It doesn't help to employ "seq" in the body of curry.
Looks rather messy.
Can some of this be salvaged somehow?
--
Stefan Kahrs
