[Haskell-cafe] GADTs are expressive

[Lennart Augustsson]

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.zielonka at 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-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe