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: data Neg a b = MkNeg (a -> Neg a b -> b) Here (Neg a b) occurs to the left of the function arrow. Some members of this data type might be: n1, n2 :: Neg Int [Int] n1 = MkNeg (\ x _ -> [x]) n2 = MkNeg (\ x (MkNeg f) -> x : f (x+1) n1) This example is not a very good one. Does anyone have an example of a useful data type involving negative recursion? Thanks. --KW 8-)
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)
Lars Henrik Mathiesen wrote:
From: Keith Wansbrough <Keith.Wansbrough@cl.cam.ac.uk>
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?
data Fix a = F (Fix a) -> a
You can find this and some related examples in Erik Meijer and Graham Hutton. Bananas in space: Extending fold and unfold to exponential types. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture (FPCA'95), pages 324-333. ACM Press, 1995. The paper also discusses some hairy details of recursive data types ;-) Olaf -- OLAF CHITIL, Dept. of Computer Science, University of York, York YO10 5DD, UK. URL: http://www.cs.york.ac.uk/~olaf/ Tel: +44 1904 434756; Fax: +44 1904 432767
Keith Wansbrough wondered: | Does anyone have an example of a useful data type | involving negative recursion? Here is an example straight from practice. If we want to implement a datatype of predicate logic formulas, it is convenient to use higher-order syntax: type Name = String data Form = Form :& Form | Form :| Form | Not Form | All (Term -> Form) | Exi (Term -> Form) | Pred Name [Term] -- predicate symbols (this is pretty standard) Then, we would like to implement the Term datatype. A simple implementation would be: data Term = Fun Name [Term] | Var Name (this is also pretty standard) Now, suppose we want to implement Hilbert's epsilon quantifier; this is a way to represent terms with a certain property. For example: eps x . (x + 7 = 8) Is the term x that satisfies "x + 7 = 8", i.e. 1. One could simpy add this as a constructor to the Term datatype: data Term = Fun Name [Term] | Var Name | Eps (Term -> Form) Et voilá, there you have a directly negatively recursive datatype. /Koen.
participants (4)
-
Keith Wansbrough -
Koen Claessen -
Lars Henrik Mathiesen -
Olaf Chitil