7 views

Skip to first unread message

Jan 7, 2007, 5:31:39 PM1/7/07

to haskel...@haskell.org

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.

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 -fglasgow-exts #-}

{- Using GADTs to encode normalizable and non-normalizable terms in

the lambda calculus. For definitions of normalizable and de Bruin

indices, I used:

Christian Urban and Stefan Berghofer - A Head-to-Head Comparison of

de Bruijn Indices and Names. In Proceedings of the International

Workshop on Logical Frameworks and Meta-Languages: Theory and

Practice (LFMTP 2006). Seattle, USA. ENTCS. Pages 46-59

http://www4.in.tum.de/~urbanc/Publications/lfmtp-06.ps

@incollection{ pierce97foundational,

author = "Benjamin Pierce",

title = "Foundational Calculi for Programming Languages",

booktitle = "The Computer Science and Engineering Handbook",

publisher = "CRC Press",

address = "Boca Raton, FL",

editor = "Allen B. Tucker",

year = "1997",

url = "citeseer.ist.psu.edu/pierce95foundational.html"

}

-}

module Terminating where

-- Terms in the untyped lambda-calculus with the de Bruijn representation

data Term t where

Var :: Nat n -> Term (Var n)

Lambda :: Term t -> Term (Lambda t)

Apply :: Term t1 -> Term t2 -> Term (Apply t1 t2)

-- Natural numbers

data Nat n where

Zero :: Nat Z

Succ :: Nat n -> Nat (S n)

data Z

data S n

data Var t

data Lambda t

data Apply t1 t2

data Less n m where

LessZero :: Less Z (S n)

LessSucc :: Less n m -> Less (S n) (S m)

data Equal a b where

Equal :: Equal a a

data Plus a b c where

PlusZero :: Plus Z b b

PlusSucc :: Plus a b c -> Plus (S a) b (S c)

{- We can reduce a term by function application, reduction under the lambda,

or reduction of either side of an application. We don't need this full

power, since we could get by with normal-order evaluation, but that

required a more complicated datatype for Reduce.

-}

data Reduce t1 t2 where

ReduceSimple :: Replace Z t1 t2 t3 -> Reduce (Apply (Lambda t1) t2) t3

ReduceLambda :: Reduce t1 t2 -> Reduce (Lambda t1) (Lambda t2)

ReduceApplyLeft :: Reduce t1 t2 -> Reduce (Apply t1 t3) (Apply t2 t3)

ReduceApplyRight :: Reduce t1 t2 -> Reduce (Apply t3 t1) (Apply t3 t2)

{- Lift and Replace use the de Bruijn operations as expressed in the Urban

and Berghofer paper. -}

data Lift n k t1 t2 where

LiftVarLess :: Less i k -> Lift n k (Var i) (Var i)

LiftVarGTE :: Either (Equal i k) (Less k i) -> Plus i n r -> Lift

n k (Var i) (Var r)

LiftApply :: Lift n k t1 t1' -> Lift n k t2 t2' -> Lift n k (Apply

t1 t2) (Apply t1' t2')

LiftLambda :: Lift n (S k) t1 t2 -> Lift n k (Lambda t1) (Lambda t2)

data Replace k t n r where

ReplaceVarLess :: Less i k -> Replace k (Var i) n (Var i)

ReplaceVarEq :: Equal i k -> Lift k Z n r -> Replace k (Var i) n r

ReplaceVarMore :: Less k (S i) -> Replace k (Var (S i)) n (Var i)

ReplaceApply :: Replace k t1 n r1 -> Replace k t2 n r2 -> Replace

k (Apply t1 t2) n (Apply r1 r2)

ReplaceLambda :: Replace (S k) t n r -> Replace k (Lambda t) n (Lambda r)

{- Reflexive transitive closure of the reduction relation. -}

data ReduceEventually t1 t2 where

ReduceZero :: ReduceEventually t1 t1

ReduceSucc :: Reduce t1 t2 -> ReduceEventually t2 t3 ->

ReduceEventually t1 t3

-- Definition of normal form: nothing with a lambda term applied to anything.

data Normal t where

NormalVar :: Normal (Var n)

NormalLambda :: Normal t -> Normal (Lambda t)

NormalApplyVar :: Normal t -> Normal (Apply (Var i) t)

NormalApplyApply :: Normal (Apply t1 t2) -> Normal t3 -> Normal

(Apply (Apply t1 t2) t3)

-- Something is terminating when it reduces to something normal

data Terminating where

Terminating :: Term t -> ReduceEventually t t' -> Normal t' -> Terminating

{- We can encode terms that are non-terminating, even though this set is

only co-recursively enumerable, so we can't actually prove all of the

non-normalizable terms of the lambda calculus are non-normalizable.

-}

data Reducible t1 where

Reducible :: Reduce t1 t2 -> Reducible t1

-- A term is non-normalizable if, no matter how many reductions you

have applied,

-- you can still apply one more.

type Infinite t1 = forall t2 . ReduceEventually t1 t2 -> Reducible t2

data NonTerminating where

NonTerminating :: Term t -> Infinite t -> NonTerminating

-- x

test1 :: Terminating

test1 = Terminating (Var Zero) ReduceZero NormalVar

-- (\x . x)@y

test2 :: Terminating

test2 = Terminating (Apply (Lambda (Var Zero))(Var Zero))

(ReduceSucc (ReduceSimple (ReplaceVarEq Equal (LiftVarGTE

(Left Equal) PlusZero))) ReduceZero)

NormalVar

-- omega = \x.x@x

type Omega = Lambda (Apply (Var Z) (Var Z))

omega = Lambda (Apply (Var Zero) (Var Zero))

-- (\x . \y . y)@(\z.z@z)

test3 :: Terminating

test3 = Terminating (Apply (Lambda (Lambda (Var Zero))) omega)

(ReduceSucc (ReduceSimple (ReplaceLambda (ReplaceVarLess

LessZero))) ReduceZero)

(NormalLambda NormalVar)

-- (\x.x@x)(\x.x@x)

test4 :: NonTerminating

test4 = NonTerminating (Apply omega omega) help3

help1 :: Reducible (Apply Omega Omega)

help1 = Reducible (ReduceSimple (ReplaceApply (ReplaceVarEq Equal

(LiftLambda (LiftApply (LiftVarLess LessZero) (LiftVarLess

LessZero)))) (ReplaceVarEq Equal (LiftLambda (LiftApply (LiftVarLess

LessZero) (LiftVarLess LessZero))))))

help2 :: ReduceEventually (Apply Omega Omega) t -> Equal (Apply Omega Omega) t

help2 ReduceZero = Equal

help2 (ReduceSucc (ReduceSimple (ReplaceApply (ReplaceVarEq _

(LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _))))

(ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess

_)))))) y) =

case help2 y of

Equal -> Equal

help3 :: Infinite (Apply Omega Omega)

help3 x =

case help2 x of

Equal -> help1

_______________________________________________

Haskell-Cafe mailing list

Haskel...@haskell.org

http://www.haskell.org/mailman/listinfo/haskell-cafe

Jan 8, 2007, 8:03:13 AM1/8/07

to Jim Apple

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

misunderstood?

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

misunderstood?

-- Lennart

Jan 8, 2007, 8:14:06 AM1/8/07

to Lennart Augustsson

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 halting problem. Can you please explain which part

> of this I have misunderstood?

> 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 misunderstood?

Perhaps you, the user, have to encode the proof of halting in the way

you construct the term? Just guessing.

Best regards

Tomasz

Jan 8, 2007, 8:52:01 AM1/8/07

to haskel...@haskell.org

On 1/8/07, Tomasz Zielonka <tomasz....@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?

> 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

Jan 8, 2007, 12:11:28 PM1/8/07

to Jim Apple

On Mon, 8 Jan 2007 08:51:40 -0500

"Jim Apple" <jbapple+ha...@gmail.com> 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. 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 Apple" <jbapple+ha...@gmail.com> 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. 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.

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 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)

or (3) and fool the typechecker into thinking that (1) terminates, when

it doesn't.

--

Robin

Jan 8, 2007, 12:21:47 PM1/8/07

to haskel...@haskell.org

On 1/8/07, Robin Green <gre...@greenrd.org> wrote:

> On Mon, 8 Jan 2007 08:51:40 -0500

> "Jim Apple" <jbapple+ha...@gmail.com> 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 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.

> On Mon, 8 Jan 2007 08:51:40 -0500

> "Jim Apple" <jbapple+ha...@gmail.com> 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 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.

Of course. Were there a recursion-free dialect of Haskell, it could be

typecheck/proofcheck the Terminating datatype, though it would be

useless for doing any actual work. Proof assistants like Coq can solve

this dilemma, and so can languages in the Dependent ML family, by

allowing non-terminating programs but only terminating proofs, and by

proving termination by well-founded induction.

Nobody should think Haskell+GADTs provides the sort of assurances that

these can.

Jim

Jan 8, 2007, 3:49:13 PM1/8/07

to gre...@greenrd.org

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 demanding

> terminates, you will get a value of the correct type.

> 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 demanding

> terminates, you will get a value of the correct type.

I only want to point out that the above "terminates" actually is "can be

put in NF", since putting the expression in WHNF is not enough. In other

words, you need deepSeq, not seq when forcing/checking proofs.

To partially mitigate this problem, I believe strictness annotations can

be used, as in

data Nat t where

Z :: Nat Zero

S :: ! Nat t -> Nat (Succ t)

Now one could safely write

foo :: Nat t -> A t -> B

foo proof value = proof `seq`

-- here you can assume t to be a finite type-level natural

If proof is invalid, foo will return _|_.

Using no strictess annotation, but still using seq instead of deepSeq,

the code above would be unsafe, since one can always pass (S undefined)

as proof.

Using seq also allows to check the proof in constant time (neglecting

the proof generation time, of course). deepSeq instead would require

traversing the proof each time one wants to check it, e.g. in different

functions.

Does anyone else believe that using strictess annotations in GADT proof

terms would be good style?

Zun.

Jan 8, 2007, 7:29:19 PM1/8/07

to Jim Apple

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. :)

but it was easier to ask.

It's very cool example, even if it doesn't practical. :)

-- Lennart

Jan 8, 2007, 7:34:34 PM1/8/07

to haskel...@haskell.org

On 1/8/07, Roberto Zunino <zun...@di.unipi.it> wrote:

> Does anyone else believe that using strictess annotations in GADT proof

> terms would be good style?

> 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

Jan 23, 2007, 11:18:14 PM1/23/07

to haskel...@haskell.org

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 actually

> >get is a "partial proof" - that *if* the expression you are demanding

> >terminates, you will get a value of the correct type.

>

> I only want to point out that the above "terminates" actually is "can be

> put in NF", since putting the expression in WHNF is not enough. In other

> words, you need deepSeq, not seq when forcing/checking proofs.

>

> To partially mitigate this problem, I believe strictness annotations can

> be used, as in

> 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 demanding

> >terminates, you will get a value of the correct type.

>

> I only want to point out that the above "terminates" actually is "can be

> put in NF", since putting the expression in WHNF is not enough. In other

> words, you need deepSeq, not seq when forcing/checking proofs.

>

> To partially mitigate this problem, I believe strictness annotations can

> be used, as in

jhc allows (in special cases at the moment, in full generality hopefully

soon) the declaration of new strict boxed types.

> data StrictList a :: ! = Cons a (StrictList a) | Nil

I think this could be used to help the situation, as absence analysis

can discard unused portions since there is no need to deepSeq

everything.

John

--

John Meacham - ⑆repetae.net⑆john⑈

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu