On 1/8/07, Robin Green <[EMAIL PROTECTED]> wrote:
On Mon, 8 Jan 2007 08:51:40 -0500
"Jim Apple" <[EMAIL PROTECTED]> wrote:
> GHC's type checker ends up doing exactly what it was doing before:
> checking proofs.
Well, not really - or not the proof you thought you were getting. As I
am constantly at pains to point out, in a language with the possibility
of well-typed, non-terminating terms, like Haskell, what you actually
get is a "partial proof" - that *if* the expression you are demanding
terminates, you will get a value of the correct type.
Of course. Were there a recursion-free dialect of Haskell, it could be
typecheck/proofcheck the Terminating datatype, though it would be
useless for doing any actual work. Proof assistants like Coq can solve
this dilemma, and so can languages in the Dependent ML family, by
allowing non-terminating programs but only terminating proofs, and by
proving termination by well-founded induction.
Nobody should think Haskell+GADTs provides the sort of assurances that
these can.
Jim
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
