[Top] [All Lists]

 ```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 <[email protected]> wrote: > 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 > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe ```