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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe