On Mon, 8 Jan 2007 08:51:40 -0500
"Jim Apple"
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.
Well, not really - or not the proof you thought you were getting. As I am constantly at pains to point out, in a language with the possibility of well-typed, non-terminating terms, like Haskell, what you actually get is a "partial proof" - that *if* the expression you are demanding terminates, you will get a value of the correct type. If it doesn't, you won't get what you wanted. (Unlike in say Coq, where all functions must be proved to terminate - modulo a recently-discovered bug.) What this means is that you can supply e.g. "undefined" in place of (2) or (3) and fool the typechecker into thinking that (1) terminates, when it doesn't. -- Robin