Negatively recursive data types

[Lars Henrik Mathiesen]

> From: Keith Wansbrough <Keith.Wansbrough@cl.cam.ac.uk>
> Date: Wed, 04 Jul 2001 18:27:05 +0100
> 
> Hi... I'm currently looking at the semantics of recursive data types.  
> One thing that Haskell allows, but the semantics for it is very hairy, 
> is *negatively* recursive data types.  That is, data types where the 
> recursion occurs to the left of a function arrow.  For example:
> 
> This example is not a very good one.  Does anyone have an example of a 
> useful data type involving negative recursion?

There's a trick you can use to port the fixpoint operator from untyped
lambda calculus:

Untyped:
> fix f = (\x -> f (x x))  (\x -> f (x x))

This doesn't work in Hindley-Milner type systems, of course, since the
lambda-bound x's need to have two different types at the same time. So
we have to help the type checker, like this:

Haskell:
> data Fix a = F (Fix a) -> a
> 
> fix :: (a -> a) -> a
> fix f = (\(F x) -> f (x (F x))) (F (\(F x) -> f (x (F x))))

At least it worked in Miranda(TM). But I don't know if it counts as
useful.

Lars Mathiesen (U of Copenhagen CS Dep) <thorinn@diku.dk> (Humour NOT marked)