[Haskell-cafe] GADTs are expressive
Lennart Augustsson
lennart at augustsson.net
Mon Jan 8 08:02:36 EST 2007
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
More information about the Haskell-Cafe
mailing list