r6research (r6research) wrote,


After attending the second St Jacob's workshop I think I now understand all the pieces that make up a good module system; though I might not understand how they all fit together yet.

There is also a notable distinction between modular programming and module systems, which turn out to only be loosely related. Modular programming is about isolating software components and using narrow interfaces to communicate between them, while a module system is about assembling larger software modules from smaller modules.

Modules are dependent records / typing contexts for some type system. Modules are abstract over the the exact details of the type system which makes the notion quite versatile. All that is needed for the type system is that it supports variable declarations and substitution. It is also very convenient from both a theoretical and a practical point of view that modules support manifest entries / definitions.

Modules are related to each other through views. A view from a module A to a module B is an assignment of expressions of the type theory in the context A for every declaration in the module B. Thus if you have an instance of a module A you can derive an instance of a module B by substituting the free variables in the expression in B with the value in A. Indeed, one can define an instance of a module A to be a view from the empty context to a module A.

Extensions form an important class of views. An extension from module A to module B is a view where each expression for module B is a unique variable name from module A.

Modules can be combined together to create new modules. I think the Mathscheme project has found a good set of combinators that can be used to create new modules: extend, combine extensions, and mixin a view over an extension (I will discuss rename later as it isn't exactly a combinator, since it only produces isomorphic modules). The empty module gets things started. Arguably combine can be defined as a mixin, but it is probably better to consider it as a separate operation.

It strikes me that where most existing module systems go wrong is by taking inclusions too seriously. Inclusions are special types of extensions where each variable assignment is identical to the variable being assigned (note, it is only possible to define inclusions when modules are *not* take up to alpha equivalence). Inclusions have several nice properties: in particular there is at most one inclusion between any two modules, so inclusions form a partial order out of the modules.

I think module systems tend to only allow combine and mixins over inclusions rather than arbitrary extensions. The problem is that a structure like Ring, is an extension of Monoid in two different ways. Both cannot be inclusions since there is a most one inclusion between two modules. The usual symptom of this problem is that abelian monoids are unrelated to monoids, and rings become a composition of these two distinct structures.

Typeclasses are dependent records that are combined with a type inference mechanism. While type inference is important, it is an orthogonal issue. SSreflect type classes are dependent records that use coercions and canonical structures to define extensions and views (in some way that haven't fully worked out). Coq's coercion mechanism works best when they form a partial order, so ssreflect appears to suffer from the inclusion problem.

Spitters and van der Weegen's pebble style type-classes is a combination of modules being dependent records and typing contexts. The domain of a view is a typing context while the codomain is a dependent record. I haven't considered their module system in detail yet.
  • Post a new comment


    default userpic
    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.