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)