[Haskell-cafe] Re: Why?
Dan Doel
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
prove
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
:)).
-- Dan
More information about the Haskell-Cafe
mailing list