typesmoduleocamlsml

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


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.


Solution

  • First, a few disclaimers:


    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.:: (h, t) = List.:: (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 op:: (h, t) = op:: (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. :-)