The group you are posting to is a Usenet group. Messages posted to this group will make your email address visible to anyone on the Internet.
Your reply message has not been sent.
Your post was successful
 |
Newsgroups: fa.haskell
From: Robin Green <gree...@greenrd.org>
Date: Mon, 08 Jan 2007 17:11:28 UTC
Local: Mon, Jan 8 2007 12:11 pm
Subject: Re: [Haskell-cafe] GADTs are expressive
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.
| |||||||||||||