[Haskell-cafe] GADTs are expressive

[Lennart Augustsson]

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


On Jan 7, 2007, at 17:31 , Jim Apple wrote:

> 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 at x
> type Omega = Lambda (Apply (Var Z) (Var Z))
> omega = Lambda (Apply (Var Zero) (Var Zero))
>
> -- (\x . \y . y)@(\z.z at z)
> test3 :: Terminating
> test3 = Terminating (Apply (Lambda (Lambda (Var Zero))) omega)
>        (ReduceSucc (ReduceSimple (ReplaceLambda (ReplaceVarLess
> LessZero))) ReduceZero)
>        (NormalLambda NormalVar)
>
> -- (\x.x at x)(\x.x at 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
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe