[Haskell-cafe] GADTs are expressive

[Jim Apple]

On 1/8/07, Tomasz Zielonka <tomasz.zielonka at gmail.com> wrote:
> On Mon, Jan 08, 2007 at 08:02:36AM -0500, Lennart Augustsson wrote:
> > So it sounds to me like the (terminating) type
> > checker solves the halting problem.  Can you please explain which part
> > of this I have  misunderstood?
>
> Perhaps you, the user, have to encode the proof of halting in the way
> you construct the term?

The Terminating datatype takes three parameters:
1. A term in the untyped lambda calculus
2. A sequence of beta reductions
3. A proof that the result of the beta reductions is normalized.

Number 2 is the hard part. For a term that calculated the factorial of
5, the list in part 2 would be at least 120 items long, and each one
is kind of a pain.

GHC's type checker ends up doing exactly what it was doing before:
checking proofs.

Jim