6 Apr
2007
6 Apr
'07
5:41 a.m.
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