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.