Forward type definitions

[alainfrisch]

A proposal to add "forward type definitions", allowing in particular mutually recursive type definitions to be split into multiple compilation units.

[lpw25]

I think this PR tries to address a genuine problem. The motivation and technical details are pretty clear in the description. All in all a pretty good first RFC for the repo.

I think the main thing missing from this RFC is a description of drawbacks and alternatives. I think it is important that RFC authors try to include these as well, since they are an important part of any decision.

Some apparent drawbacks of this proposal might be:

• The use of a flat global namespace -- i.e. the string literals -- separate from the existing namespacing mechanism of the language.

• The need for a global linearity check to ensure soundness

• The incompatibility of the linearity check with functors, local modules, etc.

Some possible alternatives include:

• Library based approaches. We have a library at Jane St that lets you declare a type to be defined later -- you call a function along the lines of val define_exn : unit -> ('a, t) eq to define the type t as equal to 'a and it will fail with an exception if called a second time. Obviously this is more awkward to use than this proposal but has the advantage of requiring no changes to the language.

• Avoiding the additional namespace of strings by having an explicit declaration syntax for the type and then using that in place of a string literal.

• Using some genuine recursion. As the description says, you are modelling your solution on using references to mimic recursion. Instead we could consider supporting actual recursion.

The last of these alternatives is particularly relevant as I have been working with @OCamlPro-Couderc on a proposal to support just such recursion. I'll try to write that proposal up as its own RFC in the next few days.

[alainfrisch]

In terms of processes, I thought the goal was to discuss and agree or reject a document that specifies, in more or less details, a solution to be implemented. So the RFC itself would only describe the target solution, and the discussion around the merits, drawbacks and alternative would be part of the discussion in the PR (and I should have listed drawbacks in the PR description indeed). Do you have a different understanding?

We have a library at Jane St

Is this something public, and if so, could you share a reference? I can imagine this is based on a generative functor producing a fresh abstract type, plus its define_exn function (with a runtime linearity check); is that right?

At least as a temporary workaround before we get full recursion in the language, this solution might indeed works well, and support higher-level abstractions than my proposal.

One problem I can foresee is the lack of "global opening of GADT", which would allow:

type (_, _) eq = Eq: ('a,'a) eq

module F(X : sig type t type s val x : t val y: s val eq: (t, s) eq end) = struct
  let Eq = X.eq
  let _ = (X.x = X.y)
end

One needs to open X.eq locally, which might become cumbersome. The code above currently fails with:

4 |   let Eq = X.eq
               ^^^^
Error: This expression has type (X.t, X.s) eq
       but an expression was expected of type (X.t, X.t) eq
       Type X.s is not compatible with type X.t

Does this bite you in practice when using your library? Do you think one could imagine extending support for GADTs opening to support code as above, or are there deep problems here?

Using some genuine recursion

Looking forward to reading your forthcoming RFC. One critical point, in some contexts at least, is to preserve separate compilation and incrementality of the build.

[lpw25]

Do you have a different understanding?

I had a slightly different understanding, where the document describes both the solution to be implemented and a summary of the main considerations that lead to that choice. So we would discuss alternatives, advantages and drawbacks in the PR and then include outlines of those in the document itself.

This is based on how the Rust RFC process seems to work -- their RFC template:

https://github.com/rust-lang/rfcs/blob/master/0000-template.md

explicitly includes sections for these bits and it does seem to be helpful.

I'm open to doing things either way, but we should try to decide which approach we want to take and then update the Readme to reflect the decision.

Is this something public, and if so, could you share a reference?

I'm afraid it isn't in our open source libraries.

I can imagine this is based on a generative functor producing a fresh abstract type, plus its define_exn function (with a runtime linearity check); is that right?

I haven't looked in close detail, but that is my understanding of how it works.

Does this bite you in practice when using your library?

My understanding is that this is indeed a bit annoying but not terrible. You kind of start every function with let Eq = eq in ... .

Do you think one could imagine extending support for GADTs opening to support code as above, or are there deep problems here?

I think you definitely could add such support. The tricky part is that you need to check some things about any types which escape the scope of a GADT equation, so we'd need to do that for everything defined in the module after that point. I think that is just work to do rather than something fundamentally difficult, but I haven't thought too deeply about it.

@garrigue, @trefis, do you have some idea of what "global opening of GADTs" would entail?

[lpw25]

Looking forward to reading your forthcoming RFC.

See #3

[garrigue]

@garrigue, @trefis, do you have some idea of what "global opening of GADTs" would entail?

Sorry for the very slow answer.
In theory there is nothing wrong with global opening of GADTs inside implementations.
Allowing it in interfaces (including exporting from an implementation) would require new signature syntax to express the added equations.
The interactions between static and dynamic aspects may require some care, but I see no problem a priori.

Note also that the nominal types proposal (#4) allows witnesses to add equations to parameterized abstract types.

This said, a GADT based approach is not only heavy-weight, it may also be very dangerous if you start using Obj.magic: one can deduce a lot from a GADT equation.

The more natural approach is to use functors (this is exactly what they are about), combined with recursive modules. It would be interesting to see where it becomes intractable to use them.