Mutually recursive datatypes

[yihozhang]

Currently, datatypes cannot be mutually recursive. For example, the following is not allowed

(datatype Foo
  (foo Bar))

(datatype Bar
  (bar Foo))

OCaml supports mutually recursive type with the type ... and ... keyword. We can probably do something similar:

(datatype Foo
  (foo Bar)
and      Bar
  (bar Foo))

Or

(datatype Foo
  (foo Bar)
 andalso  Bar
  (bar Foo))

Or

(datatype*
  Foo
    (foo Bar)
  Bar
    (bar Foo))

Or (Jul 25 updates: we are more in favor of this syntax)

(datatype*
  (Foo
    (foo Bar))
  (Bar
    (bar Foo)))

Or maybe there is a better syntax for this?

---

Another pattern we commonly have (but is not supported) is

(datatype Expr
    (Call String VecExpr))
(sort VecExpr (Vec Expr))

Our recursive datatypes should also have a good support for this.

[saulshanabrook]

FWIW in the Python bindings mutually recursive data types are supported through late binding type annotations. All classes/datatypes are translated to plain sort definitions & functions.

[oflatt]

One advantage of this proposal is that it would still allow mutually recursive data types even if we made datatype closed, instead of open as it is now

[saulshanabrook]

Thought: Could make all types "lazy", that would support recursive data.... With the current syntax, then we just defer processing until it's defined.