[Haskell-cafe] Category theory as a design tool

[Alexander Solla]

On Thu, Jun 23, 2011 at 9:14 PM, wren ng thornton <wren at freegeek.org> wrote:

> 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.
>

I've only suggested it once.  On the other hand, I had these ideas
independently, when I first learned Haskell and was trying to form a mental
picture of the lattice of Haskell types.  That must have been in 2008.  I
take no credit for their work.


> 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.
>

Unfortunately, it is an agenda mandated by the language.  Bottoms like 'seq'
and 'performUnsafeIO' or 'unsafeCoerce' might not diverge in an "in context"
sense, but they essentially change the language's semantics.  The same is
true for 'error' and 'undefined' (the only reason extensible exceptions can
catch these is because the run-time throws an exception for them...) .  This
is divergence by another name.  The semantics these bottoms introduce are
not expressible by the language, in the context which they modify.  It must
be done at a "lower" level of interpretation.

I agree that the ramifications of strictness or laziness are /real/.  But
they are not moral.


> 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.


Not quite.  Consider "reductio ad absurdum" from many deductive systems for
FOL.  We may choose to reason about bottom in total languages.  It doesn't
make them less total.  And just as we can choose to not reason about bottom
in consistent logics, we can avoid reasoning about bottom in
total/consistent fragments of paraconsistent logics.


> 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.
>

Sorry for raining on your parade!

Haskell is certainly a paraconsistent logic, as you say.  And there are
techniques for staying away from contradictions (i.e., staying within a
consistent/total fragment) in these logics.  They are not hard, and involve
creating a quotient construction which equates all bottoms.  If you want to
use "error" and "par" and "seq" and end up in a different language/logic,
that's fine by me.  You will enter a wilderness where the meaning of code
depends on referentially opaque code[1].

On the other hand, pointing out that (,) is a categorical product under this
quotient construction, and thus showing the relevance of categorical
thinking in Haskell design, is relevant to the discussion of categorical
thinking in Haskell design.  (One might even go so far to say that your
comments that (,) is not a categorical product, when it morally is, is
disruptive to the thread and counter-productive to its goal.  Funny, that's
what you say about my post! )

By the way, I /am/ interested in the goals of total functional programming.
 And that is exactly why I chose to interpret bottoms-the-proto-values as
/the unique contradiction/ in the language and bottom-the-type as the /empty
type/.[2]   Because then I can stay inside of a consistent/total fragment of
the language, and utterly ignore bottom.  It is merely a bonus that I can
use the remaining partial fragment, if I /need/ to.  For example, somebody
might /need/ to mess around with seq to get an Arrow instance to perform
quickly.  But (under some benign assumptions) they will never /need/ to mess
around with seq in order to get correct results.  In other words, using seq
is merely an implementation detail -- a special case where we abuse the
run-time system so that an undefined proto-value changes the language's
semantics in a useful way.  You might not be a fan of requiring "duplicate
code", and I am not a fan of requiring special cases where we change the
underlying interpretation system to contaminate the interpreted language.
 Unfortunately, one of these positions is more realistic than the other,
especially since strict and lazy types are necessarily distinguishable by
the type system.

[1] I guess that's not so scary considering we live in a world where C code
flies airplanes and runs nuclear power plants. ;0)

[2] Note that this is the same reasoning used to model the adjunction
between first order languages and their models.  The lattice of models for a
language has a bottom model, which is empty, and for which everything in the
language is vacuously true.  There is a "bottom" there, and we can safely
ignore it.  Indeed, we can say /anything we want/ about bottoms-as-values,
and it will always be /vacuously true/, even in a consistent/total logic!

And even the languages of consistent logics can have an expression to
represent contradiction.  I have used plenty of FOL deduction systems where
we have the deductive rule of "contradiction elimination":

A |- _|_   => |- !A   (contradiction elimination, reductio ad absurdum,
etc.)

"Doctor, it hurts when I do this" -- "Then don't do that".  Note that we can
impose this deductive rule on Haskell as a logic, to remain in a total
fragment of the paraconsistent whole.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110624/bee19ecc/attachment.htm>