# Negatively recursive data types

**Koen Claessen
**
koen@cs.chalmers.se

*Thu, 5 Jul 2001 08:55:14 +0200 (MET DST)*

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.