On Thu, Apr 05, 2007 at 06:26:17PM -0300, Felipe Almeida Lessa wrote: > I know that types like > > >data T = T (T -> T) > > are inhabitated by things other than bottom (like id or \_ -> > undefined), but can it be useful for *anything*?
Yes. In particular, types like those can produce an explicit embedding of general recursion. There is a world of difference between not having a proof of strong normalization, and having a proof that strong normalization does not hold. If you don't like theory, then I'll say that you can use types like those to embed typeless lambda calculi in Haskell. Stefan _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
