41

The ML module system stands as a high-water mark of programming language support for data abstraction. However, superficially, it seems that it can easily be encoded in an object-oriented language that supports abstract type members. For example, we can encode the elements of SML module system in Scala as follows:

  • SML signatures: Scala traits with no concrete members
  • SML structures with given signatures: Scala objects extending given traits
  • SML functors parameterised by given signatures: Scala classes taking objects extending given traits as constructor arguments

Are there any significant features such an encoding would miss? Anything that can be expressed in SML modules that encoding can't express? Any guarantees that SML makes that this encoding would not be able to make?

narthi
  • 2,188
  • 1
  • 16
  • 27

1 Answers1

52

There are a few fundamental differences that you cannot overcome easily:

  • ML signatures are structural types, Scala traits are nominal: an ML signature can be matched by any appropriate module after the fact, for Scala objects you need to declare the relation at definition time. Likewise, subtyping between ML signatures is fully structural. Scala refinements are closer to structural types, but have some rather severe limitations (e.g., they cannot reference their own local type definitions, nor contain free references to abstract types outside their scope).

  • ML signatures can be composed structurally using include and where. The resulting signature is equivalent to the inline expansion of the respective signature expression or type equation. Scala's mixin composition, while more powerful in many ways, again is nominal, and creates an inequivalent type. Even the order of composition matters for type equivalence.

  • ML functors are parameterised by structures, and thereby by both types and values, Scala's generic classes are only parameterised by types. To encode a functor, you would need to turn it into a generic function, that takes the types and the values separately. In general, this transformation -- called phase-splitting in the ML module literature -- cannot be limited to just definitions and uses of functors, because at their call-sites it has to be applied recursively to nested structure arguments; this ultimately requires that all structures are consistently phase-split, which is not a style you want to program in manually. (Neither is it possible to map functors to plain functions in Scala, since functions cannot express the necessary type dependencies between parameter and result types. Edit: since 2.10, Scala has support for dependent methods, which can encode some examples of SML's first-order generative functors, although it does not seem possible in the general case.)

  • ML has a general theory of refining and propagating "translucent" type information. Scala uses a weaker equational theory of "path-dependent" types, where paths denote objects. Scala thereby trades ML's more expressive type equivalences for the ability to use objects (with type members) as first-class values. You cannot easily have both without quickly running into decidability or soundness issues.

  • Edit: ML can naturally express abstract type constructors (i.e., types of higher kind), which often arise with functors. For Scala, higher kinds have to be activated explicitly, which are more challenging for its type system, and apparently lead to undecidable type checking.

The differences become even more interesting when you move beyond SML, to higher-order, first-class, or recursive modules. We briefly discuss a few issues in Section 10.1 of our MixML paper.

Andreas Rossberg
  • 34,518
  • 3
  • 61
  • 72
  • All nice points. I find it weird that datatype and exception generativity was not mentioned, though. – isekaijin Apr 16 '14 at 11:46
  • @EduardoLeón, I didn't mention them because they are pretty much orthogonal to modules. And they don't really add anything fundamentally new to the picture: datatype generativity is no different from the (static) generativity of abstract types, and exception generativity is no different from the (dynamic) generativity of references or objects. – Andreas Rossberg Apr 16 '14 at 15:15
  • Nice summary. Just one remark: Later versions of Scala admit dependent function types. So it seems your third point of difference above no longer applies. Do you agree? – Martin Odersky Jul 27 '14 at 16:35
  • @MartinOdersky: Maybe. I seem to be running into "error: Parameter type in structural refinement may not refer to an abstract type defined outside that refinement" as soon as I try to encode a functor whose body refers to a type from a parameter. Moreover, I get "error: can't existentially abstract over parameterized type" when returning a (used) type constructor without sealing. Also, I had to activate -language:higherKinds as soon as I define type constructors in functors. (Is there an up-to-date spec that defines dependent methods? Scala-lang still points to the 2.9 spec.) – Andreas Rossberg Jul 30 '14 at 12:58
  • @AndreasRossberg I'd be curious to see your code that's failing, if you wanted to paste it somewhere! – copumpkin Aug 02 '14 at 01:14
  • 1
    @copumpkin, e.g. try a trivial toy functor like `functor F(X : ORD) = struct fun eq(x, y) = X.leq(x, y) andalso X.leq(y, x) end` (for the obvious definition of `ORD`) -- its direct translation to Scala would be `def F(X : ORD) = new { def eq(x : X.T, y : X.T) = X.leq(x, y) && X.leq(y, x) }`, which doesn't type-check. – Andreas Rossberg Aug 02 '14 at 08:42
  • @AndreasRossberg: it works better if you avoid structural refinements — which indeed reinforces your first point. Here's the result (tested with Scala 2.11): https://gist.github.com/Blaisorblade/19ef1abb28e20995e187 – Blaisorblade Sep 10 '14 at 22:09
  • I'm curious on point 4: what's stronger about translucent type information from ML? Do you have an example? Path-dependent types feel weaker than they are because of choices in inference — e.g., with enough type annotations you get sharing constraints, but you fight against type inference and bad error messages (https://twitter.com/Blaisorblade/status/473995303100502017, https://github.com/inc-lc/ilc-scala/commit/06146d44a3d571eef17273ba2c8a0c9d66f64dd9), which is indeed very annoying. – Blaisorblade Sep 10 '14 at 22:30
  • 2
    @Blaisorblade, note that your gist does not only use nominal typing, it also changes the interface of the functor by reexporting the type. Sometimes this may be what you want, but sometimes it is not. The latter case cannot be expressed in Scala, AFAICT. – Andreas Rossberg Sep 11 '14 at 17:46
  • 1
    @Blaisorblade, here is a simple example: `trait T { type V; val v : V }; trait U { val a : T; val b : a.V }; def f(x : T) = new U { val a = x; val b = x.v }` -- this produces "error: overriding value b in trait U of type this.a.V; value b has incompatible type". Though I can't claim to understand why this doesn't work. – Andreas Rossberg Sep 11 '14 at 17:48
  • @AndreasRossberg: it's exactly the problem I mentioned — it's not your fault for losing against the typechecker. The fixed def. of `f` is: `def f(x : T) = new U { val a: x.type = x; val b = x.v }`. I changed `val a = x` (which is inferred to `val a: T = x`) to `val a: x.type = x`. With the former, the mismatch happens because x.v has type x.V which is not a.V. The error is shown better when writing `def f(x : T) = new U { val a = x; val b: a.V = x.v }`. – Blaisorblade Sep 11 '14 at 21:12
  • 1
    @AndreasRossberg: the insight you need to understand the above is that Γ ⊦ A = B is only ever deduced if Γ ⊦ A : B.type, or if A is a type alias to B (see the vObj paper at ECOOP 2003 from the Odersky group, especially rule SINGLE-=). That's because the typechecker doesn't even inline `a = b` to respect the phase distinction (and because type inference is too dumb in this context). I imagine that might be similar to singleton kinds one level down, but I've not studied singleton kinds fully yet. – Blaisorblade Sep 11 '14 at 21:22
  • @AndreasRossberg: On my gist reexporting the type: agreed, I don't see immediately how to really avoid that (unless the type is bound from outside). – Blaisorblade Sep 11 '14 at 21:30
  • 1
    @Blaisorblade, I see, thanks for the explanation. Re singletons: I think they are different, because their semantics actually yields an equivalence relation that is reflexive, symmetric, transitive, congruent, and closed under all beta/eta rules -- which was what I was alluding to with my point 4 (although you can actually explain ML module typing without singletons). – Andreas Rossberg Sep 11 '14 at 21:42
  • @AndreasRossberg: I see. Scala type equality is also a congruence (forgot to say it, sorry), but I guess I essentially showed that eta-expansion is not supported (without annotations). I guess ML module expressions can be normalized because modules are second-class so module expressions are part of a different phase? But I'll have to read up on PFPL I guess. – Blaisorblade Sep 11 '14 at 21:51
  • One think I really like about ML is that, given `functor Foo (X : TEST) = struct datatype t = ... end; structure FooBar = Foo(Bar); structure FooBaz = Foo(Baz)`, then `FooBar.t` and `FooBaz.t` are guaranteed to be distinct, even if `Bar.t` and `Baz.t` are the same type. This is important for enforcing abstraction when the body of `Foo` is impure. I have no idea how to do this in Scala. And this is why I mentioned datatype and exception generativity being an important aspect of ML modularity. – isekaijin Dec 09 '14 at 04:00
  • @EduardoLeón In standard jargon, one says that the functor `Foo` is generative. Scala has *only* generative functors, not applicative ones. Concretely, take `def Foo(X: Test) = new { trait T }` and call `Foo` twice. (You'll only have a problem if you make `T` a type synonym, but I think that's the same in ML). – Blaisorblade Jan 18 '15 at 16:12
  • 1
    @AndreasRossberg Here's a variant of the previous gist, where `T` is not reexported as a member (though it's a type parameter, and I'm not sure that's better). https://gist.github.com/Blaisorblade/dae225ca756ad4e5c5e6 I just got why Scala type equivalence is limited: in a Scala type, you can substitute a type with an equal one. But types also depend on terms, yet you can't substitute terms with equal ones! – Blaisorblade Jan 18 '15 at 16:25
  • I don't really understand why classes can't be used to model functors. Can't we use the class constructor to parameterize over values? – Ionuț G. Stan Feb 15 '17 at 14:10
  • @IonuțG.Stan, like with functions that would generally require phase-splitting the arguments into types and values. – Andreas Rossberg Feb 15 '17 at 16:15
  • @AndreasRossberg thanks. I'm still struggling to understand what this manual phase-split operation would look like in Scala. Resources are scarce regarding this topic. I've only found an example in the "Elaboration and Phase-Splitting in the TIL/ML Compiler" paper, but that uses a target pseudo-language. Do you have a pointer or can you show an example of how this manual separation would look like in Scala (if your time permits, obviously)? – Ionuț G. Stan Feb 16 '17 at 11:17
  • @IonuțG.Stan, that's a bit difficult to answer adequately in a comment. But for a contrived example, consider a signature S = {type t; module M : {type u; val v : something t u; ...}; val w : otherthing t M.u; ...} and a functor F : S -> S and imagine you need to apply F(F(A)). Now try to transform F and its applications such that types and values are separated. – Andreas Rossberg Feb 24 '17 at 10:40