[Haskell-cafe] GADTs are expressive

7 views
Skip to first unread message

Jim Apple

unread,
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.

{-# 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

Lennart Augustsson

unread,
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?

-- Lennart

Tomasz Zielonka

unread,
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?

Perhaps you, the user, have to encode the proof of halting in the way
you construct the term? Just guessing.

Best regards
Tomasz

Jim Apple

unread,
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?

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

Robin Green

unread,
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.

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

Jim Apple

unread,
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.

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

Roberto Zunino

unread,
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.

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.

Lennart Augustsson

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

-- Lennart

Jim Apple

unread,
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?

I think Tim Sheard uses strictness in his Omega project for the same
reason you suggest. See

http://web.cecs.pdx.edu/~sheard/

Jim

John Meacham

unread,
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

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