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