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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
