On Mon, 8 Jan 2007 08:51:40 -0500
"Jim Apple" <jbapple+haskell-c...@gmail.com> wrote:Well, not really - or not the proof you thought you were getting. As I
> 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
> GHC's type checker ends up doing exactly what it was doing before:
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)
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.