# Negatively recursive data types

**Lars Henrik Mathiesen
**
thorinn@diku.dk

*4 Jul 2001 18:20:32 -0000*

>* 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)