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)