Comment author: @gasche

Jacques, do you know what the restriction is there for soundness? If this is simply a productivity restriction (all cycles through the definitions have to be guarded by at least one constructor), I would be curious to maybe look at implementing this.

Comment author: skaller

Cyclic dependence can't be allowed though:

type a = [A | b] and b = [B | a]

Also, if the types involved are parametric, a different kind
of cycle might be present:

type a = [`A | a t] (* some type t with parameter *)

Comment author: @garrigue

The restriction is not for soundness, but removing it would introduce some symmetry issue.
I.e., should we only allow including definitions occurring before (while these are recursive definitions), or do something more clever (topological sorting)?
Note that first behavior coincides with what is done for class types (and even classes?)
IIRC, this issue was discussed when I introduced this feature, and the consensus among developers was that it was better just to forbid it. In particular some people were insistent that the behavior with class types was not a good reason to do it for polymorphic variants.

On simple cases, the work around is the same as with combinations of class types and normal types: make the definition you want to include parametric in those that will use it.

type 'e t_ = [A of 'e t_ | B of 'e]
type t = e t
and e = [e t_ | C of t | D of e | `E]

But of course, depending on the mutual dependencies, this may be harder to write.

Comment author: skaller

Unfortunately the workaround is not always viable.
I actually looked at doing this in my particular code.

For reference here is the file:

https://github.com/felix-lang/felix/blob/master/src/compiler/flx_core/flx_ast.ml

and the type which is "copied" is typecode_t, lines 65 to 127, copied into expr_t, lines 145 to 330. It is, I think, possible in this case but cut and paste was just a lot easier and more reliable.

In my language Felix everything is automatically mutually recursive and polymorphic variants in Felix can use abbreviations of any polymorphic type. The compiler simply keeps a trail, and bombs out if it finds a circularity.

In C++, member functions can call others that aren't defined yet, the compiler does a pass to find the interfaces first, then a second pass. A recursive type definition can be handled the same way. In fact probably one pass is enough if you use back-patching. C has no problem with incomplete types, its embarrassing that C does recursion better than Ocaml!

Comment author: @gasche

Jacques: my proposal was to allow mutually-recursive declarations as long as cycles between the type names are guarded by ocurring under a constructor (which guarantees that the definition is "productive" in the usual sense, that there exists a unique infinite unfolding). So

type t = [u | ...]
and u = [t | ...]

would be rejected, but

type t = [u | ...]
and u = [`Foo of (.. t ...) | ...]

would be accepted.

I think that we don't need a full topological sort to decide this, but we do need to check that the graph of the "inherits from" relation between the recursive definitions is acyclic. We can also do this for classes.

Comment author: @garrigue

Actually you need a full topological sort, because polymorphic variant expansion is a purely syntactic feature: expansion is done immediately when translating the type, so the type you include must be already defined. Same problem for classes.

Comment author: @gasche

I see.

If I understand correctly:

• The expansion you mention is done in the Rinherit case of typetexp.ml: the reference to the inherited type is kept (goes into ctype_desc), but the global/inlined set of fields/variants is computed at the same time (goes into ctype_type).

• The way recursive declaration blocks are handled by Typedecl.transl_type_decl is to first add "unitialized" bindings for the block type names in the typing environment, whose definitions are fresh unification variables, compute "real" type-checked declarations in this environment (so (non-dereferencing) references to mutually-defined types are accepted), and backpatch the typing environment with these a-posteriori computations.

The two-phase approach of typedecl wouldn't quite work here without a topological sort, because Rinherit typing would encounter an inherited type name whose fields are not yet known, so their expansion could not be precomputed.

Conceptually might be possible to extend to a three-phase approach (delaying the computation of the final list of fields in ctype_type to after all the ctype_type have been computed in the temporary environment), but this sounds like an invasive change to the current approach, while a second phase in topological order suffices and would be easier to implement (if we do it right, it may not even change the actual traversal order in all currently-accepted cases).

Comment author: skaller

As an added issue (heh): if you're "doing it for polymorphic variants" and "doing it for classes" can't that be included to "do it for mixed types and classes"?

Its the same kind of problem: lack of recursion. Sometimes a term algebra needs to include class types as arguments, and the classes have methods with terms of the algebra as arguments.

Also .. I am wondering if there is a syntax which "automates" open recursion. Consider you have 10 mutually recursive types, then to open them each needs 10 parameters. Then you need to close them in a recursion with each taking 10 arguments. Fine. But, suppose you want to change something, add a type or add a constructor .. thats a LOT of editing to get right. Especially if you're adding a 2 constructors, 2 new types, and modifying some things. And that's just the types. If you have open/closed functions as well they have to all be edited as well. What i'm getting at is that if there is a systematic way to take a bunch of recursive types and open/close them .. then there has to be an automatic algorithm that does it as well (if only we can dream up syntax for it).

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.