[Haskell-cafe] GADTs are expressive

[Jim Apple]

On 1/8/07, Robin Green <greenrd at greenrd.org> wrote:
> On Mon, 8 Jan 2007 08:51:40 -0500
> "Jim Apple" <jbapple+haskell-cafe at gmail.com> 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