[Haskell] Fixpoint combinator without recursion
stefanor at cox.net
Thu Apr 5 17:41:09 EDT 2007
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.
More information about the Haskell