[Haskell-cafe] Category theory as a design tool

[wren ng thornton]

On 6/23/11 4:30 PM, Alexander Solla wrote:
> Please read "Fast and Loose Reasoning is Morally Correct".
> http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/fast+loose.pdf
>
> As I have told you before, it is perfectly appropriate to ignore
> bottom-the-type and bottoms-the-inexpressible proto-values to recover the
> categorical product semantics of (,).  It's not even hard.  It will make
> your life easier.  All you have to do is apply an equivalence relation that
> considers all bottom-proto-values as equivalent.  Domain theory is an
> unnecessary complication.  All bottoms have the same semantics anyway --
> they all diverge.

I've read it a few times, even before the first time you suggested it.
It's an excellent paper. And yet, there are times when fast and loose
reasoning is not factually correct, morals aside. For one, not all bottoms
do diverge, thanks to extensible exceptions.

The fact that tuples are not products does have real, moral(!)
ramifications--- even if we fallaciously assume that all bottoms do
diverge. For example, it dictates a particular implementation for Arrow
(->), an implementation which can cause performance issues due to
excessive laziness. There are plenty of other examples where the choice of
implementation is forced by the desire to be lazy, even when the laziness
is not necessary or helpful in all contexts. I'm a big fan of laziness,
but it's a two edged sword. Forcing people to grip one edge or to write
duplicate code for different circumstances is not an agenda I can support.

Another example that's near and dear to many folks on this list is the
fact that the existence of bottoms means Haskell as a logic is
inconsistent and therefore lacks many properties we would like for
provably correct programming. Regardless of how we reason about bottom,
the fact that we cannot choose to *not* reason about bottom means that the
game is already fixed. Clearly you're not interested in the goals of total
functional programming, but many people on this list are, and your
continuing argument that those goals are irrelevant (or irreconcilable
with laziness) is not endearing.

Arnaud was asking how CT could be used when designing systems. I gave an
example. That you do not like my example is neither here nor there.
Besides, domain theory isn't all that complicated; especially not when
comparing it to the whole of category theory.

-- 
Live well,
~wren