Re: [Haskell-cafe] GADTs are expressive

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 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