Skip to content
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

Closed
vicuna opened this issue Jan 9, 2013 · 16 comments
Closed

Forward type declarations as an alternative to recursive modules #5878

vicuna opened this issue Jan 9, 2013 · 16 comments

Comments

@vicuna
Copy link

vicuna commented Jan 9, 2013

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:

module rec Node : sig
  type t =
      {
       uid: int;
       children: NodeSet.t;
      }
end = Node and NodeSet : Set.S with type elt = Node.t = Set.Make(struct
  type t = Node.t
  let compare n1 n2 = n1.Node.uid - n2.Node.uid
end)

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:

  type t = forward
  ...
  type t := ...

or simply use the syntax for abstract type declaration:

  type t
  ...
  type t  = ...

(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:

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 = NodeSet.t

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:

type node
let forward_compare = ref (fun _ _ -> assert false)
module NodeSet = Set.Make(struct
  type t = node
  let compare n1 n2 = !forward_compare n1 n2
end)
type node = {uid: int; children: NodeSet.t}
let () = forward_compare := (fun n1 n2 -> n1.uid - n2.uid)

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.

@vicuna
Copy link
Author

vicuna commented Jan 9, 2013

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).

@vicuna
Copy link
Author

vicuna commented Jan 17, 2013

Comment author: @garrigue

This would break the current typing of GADTs, which assumes that abstract types defined in the current module are never aliases.

@vicuna
Copy link
Author

vicuna commented Jan 17, 2013

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?

@vicuna
Copy link
Author

vicuna commented Apr 22, 2013

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:

  • people ( http://www.reddit.com/r/ocaml/comments/1btqg5/specifying_type_signatures_haskell_vs_ocaml/ ) requesting the ability to use 'val : ...' before the corresponding 'let ...' to have strong polymorphic annotations in implementation files as well, as in Haskell

  • the present suggestion by Alain

  • his recent change to allow abstract module types (module type S;;) in structure items

  • some problems we have when playing with 'include' at the module level, where it is correct to shadow a let/val, but not a type or module declaration; this forces us to use subtle signature tricks when sometimes the redundancy is obviously safe, because the two declarations are identical or in a subtyping relation (one is more general than the other) and we could give a natural meaning to the redeclaration (take the least-upper-bound in precision)

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.)

@vicuna
Copy link
Author

vicuna commented Apr 23, 2013

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:

  • val x: ...
  • let x = ...

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...

@vicuna
Copy link
Author

vicuna commented Apr 23, 2013

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 val provides a precise type (polymorphic or monomorphic) but no dynamic meaning, and let provides a "less defined" inferred type with inferred type variables, but a dynamic meaning (a program term), the end result would be the precise typing of the val combined with the precise dynamic semantics of the let. And as you know that from the start, you can even propagate the annotation of the val when type-checking the let.

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.

@vicuna
Copy link
Author

vicuna commented May 23, 2013

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

@vicuna
Copy link
Author

vicuna commented Oct 31, 2013

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.

@vicuna
Copy link
Author

vicuna commented Oct 31, 2013

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.
And I wouldn't expect Xavier to like it more.
Remember also all the problems we already have with abstract types. This would only add more.

This said, extensible types proposed by lpw25 allow to do that, and I find it less shocking in that context.
In particular extensible types are variant types from the beginning, so they are less "unknown".

@vicuna
Copy link
Author

vicuna commented Oct 31, 2013

Comment author: @alainfrisch

Remember also all the problems we already have with abstract types. This would only add more.

Are you referring to issues related to injectivity?

extensible types

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.

@vicuna
Copy link
Author

vicuna commented Oct 31, 2013

Comment author: @garrigue

What's wrong with the recursive module approach?
It is true there are some subtle cases with recursive modules, but this is not the case here.

@vicuna
Copy link
Author

vicuna commented Oct 31, 2013

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).

@vicuna
Copy link
Author

vicuna commented Oct 31, 2013

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.

@vicuna
Copy link
Author

vicuna commented Oct 31, 2013

Comment author: @garrigue

Yes, this is a form of abstraction.
And abstraction requires a binder and a scope.
Here they are indicated by

type t = forward
...
type t := ...

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.

@vicuna
Copy link
Author

vicuna commented Nov 1, 2013

Comment author: @lpw25

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.

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 and to be used in a mutually recursive set of definitions, even if some of them (e.g. modules) required explicit type annotations.

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. let exception E of int in).

@github-actions
Copy link

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant