#1999: panic with GADT etc.
----------------------------+-----------------------------------------------
Reporter: jeltsch | Owner: chak
Type: bug | Status: closed
Priority: normal | Milestone: 6.10 branch
Component: Compiler | Version: 6.9
Resolution: fixed | Keywords:
Testcase: T1999, T1999a | Blockedby:
Difficulty: Unknown | Os: Linux
Blocking: | Architecture: x86
Failure: None/Unknown |
----------------------------+-----------------------------------------------
Changes (by simonpj):
* failure: => None/Unknown
Comment:
Here is another example of the usefulness of decomposing type
applications, due to Jim Apple, and recorded in test `gadt/termination`:
{{{
{-# LANGUAGE GADTs, Rank2Types #-}
module Termination where
{- Message from Jim Apple to Haskell-Cafe, 7/1/07
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.
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"
}
> 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?
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.
-}
-- 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
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1999#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
