Negatively recursive data types

Lars Henrik Mathiesen
4 Jul 2001 18:20:32 -0000

> From: Keith Wansbrough <>
> 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:

> 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:

> 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

Lars Mathiesen (U of Copenhagen CS Dep) <> (Humour NOT marked)