; The following types implement the natural numbers,
; using simplest kind of recursion (a single feature SUCC).
; A fully specified natural number is a chain of feature structures of type "pos",
; eventually terminating in a feature structure of type "zero".
natnum := *top*.
zero := natnum.
pos := natnum &
  [ SUCC natnum ].

; The following types implement an identity function on the natural numbers,
; in the sense that, for any feature structure compatible with "natnum",
; unifying that feature structure with "natnum-with-copy"
; will produce the original feature structure under RESULT.
natnum-with-copy := natnum &
  [ RESULT natnum ].
zero-with-copy := zero & natnum-with-copy &
  [ RESULT zero ].
pos-with-copy := pos & natnum-with-copy &
  [ SUCC.RESULT #diagonal,
    RESULT.SUCC #diagonal ].

; The following types implement a defective subtype of "natnum",
; in the sense that "defective-natnum" does not have a common subtype with "zero".
defective-natnum := natnum.
defective-pos := defective-natnum & pos.

; The following types extend the copying function to the defective type.
; However, note that defectiveness is shifted along the number by one:
; "defective-natnum-with-copy" has a RESULT that is just "natnum";
; "defective-pos-with-copy" enforces defectiveness on its RESULT.SUCC.
defective-natnum-with-copy := defective-natnum & natnum-with-copy.
defective-pos-with-copy := defective-natnum-with-copy & defective-pos & pos-with-copy &
  [ RESULT.SUCC defective-natnum ].

; The following are wrapper types, holding a natural number under NATNUM.
; "natnum-with-copy-wrapper" holds the copy operation.
; "defective-one-wrapper" holds the number one (it has one SUCC),
; but where the "pos" is defective.
natnum-wrapper := *top* &
  [ NATNUM natnum ].
natnum-with-copy-wrapper := natnum-wrapper &
  [ NATNUM natnum-with-copy ].
defective-one-wrapper := natnum-wrapper &
  [ NATNUM defective-pos & [ SUCC zero ]].

; The following type would apply the copy operation to the defective number one.
; This would cause a unification failure:
; NATNUM.RESULT.SUCC must be of type "defective-natnum";
; NATNUM.SUCC.RESULT must be of type "zero";
; the above two paths must be re-entrant;
; and there is no common subtype of "defective-natnum" and "zero".
; (Intuitively, the operation pushes the defectiveness along by one,
; but defectiveness is not allowed at the end of the number.)
; Note that neither of the above paths exist in the parent types
; "natnum-with-copy-wrapper" and "defective-one-wrapper".
;fail-wrapper := natnum-with-copy-wrapper & defective-one-wrapper.

; If the above type is uncommented, the LKB correctly throws an error when compiling.
; However, leaving the above type commented out,
; interactive unification of the values of NATNUM
; from "natnum-with-copy-wrapper" and "defective-one-wrapper"
; displays an incorrect result (it does not enforce all the constraints).

; When there is a well-defined result, interactive unification
; does not seem to have a problem with recursive type constraints.
; For example, we can fix the defective type by adding the following two types:
;defective-zero := defective-natnum & zero.
;defective-zero-with-copy := defective-natnum-with-copy & defective-zero & zero-with-copy.

; If these two types are uncommented, interactive unification produces the correct result.
; Similarly, if all three types ("fail-wrapper", "defective-zero", "defective-zero-with-copy")
; are uncommented, the LKB correctly compiles.