[Haskell-cafe] GADTs are expressive

[Robin Green]

On Mon, 8 Jan 2007 08:51:40 -0500
"Jim Apple" <jbapple+haskell-cafe at gmail.com> wrote:
> 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