Thanks! I'm sure I could have figured this out by looking at the code,
but it was easier to ask.
It's very cool example, even if it doesn't practical. :)
-- Lennart
On Jan 8, 2007, at 08:51 , Jim Apple wrote:
On 1/8/07, Tomasz Zielonka <[EMAIL PROTECTED]> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
