Path: g2news2.google.com!news3.google.com!news2.volia.net!news.banetele.no!uio.no!nntp.uio.no!not-for-mail
From: Lennart Augustsson <lenn...@augustsson.net>
Newsgroups: fa.haskell
Subject: Re: [Haskell-cafe] GADTs are expressive
Date: Tue, 09 Jan 2007 00:29:19 UTC
Organization: Internet mailing list
Lines: 40
Sender: haskell-cafe-boun...@haskell.org
Message-ID: <fa.myCER+BcxmEEhjESLokm+UM37bY@ifi.uio.no>
References: <fa.ItfTidVPw1QyDH+tqMWJZNoMcuc@ifi.uio.no> <fa.RJIHdoYOZjkMiyUqkCGN6AT3ryU@ifi.uio.no> <fa.aHPySEve1LnLtczDDWtDcJw6ww8@ifi.uio.no> <fa.cVjiaepnYU6NbaqPSUtBtwcKqsw@ifi.uio.no>
NNTP-Posting-Host: jess.uio.no
Mime-Version: 1.0 (Apple Message framework v752.3)
Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: readme.uio.no 1168302559 29702 129.240.10.48 (9 Jan 2007 00:29:19 GMT)
X-Complaints-To: abuse@uio.no
NNTP-Posting-Date: Tue, 9 Jan 2007 00:29:19 +0000 (UTC)
To: "Jim Apple" <jbapple+haskell-c...@gmail.com>
X-Original-To: haskell-c...@haskell.org
Delivered-To: haskell-c...@haskell.org
In-Reply-To: <ad0e24930701080551t1e28349ct8718941646e9fc6a@mail.gmail.com>
X-Mailer: Apple Mail (2.752.3)
X-Greylist: Sender succeded SMTP AUTH authentication, not delayed by
	milter-greylist-1.6 (calvin.augustsson.net [82.182.103.12]);
	Tue, 09 Jan 2007 01:29:02 +0100 (MET)
X-BeenThere: haskell-c...@haskell.org
X-Mailman-Version: 2.1.5
List-Id: The Haskell Cafe <haskell-cafe.haskell.org>
List-Unsubscribe: <http://www.haskell.org/mailman/listinfo/haskell-cafe>,
	<mailto:haskell-cafe-requ...@haskell.org?subject=unsubscribe>
List-Archive: <http://www.haskell.org/pipermail/haskell-cafe>
List-Post: <mailto:haskell-c...@haskell.org>
List-Help: <mailto:haskell-cafe-requ...@haskell.org?subject=help>
List-Subscribe: <http://www.haskell.org/mailman/listinfo/haskell-cafe>,
	<mailto:haskell-cafe-requ...@haskell.org?subject=subscribe>
Original-CC: "haskell-c...@haskell.org" <haskell-c...@haskell.org>
Original-Date: Mon, 8 Jan 2007 19:28:51 -0500
Original-Message-Id: <786CB009-AD68-4169-A642-E95EDF79D536@augustsson.net>
Original-References: <ad0e24930701071431u30a12554lf2f9e683e1b81...@mail.gmail.com>
	<B31251DF-3AD6-47ED-9641-AC2790227...@augustsson.net>
	<20070108131342.GA5630@lambda>
	<ad0e24930701080551t1e28349ct8718941646e9f...@mail.gmail.com>

Thanks!  I'm sure I could have figured this out by looking at the code,
but it was easier to ask.
It's very cool example, even if it doesn't practical. :)

	-- Lennart

On Jan 8, 2007, at 08:51 , Jim Apple wrote:

> On 1/8/07, Tomasz Zielonka <tomasz.zielo...@gmail.com> wrote:
>> On Mon, Jan 08, 2007 at 08:02:36AM -0500, Lennart Augustsson wrote:
>> > So it sounds to me like the (terminating) type
>> > checker solves the halting problem.  Can you please explain  
>> which part
>> > of this I have  misunderstood?
>>
>> Perhaps you, the user, have to encode the proof of halting in the way
>> you construct the term?
>
> 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.
>
> Jim
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-C...@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-C...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe