New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Forward type declarations as an alternative to recursive modules #5878
Comments
Comment author: @lpw25 While not ideal, a similar thing can be done using my "extensible types" extension: type nodeset = ..
type node =
{
uid: int;
children: nodeset;
}
module NodeSet = Set.Make(struct
type t = node
let compare n1 n2 = n1.uid - n2.uid
end)
type nodeset += Set of NodeSet.t By enclosing this in a module the "openness" of nodeset can be hidden, so that Set is guaranteed to be the only constructor of nodeset. Of course, this means that all references to the set must be matched against both Set and a default case (to avoid warnings for non-exhaustive matches). |
Comment author: @garrigue This would break the current typing of GADTs, which assumes that abstract types defined in the current module are never aliases. |
Comment author: @alainfrisch Jacques: I guess that if we can keep in the environment the information that the type is "currently" a forward declaration and not really an abstract type, this would address the problem with the typing of GADTs. Do you agree? |
Comment author: @gasche In relation to the discussion in #5985 (I'm not saying the issues themselves are related), I have grown a mistrust for the use of "abstract types defined in the current module" for strong inequalities when used as phantom types of GADTs: this property cannot be properly propagated through a signature boundary, and therefore breaks composability. My guess would be that this use of abstract-implementation types will become deprecated before any decision is made on this forward-declaration feature. I have a mild sympathy with the proposal. There are a lot of satellite proposals of foward-declaration stuff, notably:
Maybe none of them seems vital enough to warrant a language change, but together they paint a picture of a feature where signature items are accepted as structure items, and (except for let-and-let where shadowing is resolved by ordering) the static semantics of such repetitions is the least upper bound in precision. (I would be fine with arbitrary restrictions designed to avoid any change in the dynamic semantics, in particular requiring that a 'val foo : ...' is always followed by a structure item introducing the corresponding 'let foo = ...', to avoid any recursion considerations.) |
Comment author: @alainfrisch For values, the second declaration must be an instance of the first one, but the first one should be exported in the interface:
For my proposal of forward types, the second declaration is again an instance of the first one, but it should be the second one which should be exported in the interface (the interface could itself use a forward declaration if needed): So I don't see immediately how to combine the two ideas... |
Comment author: @gasche My idea was to take in any case the "intersection" (that's what I maybe confusingly called least upper-bound) of "definedness" of both sentences (forgetting about the let-shadowing behaviour). If Similarly, you could define a variance or injectivity annotation in the "forward declaration" of the type, and have it checked against the latter definition, and incorporated into the final signature. I think this "intersection of definedness" idea is consistent with both forward types and val+let. But I don't want to torpedo your proposal with additional debatable things. |
Comment author: bobot Another example where you want to introduce circularity between type declarations is between module types and data types. For the syntax can't the "rec ... and" construct be extended to different kind of definition? (I used "and type" "and let" because otherwise it seems that give rise to ambiguity) module type S = sig
val c: int -> TSet.t
end
and type foo =
A of (module S)
and module TSet = Set.Make(struct
type t = foo
let compare n1 n2 = .. compare_set ..
end)
and let compare_set s1 s2 = TSet.compare s1 s2 |
Comment author: @alainfrisch I'm wondering if our type and module system experts have an opinion about the usefulness and feasibility of this "forward-type declaration" proposal. Xavier, Jacques? Providing a simpler replacement to many uses of recursive modules sounds very compelling to me. |
Comment author: @garrigue To be honest, I don't like this kind of approach, which makes the static semantics work as if it were dynamic. This said, extensible types proposed by lpw25 allow to do that, and I find it less shocking in that context. |
Comment author: @alainfrisch
Are you referring to issues related to injectivity?
They'd force to pattern match everywhere (and the matching cannot be exhaustive). But in essence, what I'm asking for is a restriction of extensible types with exactly one single extension (and it must be in the structure defining the type). With this restriction, the spurious pattern matching disappear. |
Comment author: @garrigue What's wrong with the recursive module approach? |
Comment author: @alainfrisch Given the number of small bugs and issues with recursive modules, with no resolution plan, I feel more and more uncomfortable relying on them. Moreover, it doesn't feel right to rely on the module system to allow recursion between base language features (e.g. recursion between a class and a data type). |
Comment author: @lpw25 I quite like this feature: in OCaml we have the ability to abstract over type equalities, and this seems like a good use of that ability. If you think of Alain's example as: module F (X : sig type nodeset end) = struct
type node =
{
uid: int;
children: X.nodeset;
}
module NodeSet = Set.Make(struct
type t = node
let compare n1 n2 = n1.uid - n2.uid
end)
end;;
module rec M : sig type nodeset = F(M).NodeSet.t end = M;; then it seems like a simple form of abstraction. If, however, people don't like it, then bobot's proposal also seems reasonable. |
Comment author: @garrigue Yes, this is a form of abstraction. type t = forward This is fundamentally different from all the other abstractions you get in the language. If the problem is that recursive modules are not specified, then maybe we should get Xavier in a corner, and ask for some subset of recursive modules that are guaranteed to work. For me one point of recursive modules (and first class modules) is that they avoid cluttering the base language with ad hoc features to express things that are better understood at the module level. By the way, Bobot's proposal would be very nice, the only trouble is that we don't know how to implement it. There are just too many interactions to allow it without requiring type annotations. |
Comment author: @lpw25
I this just a case of requiring modules to have signatures, like: type node =
{
uid: int;
children: NodeSet.t;
}
and module NodeSet : Set.S with type elt = node = Set.Make(struct
type t = node
let compare n1 n2 = n1.uid - n2.uid
end) because that would still be a really nice feature. In general, it would be nice if all definitions could be preceded by As a side note, it would also be good if all definitions could be done locally using a syntax similar to local modules (e.g. |
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. |
Original bug ID: 5878
Reporter: @alainfrisch
Status: acknowledged (set by @damiendoligez on 2014-06-04T20:02:58Z)
Resolution: open
Priority: normal
Severity: feature
Category: typing
Monitored by: @diml bobot @jberdine
Bug description
Recursive modules are often used only to introduce circularity between type declarations. A typical example is the definition of a tree data structure where each node contains a set of nodes:
Another typical use of recursive modules is to create recursion between a data type and a class type.
For these uses, recursive modules introduce heavy syntax, type-checking subtleties which are hard to understand for the programmer. And recursive modules are not yet fully understood/supported (i.e. there are several pending bugs with no clear resolution plan).
I wonder whether a more basic language feature wouldn't be better for those typical uses of recursive modules mentioned above: forward type declarations. The idea is to allow declaring a type name in a structure (or signature) but only give its actual definition later in the same structure. In between, the type is considered as being abstract.
We could introduce an explicit syntax:
or simply use the syntax for abstract type declaration:
(Currently, this is rejected, because a type name can only be defined once in a structure/signature, so this does not change the meaning of existing well-typed programs.)
The example above could then be written:
Here I assumed that it would be ok to define a forward type as a type abbreviation. I'm not 100% sure this would be safe. It not, we could only allow concrete definitions, but we would still be able to write:
On the implementation side, the basic strategy could be to reuse the same Ident.t as for the forward type when inserting the concrete declaration in the environment. I haven't fully thought about the implications of this proposal, maybe there are some tricky aspects to it, but I've the intuition that this feature would be easier to understand (both for users and for language developers) than recursive modules.
The text was updated successfully, but these errors were encountered: