
Dear All,
Recently, I've been playing with selfapplication and fixedpoint
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 Fomega, 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 Fomega.
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
_______________________________________________
HaskellCafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskellcafe

