Re: [Haskell-cafe] GADTs are expressive
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. John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
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
Re: [Haskell-cafe] GADTs are expressive
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. Best regards Tomasz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
On 1/8/07, Tomasz Zielonka [EMAIL PROTECTED] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
On Mon, 8 Jan 2007 08:51:40 -0500 Jim Apple [EMAIL PROTECTED] 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. -- Robin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
On 1/8/07, Robin Green [EMAIL PROTECTED] wrote: On Mon, 8 Jan 2007 08:51:40 -0500 Jim Apple [EMAIL PROTECTED] 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. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
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? Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
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. :) -- Lennart On Jan 8, 2007, at 08:51 , Jim Apple wrote: On 1/8/07, Tomasz Zielonka [EMAIL PROTECTED] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] GADTs are expressive
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 = [EMAIL PROTECTED]
type Omega = Lambda (Apply (Var Z) (Var Z))
omega = Lambda (Apply (Var Zero) (Var Zero))
-- (\x . \y . y)@([EMAIL PROTECTED])
test3 :: Terminating
test3 = Terminating (Apply (Lambda (Lambda (Var Zero))) omega)
(ReduceSucc (ReduceSimple
