[Haskell-cafe] Haskell type system and Barendregt's Lambda Cube
classification
Vladimir Ivanov
vladimir.v.ivanov at gmail.com
Fri Dec 25 11:35:36 EST 2009
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
More information about the Haskell-Cafe
mailing list