[Haskell-cafe] Re: Why?
dan.doel at gmail.com
Fri Dec 11 13:34:28 EST 2009
On Friday 11 December 2009 1:06:39 pm Luke Palmer wrote:
> That's how I see it as a user of the language. At the most abstract
> level, omitting some of the practical details of the language (such as
> the built-in numeric types), Haskell's reduction follows beta
> reduction with sharing, and so at that level I think the answer to (2)
> is "nothing".
Yes, that's probably the answer, but a related question is how useful the
logic is for various applications.
For one, the logic that corresponds to Haskell via Curry-Howard is
inconsistent, because general recursion/fix/error/negative types/etc. let you
forall a. a
But that isn't a very desirable property from a logical standpoint, because it
calls into question whether any proofs you do really prove what they allege.
Second, again via Curry-Howard, Haskell's (GHC's) type system corresponds to a
higher-order logic without first-order quantification, because it doesn't have
real dependent types. This is why you need things like Haskabelle: because the
propositions (types) in Haskell *can't* talk about value-level terms, and
those are generally what you want to prove things about.
With enough GADT/type family fanciness, you can reconstruct (roughly) every
value-level entity in the type level, and establish a correspondence between
any value-level term 't' and its associated type-level term 'T', such that if
you prove something about T, you know (by construction) that a related
property holds for t. And then you can use the fact that Haskell is a higher-
order logic to prove the things you want about T. But this is convoluted and
difficult (and you still have to worry that your proof is accidentally bottom
More information about the Haskell-Cafe