Objects with type members: what is Scala's object vs module system ? (Trying to understand a 2014 Odersky paper on path dependent types)

user_1198559 0
Viewed 282

I am reading Foundations of path dependent types. On the first page, on the right column it is written:

Our motivation is twofold. First, we believe objects with type members are not fully understood. It is not clear what causes the complexity, which pieces of complexity are essential to the concept or accidental to a language implementation or calculus that tries to achieve something else. Second, we believe objects with type members are really useful. They can encode a variety of other, usually separate type system features. Most importantly, they unify concepts from object and module systems, by adding a notion of nominality to otherwise structural systems.

Could someone clarify/explain what does "object vs module" system mean?

Or in general, what does

"they (objects with type members) unify concepts from object and module systems, by adding a notion of nominality to otherwise structural systems."

mean ?

What concepts? From where ?

Nominality in the object names / values ? Structure in the types ? Or the other way around?

Where do type members here belong to ? To module system ? Object system ? How? Why?

EDIT:

How does this unification relate to path dependent types ? It seems to me that they allow this unification to happen (objects with type members). Is that so ? If yes, how ?

Could you give a simple example what that means ? (I.e. path dependent types allowing the unification of module and object systems vs. why would the unification not be possible happen if we would not have path dependent types?)

EDIT 2:

From the paper:

To make any use of type members, programmers need a way to refer to them. This means that types must be able to refer to objects, i.e. contain terms that serve as static approximation of a set of dynamic objects. In other words, some level of dependent types is required; the usual notion is that of path-dependent types.

So my understanding so far (with the help of Jesper's answer) :

This paragraph above partially answers some of the questions above. The main seems to be to have objects with type members and to have that path dependent types are needed because objects are dynamic/runtime dependent but types are static (defined at compile time) so just by having objects that lead to type members would not work because then those type members would not be defined clearly at compile time.

Path dependent types help here by pinning down the path leading to a type member at compile time (by requiring that the objects are already known/defined at compile time), so even if the path goes via objects (that can change during compile time) but if those objects are fixed already at compile time then their type members can have a clear meaning at compile time too.

type-members path-dependent-type module scala
1 Answers

I'm not sure I fully understand what your question is, but I'll take a stab at it. :) I think the authors mainly are referring to ML style modules where a signature corresponds to a Scala trait and a structure corresponds to a Scala object. Scala unifies the concepts of record values, objects and modules which in most other languages (like ML, Rust etc.) are separate concepts. The main benefit is that in Scala modules/objects can be passed around as normal function arguments (while in ML you have to use special functors for this).

In ML a module is checked for compatibility with a signature (trait in Scala) based on its structure (similar to structural typing in Scala), but in Scala the module must implement the trait by name (nominal typing). So even if two modules/objects have the same structure in Scala they might not be compatible with each other depending on their super type hierarchy.

A really powerful feature regarding type members in Scala is that you can use a trait even if you don't know the exact type of its type members as long as you do it in a type safe way (I think this is also possible in ML modules), for example:

trait A {
  type X
  def getX: X
  def setX(x: X): Unit
}

def foo(a: A) = a.setX(a.getX)

In foo the Scala compiler doesn't know the exact type of a.X but a value of the type can still be used in a way the compiler knows is safe. This is not possible in Rust for example.

The next version of the Scala compiler, Dotty, will be based on the theory described in the paper you reference. This unification of modules and objects combined with subtyping, traits and type members is one reason that Scala is unique and very powerful.

EDIT: To expand a bit why path dependent types increases the flexibility of Scala's module/object system, let's expand the example above with:

def bar(a: A, b: A) = a.setX(b.getX)

This will result in a compilation error:

error: type mismatch;
 found   : b.T
 required: a.T
  def foo(a: A, b: A) = a.setX(b.getX)
                                ^

and correctly so because a.T and b.T could resolve to different types. You can fix it by using a path dependent type:

def bar(a: A)(b: A { type X = a.X }) = a.setX(b.getX)

Or add a type parameter:

def bar[T](a: A { type X = T }, b: A { type X = T }) = a.setX(b.getX)

So, path dependent types eliminates some need of type parameters, and also allows us to express existential types efficiently (corresponding to A[_] or A[T] forSome { type T } if A had a type parameter instead of a type member).

user_21190020
Related