On Mon, Jan 08, 2007 at 09:48:09PM +0100, Roberto Zunino wrote:
> Robin Green wrote:
> >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 a
On 1/8/07, Roberto Zunino <[EMAIL PROTECTED]> wrote:
Does anyone else believe that using strictess annotations in GADT proof
terms would be good style?
I think Tim Sheard uses strictness in his Omega project for the same
reason you suggest. See
http://web.cecs.pdx.edu/~sheard/
Jim
___
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 <[EMAIL PROTECTED]> wrote:
On Mon, Jan 08, 2007
Robin Green wrote:
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 deman
On 1/8/07, Robin Green <[EMAIL PROTECTED]> wrote:
On Mon, 8 Jan 2007 08:51:40 -0500
"Jim Apple" <[EMAIL PROTECTED]> wrote:
> 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
On Mon, 8 Jan 2007 08:51:40 -0500
"Jim Apple" <[EMAIL PROTECTED]> 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
On 1/8/07, Tomasz Zielonka <[EMAIL PROTECTED]> 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 us
On Mon, Jan 08, 2007 at 08:02:36AM -0500, Lennart Augustsson wrote:
> So Terminating contains all the terminating terms in the untyped
> lambda calculus and none of the non-terminating ones. And the type
> checker checks this. So it sounds to me like the (terminating) type
> checker solves the h
So Terminating contains all the terminating terms in the untyped lambda
calculus and none of the non-terminating ones. And the type checker
checks
this. So it sounds to me like the (terminating) type checker solves the
halting problem. Can you please explain which part of this I have
misun
To show how expressive GADTs are, the datatype Terminating can hold
any term in the untyped lambda calculus that terminates, and none that
don't. I don't think that an encoding of this is too surprising, but I
thought it might be a good demonstration of the power that GADTs
bring.
{-# OPTIONS -fg
10 matches
Mail list logo
