Haskell type system and Barendregt's Lambda Cube classification
Dear All, Recently, I've been playing with self-application and fixed-point combinators definition in Haskell. It is possible to type them in Haskell using recursive types. I took Y & U combinators:
newtype Rec a = In { out :: Rec a -> a }
u :: Rec a -> a u x = out x x
y :: (a -> a) -> a y f = let uf = f . u in uf (In uf)
Recursive types are part of System F-omega, which corresponds to lambda omega in Barendregt's Lambda Cube. For all type systems in Lambda Cube it is proven that they are strongly normalizing. But using "y" I can easily construct a term even without a normal form. So, I got a contradition and conclude that type system implementation in Haskell contains something, that is absent from System F-omega. My question is: what's particular feature in Haskell type system, that breaks strong normalization property? Or am I totally wrong classifying it in terms of Lambda Cube? Best regards, Vladimir Ivanov
On Friday 25 December 2009 11:35:38 am Vladimir Ivanov wrote:
Dear All,
Recently, I've been playing with self-application and fixed-point combinators definition in Haskell.
It is possible to type them in Haskell using recursive types.
I took Y & U combinators:
newtype Rec a = In { out :: Rec a -> a }
u :: Rec a -> a u x = out x x
y :: (a -> a) -> a y f = let uf = f . u in uf (In uf)
Recursive types are part of System F-omega, which corresponds to lambda omega in Barendregt's Lambda Cube. For all type systems in Lambda Cube it is proven that they are strongly normalizing. But using "y" I can easily construct a term even without a normal form.
So, I got a contradition and conclude that type system implementation in Haskell contains something, that is absent from System F-omega.
My question is: what's particular feature in Haskell type system, that breaks strong normalization property? Or am I totally wrong classifying it in terms of Lambda Cube?
General recursive types are not part of F_omega. It only has... 1) Type functions of arbitrary order /\ F : * -> *. /\ T : *. F T 2) Universal quantification over the above spaces Pi F : * -> *. Pi T : (* -> *) -> *. T F You can encode inductive and coinductive types in such a type system. If F is the shape functor, then the encoding of the inductive type is: Pi R : *. (F R -> R) -> R and the encoding of the coinductive type is: Ex R : *. F R * R where: Ex R : *. T[R] = Pi Q : *. (Pi R : *. T[R] -> Q) -> Q and: A * B = Pi R : *. (A -> B -> R) -> R (and A + B = Pi R : *. (A -> R) -> (B -> R) -> R if you need it to encode F R, although often one may be able to massage F into a more suitable form to avoid using the * and + encodings). However, as you can imagine, Rec cannot be encoded. Allowing such types adds general recursion back in. In type theories that do support Haskell-alike algebraic/(co)inductive definitions (which none in the lambda cube do; they're plain lambda calculi), the total ones restrict what types you can declare (to strictly positive types, usually) to make types like Rec illegal. -- Dan
Thanks for the thorough answer, Dan.
That's exactly what I was looking for.
During further search, I stumbled on an excellent introductory
description of recursive types in a draft of Robert Harper's book
"Programming Languages: Theory and Practice"
http://www.cs.cmu.edu/~rwh/plbook/book.pdf
-- vi
On Fri, Dec 25, 2009 at 10:48 PM, Dan Doel
On Friday 25 December 2009 11:35:38 am Vladimir Ivanov wrote:
Dear All,
Recently, I've been playing with self-application and fixed-point combinators definition in Haskell.
It is possible to type them in Haskell using recursive types.
I took Y & U combinators:
newtype Rec a = In { out :: Rec a -> a }
u :: Rec a -> a u x = out x x
y :: (a -> a) -> a y f = let uf = f . u in uf (In uf)
Recursive types are part of System F-omega, which corresponds to lambda omega in Barendregt's Lambda Cube. For all type systems in Lambda Cube it is proven that they are strongly normalizing. But using "y" I can easily construct a term even without a normal form.
So, I got a contradition and conclude that type system implementation in Haskell contains something, that is absent from System F-omega.
My question is: what's particular feature in Haskell type system, that breaks strong normalization property? Or am I totally wrong classifying it in terms of Lambda Cube?
General recursive types are not part of F_omega. It only has...
1) Type functions of arbitrary order /\ F : * -> *. /\ T : *. F T 2) Universal quantification over the above spaces Pi F : * -> *. Pi T : (* -> *) -> *. T F
You can encode inductive and coinductive types in such a type system. If F is the shape functor, then the encoding of the inductive type is:
Pi R : *. (F R -> R) -> R
and the encoding of the coinductive type is:
Ex R : *. F R * R
where:
Ex R : *. T[R] = Pi Q : *. (Pi R : *. T[R] -> Q) -> Q
and:
A * B = Pi R : *. (A -> B -> R) -> R
(and
A + B = Pi R : *. (A -> R) -> (B -> R) -> R
if you need it to encode F R, although often one may be able to massage F into a more suitable form to avoid using the * and + encodings).
However, as you can imagine, Rec cannot be encoded. Allowing such types adds general recursion back in. In type theories that do support Haskell-alike algebraic/(co)inductive definitions (which none in the lambda cube do; they're plain lambda calculi), the total ones restrict what types you can declare (to strictly positive types, usually) to make types like Rec illegal.
-- Dan
participants (2)
-
Dan Doel -
Vladimir Ivanov