[Haskell-cafe] GADTs are expressive
tomasz.zielonka at gmail.com
Mon Jan 8 08:13:42 EST 2007
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.
More information about the Haskell-Cafe