[Haskell-cafe] GADTs are expressive

Robin Green greenrd at greenrd.org
Mon Jan 8 11:59:06 EST 2007

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.


More information about the Haskell-Cafe mailing list