[Haskell-cafe] GADTs are expressive

[Tomasz Zielonka]

On Mon, Jan 08, 2007 at 08:02:36AM -0500, Lennart Augustsson wrote:
> So Terminating contains all the terminating terms in the untyped
> lambda calculus and none of the non-terminating ones.  And the type
> checker  checks this.  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? Just guessing.

Best regards
Tomasz