Negatively recursive data types

[Koen Claessen]

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.