[Haskell-cafe] Re: Why?

[Dan Doel]

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