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
@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
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 Haskell-C...@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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?
> 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
> @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
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.
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 Apple" <jbapple+haskell-c...@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.
On 1/8/07, Robin Green <gree...@greenrd.org> wrote:
> On Mon, 8 Jan 2007 08:51:40 -0500 > "Jim Apple" <jbapple+haskell-c...@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.
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?
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. :)
> 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.
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.
