What, if anything, do you need to add to a dependent type system to get a module system?

Question

Dependent type systems seem to support some of the uses of a ML module system. What do you get out of a module system that you do not get out of dependent records?

module ~ record

signature ~ record type

functor ~ function on records

module with an abstract type component ~ dependent record with a type field

I'm interested in how well this works as a module system, and if and how you could integrate features such as applicative functors and mixins.

Answer 1

First, a few disclaimers:

• Different languages in the ML family have somewhat different implementations of the module system. For that matter, different implementations of the same language have differences. In this answer, I'll focus exclusively on Standard ML as specified in The Definition of Standard ML (Revised).

• Likewise, different dependently-typed languages have different features.

• I'm not as knowledgeable about dependent types as I could be. I think I understand them enough for purposes of this answer, but of course, we don't always know what we don't know. :-)

• This sort of question is more subjective than it might seem, because it's not always obvious what actually counts as a thing that you "get".

  • For an example of what I mean: Standard ML defines fun ... by showing how to transform it to val rec .... So you could easily argue that the 'fun' syntax doesn't "get" you anything, since anything you can write with the 'fun' syntax is something you can easily write with the 'val rec' syntax; but apparently the language designers felt that it does get you something — clarity, convenience, cleanness, whatever — because otherwise they wouldn't have bothered to define this form that they clearly understood was equivalent.

  • This is especially true for the module system. Many of the features of Standard ML modules are actually achievable with just the Standard ML "core" — no need for dependent types, even — except that modules provide a much pleasanter syntax and encourage modular design. Even functors, which you compare to functions on records, aren't quite like regular functions, in that you can't "call" them inside an expression, so they can't appear in loops or conditions, they can't call themselves recursively (which is just as well since the recursion would necessarily be infinite), and so on. Is this a limitation of functors, potentially fixable by a more general approach? Or would a more general approach make it less pleasant to use functors the way they're intended? I think a case can be made either way.

  So, I'll just call out a few features that make Standard ML modules good at their job, and that aren't, to my limited knowledge, provided by current dependently-typed languages (and that even if they were, wouldn't be inherent consequences of having dependent types). You can judge for yourself which ones, if any, really "count".

---

value constructors

A structure can contain not just types and values, but also value constructors, which can be used in pattern matching. For example, you can write things like this:

fun map f List.nil = List.nil   | map f List.cons (h, t) = List.cons (f h, map f t) 

where a pattern uses a value constructor from a structure. I don't think there's an essential reason that a dependent type system couldn't support this, but it seems awkward.

Likewise, structures can contain exceptions, which, same story.

---

'open' declarations

An open declaration copies the entirety of a structure — all the values, types, nested structures, etc. — into the current environment, which can be either the top-level environment or a smaller scope (such as local or let).

One use of this is to define a structure that enriches another structure (or even the "same" structure, in that the new one can have the same name and thereby shadow the old binding). For example, if I write:

structure List = struct   open List    fun map f nil = nil     | map f cons (h, t) = cons (f h, map f t) end 

then List now has all of the bindings it had before, plus a new List.map (which may replace a previously-defined List.map). (Likewise, I can use an include specification to augment a signature, though for that one I probably would not reuse the same name.)

Of course, even without this feature, you could also write a series of declarations like datatype list = datatype List.list, val hd = List.hd, etc., to copy everything out of a structure; but I think you'll agree that open List is much clearer, less error-prone, and more robust in the face of future changes.

There are languages that have this sort of operation for records — for example, JavaScript's spread/rest syntax, starting in ECMAScript 2018, lets you copy all fields from an existing object to a new one, adding or replacing as desired — but I'm not sure if any dependently-typed languages have it.

---

flexible matching

In Standard ML, a structure matches a signature even if it has extra bindings not specified by the signature, or if it has bindings that are more polymorphic than what is specified by the signature, or the like.

This means that a functor can require only what it actually needs, and still be used with structures that also have other things the functor doesn't care about. (This is in contrast to regular functions; val first = # 1 only cares about the first element of a tuple, but its type has to specify exactly how many elements are in the tuple.)

In a dependently-typed language, this would amount to a kind of subtype relation. I don't know if any dependently-typed languages have it — it wouldn't surprise me — but certainly some don't.

---

projection and abstraction

Continuing on the previous point: when you match a structure to a signature, the result is (if I may simplify a bit) the "projection" of the structure onto the subspace specified by the signature, that is, the structure "minus" whatever is not specified by the signature.

This effectively "hides" aspects of the structure, analogously to how you might use 'private' in a language like C++ or Java.

You can even have 'friends' (in the C++ sense) by initially defining the structure more openly, and then rebinding the same structure identifier more narrowly:

structure Foo = struct   ... end  ... code with unfettered access to the contents of Foo ...  structure Foo = Foo :> FOO  ... code with access only to what's specified by FOO ... 

Because you can define a signature very precisely, you have a high degree of granularity here in what you expose and how. The grammar lets you refine a signature on-the-fly (for example, FOO where type foo = int is a valid signature expression), and because it's often desired to retain all types without making them abstract, there's a simple syntax for that (for example, Foo : FOO is roughly equivalent to Foo :> FOO where type foo = Foo.foo and type bar = Foo.bar and ...).

In a dependently-typed language that supported flexible matching via subtyping (above), some of this would probably come together with that; but I list it separately, and call out the syntactic conveniences, in order to highlight how Standard ML modules serve their intended purposes.

---

Well, that's probably enough examples to show the idea. If you don't feel that any of the above really "count", then listing more features probably wouldn't change that. :-)