Derek and Lennart,
Thank you both for your clarifications. Tutorials (and blogs) of the C-H
correspondence and the naive (i.e. set-theoretic) categorical
descriptions of Haskell are so eager to get to the insights you mention
that they gloss too easily over the important role of _|_, a term I have
been learning to give more respect to every time I (re)read about the
differences between sets and CPOs.
If types correspond to theorems and terms correspond to proofs, then I
guess program transformations correspond to rules of inference (e.g.
function application flip ($) :: p -> (p -> q) -> q corresponding to
modus ponens), and what causes the inconsistency is an extra rule of
inference implied by non-strict function application when applied to
bottom allowing the proof \_ -> undefined :: p -> q
What slightly bemuses me is that I would have thought this makes the
proof procedure unsound, and consequently the insights into "the logic
Haskell's type system corresponds to" not terribly insightful when
analogized to intuitionist logic unless there were some computational
way of restricting the proof system to a sound subset, which is what I
was trying to get at by proposing to accept only proofs that terminated.
Obviously, I've got a bit more reading to do before I can really
understand all this.
Dan
Derek Elkins wrote:
On Mon, 2007-10-22 at 01:12 +0100, Lennart Augustsson wrote:
There's nothing wrong with Haskell types. It's the terms that make
Haskell types an inconsistent logic.
Logics are what are consistent or not, so saying the logic Haskell's
type system corresponds to is inconsistent is all that can be said.
Somewhere there is an axiom in it that makes forall a.(a -> a) -> a
hold. Usually, we just take that directly as the axiom (i.e. the
existence of fix).
But that doesn't mean that the C-H correspondence doesn't have any
insight to offer.
Which is certainly not what I said at all.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
