Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005878OCamlOCaml typingpublic2013-01-09 10:292014-06-04 22:02
Reporterfrisch 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityhave not tried
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0005878: Forward type declarations as an alternative to recursive modules
DescriptionRecursive 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0008726)
lpw25 (developer)
2013-01-09 16:40
edited on: 2013-01-09 16:41

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

(0008765)
garrigue (manager)
2013-01-17 04:18

This would break the current typing of GADTs, which assumes that abstract types defined in the current module are never aliases.
(0008770)
frisch (developer)
2013-01-17 08:35

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?
(0009176)
gasche (developer)
2013-04-22 11:08

In relation to the discussion in PR#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.)
(0009193)
frisch (developer)
2013-04-23 12:04

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...
(0009197)
gasche (developer)
2013-04-23 15:38

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.
(0009326)
bobot (reporter)
2013-05-23 16:47

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
(0010550)
frisch (developer)
2013-10-31 11:34

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.
(0010551)
garrigue (manager)
2013-10-31 14:45

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".
(0010552)
frisch (developer)
2013-10-31 15:05

> 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.
(0010553)
garrigue (manager)
2013-10-31 15:23

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.
(0010554)
frisch (developer)
2013-10-31 16:39

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).
(0010555)
lpw25 (developer)
2013-10-31 21:59
edited on: 2013-10-31 22:00

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.

(0010556)
garrigue (manager)
2013-11-01 00:52

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.
(0010557)
lpw25 (developer)
2013-11-01 02:06
edited on: 2013-11-01 03:50

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


- Issue History
Date Modified Username Field Change
2013-01-09 10:29 frisch New Issue
2013-01-09 16:40 lpw25 Note Added: 0008726
2013-01-09 16:41 lpw25 Note Edited: 0008726 View Revisions
2013-01-17 04:18 garrigue Note Added: 0008765
2013-01-17 08:35 frisch Note Added: 0008770
2013-04-22 11:08 gasche Note Added: 0009176
2013-04-23 12:04 frisch Note Added: 0009193
2013-04-23 15:38 gasche Note Added: 0009197
2013-05-23 16:47 bobot Note Added: 0009326
2013-06-19 12:09 doligez Status new => feedback
2013-10-31 11:34 frisch Note Added: 0010550
2013-10-31 11:34 frisch Status feedback => new
2013-10-31 14:45 garrigue Note Added: 0010551
2013-10-31 15:05 frisch Note Added: 0010552
2013-10-31 15:23 garrigue Note Added: 0010553
2013-10-31 16:39 frisch Note Added: 0010554
2013-10-31 21:59 lpw25 Note Added: 0010555
2013-10-31 22:00 lpw25 Note Edited: 0010555 View Revisions
2013-10-31 22:00 lpw25 Note Edited: 0010555 View Revisions
2013-11-01 00:52 garrigue Note Added: 0010556
2013-11-01 02:06 lpw25 Note Added: 0010557
2013-11-01 03:50 lpw25 Note Edited: 0010557 View Revisions
2014-06-04 22:02 doligez Status new => acknowledged


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker