Modify a couple of error messages slightly
[ghc.git] / testsuite / tests / gadt / termination.hs
1 {-# LANGUAGE GADTs, RankNTypes #-}
2
3 module Termination where
4
5 {- Message from Jim Apple to Haskell-Cafe, 7/1/07
6
7 To show how expressive GADTs are, the datatype Terminating can hold
8 any term in the untyped lambda calculus that terminates, and none that
9 don't. I don't think that an encoding of this is too surprising, but I
10 thought it might be a good demonstration of the power that GADTs
11 bring.
12
13
14 Using GADTs to encode normalizable and non-normalizable terms in
15 the lambda calculus. For definitions of normalizable and de Bruin
16 indices, I used:
17
18 Christian Urban and Stefan Berghofer - A Head-to-Head Comparison of
19 de Bruijn Indices and Names. In Proceedings of the International
20 Workshop on Logical Frameworks and Meta-Languages: Theory and
21 Practice (LFMTP 2006). Seattle, USA. ENTCS. Pages 46-59
22
23 http://www4.in.tum.de/~urbanc/Publications/lfmtp-06.ps
24
25 @incollection{ pierce97foundational,
26 author = "Benjamin Pierce",
27 title = "Foundational Calculi for Programming Languages",
28 booktitle = "The Computer Science and Engineering Handbook",
29 publisher = "CRC Press",
30 address = "Boca Raton, FL",
31 editor = "Allen B. Tucker",
32 year = "1997",
33 url = "citeseer.ist.psu.edu/pierce95foundational.html"
34 }
35
36 > So it sounds to me like the (terminating) type checker solves the
37 > halting problem. Can you please explain which part of this I have
38 > misunderstood?
39
40 The Terminating datatype takes three parameters:
41 1. A term in the untyped lambda calculus
42 2. A sequence of beta reductions
43 3. A proof that the result of the beta reductions is normalized.
44
45 Number 2 is the hard part. For a term that calculated the factorial of
46 5, the list in part 2 would be at least 120 items long, and each one
47 is kind of a pain.
48
49 GHC's type checker ends up doing exactly what it was doing before:
50 checking proofs.
51
52 -}
53
54
55 -- Terms in the untyped lambda-calculus with the de Bruijn representation
56
57 data Term t where
58 Var :: Nat n -> Term (Var n)
59 Lambda :: Term t -> Term (Lambda t)
60 Apply :: Term t1 -> Term t2 -> Term (Apply t1 t2)
61
62 -- Natural numbers
63
64 data Nat n where
65 Zero :: Nat Z
66 Succ :: Nat n -> Nat (S n)
67
68 data Z
69 data S n
70
71 data Var t
72 data Lambda t
73 data Apply t1 t2
74
75 data Less n m where
76 LessZero :: Less Z (S n)
77 LessSucc :: Less n m -> Less (S n) (S m)
78
79 data Equal a b where
80 Equal :: Equal a a
81
82 data Plus a b c where
83 PlusZero :: Plus Z b b
84 PlusSucc :: Plus a b c -> Plus (S a) b (S c)
85
86 {- We can reduce a term by function application, reduction under the lambda,
87 or reduction of either side of an application. We don't need this full
88 power, since we could get by with normal-order evaluation, but that
89 required a more complicated datatype for Reduce.
90 -}
91 data Reduce t1 t2 where
92 ReduceSimple :: Replace Z t1 t2 t3 -> Reduce (Apply (Lambda t1) t2) t3
93 ReduceLambda :: Reduce t1 t2 -> Reduce (Lambda t1) (Lambda t2)
94 ReduceApplyLeft :: Reduce t1 t2 -> Reduce (Apply t1 t3) (Apply t2 t3)
95 ReduceApplyRight :: Reduce t1 t2 -> Reduce (Apply t3 t1) (Apply t3 t2)
96
97 {- Lift and Replace use the de Bruijn operations as expressed in the Urban
98 and Berghofer paper. -}
99 data Lift n k t1 t2 where
100 LiftVarLess :: Less i k -> Lift n k (Var i) (Var i)
101 LiftVarGTE :: Either (Equal i k) (Less k i) -> Plus i n r -> Lift n k (Var i) (Var r)
102 LiftApply :: Lift n k t1 t1' -> Lift n k t2 t2' -> Lift n k (Apply t1 t2) (Apply t1' t2')
103 LiftLambda :: Lift n (S k) t1 t2 -> Lift n k (Lambda t1) (Lambda t2)
104
105 data Replace k t n r where
106 ReplaceVarLess :: Less i k -> Replace k (Var i) n (Var i)
107 ReplaceVarEq :: Equal i k -> Lift k Z n r -> Replace k (Var i) n r
108 ReplaceVarMore :: Less k (S i) -> Replace k (Var (S i)) n (Var i)
109 ReplaceApply :: Replace k t1 n r1 -> Replace k t2 n r2 -> Replace k (Apply t1 t2) n (Apply r1 r2)
110 ReplaceLambda :: Replace (S k) t n r -> Replace k (Lambda t) n (Lambda r)
111
112 {- Reflexive transitive closure of the reduction relation. -}
113 data ReduceEventually t1 t2 where
114 ReduceZero :: ReduceEventually t1 t1
115 ReduceSucc :: Reduce t1 t2 -> ReduceEventually t2 t3 -> ReduceEventually t1 t3
116
117 -- Definition of normal form: nothing with a lambda term applied to anything.
118 data Normal t where
119 NormalVar :: Normal (Var n)
120 NormalLambda :: Normal t -> Normal (Lambda t)
121 NormalApplyVar :: Normal t -> Normal (Apply (Var i) t)
122 NormalApplyApply :: Normal (Apply t1 t2) -> Normal t3 -> Normal (Apply (Apply t1 t2) t3)
123
124 -- Something is terminating when it reduces to something normal
125 data Terminating where
126 Terminating :: Term t -> ReduceEventually t t' -> Normal t' -> Terminating
127
128 {- We can encode terms that are non-terminating, even though this set is
129 only co-recursively enumerable, so we can't actually prove all of the
130 non-normalizable terms of the lambda calculus are non-normalizable.
131 -}
132
133 data Reducible t1 where
134 Reducible :: Reduce t1 t2 -> Reducible t1
135 -- A term is non-normalizable if, no matter how many reductions you have applied,
136 -- you can still apply one more.
137 type Infinite t1 = forall t2 . ReduceEventually t1 t2 -> Reducible t2
138
139 data NonTerminating where
140 NonTerminating :: Term t -> Infinite t -> NonTerminating
141
142 -- x
143 test1 :: Terminating
144 test1 = Terminating (Var Zero) ReduceZero NormalVar
145
146 -- (\x . x)@y
147 test2 :: Terminating
148 test2 = Terminating (Apply (Lambda (Var Zero))(Var Zero))
149 (ReduceSucc (ReduceSimple (ReplaceVarEq Equal (LiftVarGTE (Left Equal) PlusZero))) ReduceZero)
150 NormalVar
151
152 -- omega = \x.x@x
153 type Omega = Lambda (Apply (Var Z) (Var Z))
154 omega = Lambda (Apply (Var Zero) (Var Zero))
155
156 -- (\x . \y . y)@(\z.z@z)
157 test3 :: Terminating
158 test3 = Terminating (Apply (Lambda (Lambda (Var Zero))) omega)
159 (ReduceSucc (ReduceSimple (ReplaceLambda (ReplaceVarLess LessZero))) ReduceZero)
160 (NormalLambda NormalVar)
161
162 -- (\x.x@x)(\x.x@x)
163 test4 :: NonTerminating
164 test4 = NonTerminating (Apply omega omega) help3
165
166 help1 :: Reducible (Apply Omega Omega)
167 help1 = Reducible (ReduceSimple
168 (ReplaceApply (ReplaceVarEq Equal (LiftLambda
169 (LiftApply (LiftVarLess LessZero) (LiftVarLess LessZero))))
170 (ReplaceVarEq Equal (LiftLambda (LiftApply
171 (LiftVarLess LessZero) (LiftVarLess LessZero))))))
172
173 help2 :: ReduceEventually (Apply Omega Omega) t -> Equal (Apply Omega Omega) t
174 help2 ReduceZero = Equal
175 help2 (ReduceSucc (ReduceSimple (ReplaceApply
176 (ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _))))
177 (ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _)))))) y)
178 = case help2 y of
179 Equal -> Equal
180
181 help3 :: Infinite (Apply Omega Omega)
182 help3 x = case help2 x of
183 Equal -> help1