Dependent Object Types: Towards a foundation for Scala's type system

Preview

Mika will present “Dependent Object Types: Towards a foundation for Scala’s type system” by Amin, Moors, and Odersky.

Summary

This was basically a presentation on how not to write a paper. We got stuck on page 1 of the paper, and pretty much discussed only the terms of what it means for a type to be an “intersection”.

The paper itself presents DOT, a dependent object types calculus, which proves not much, is clanky, is hard to reason about and lacks proofs of both type-safety and type-soundness, but believes that they exist. Works that came after this one showed that a subcalculus of it can be proven type-sound, and the proof of type-safety through step-indexed logical relations is still being investigated. It’s an interesting experiment in making a dependent link between objects and types via path-dependencies, at most.

Discussion

Page one of this paper says that Scala’s compound types are modelled with “classic intersection types”. In Scala parlance, the term “compound type” means “type extended via mixins”, using the following syntax:

Foo with Bar { self => ... }

Mixing in traits ends up with a type that could be abstract (with no concrete classes as base, but containing all the fields and methods of the traits mixed in). It is, however, not commutative, and does not, in theory, always work (even though cases in which it doesn’t are quite exhibitional). To mend this, DOT introduces their idea of intersection types that seem to fix this.

This is where everything falls apart, though. An intersection (and respectively, the union) of two sets, contains only those elements of the sets which are in both sets. However, not being very careful with their langauge, the authors mention that the type intersections T ∧ T' carries the declarations of members present in either T or T'. Even though the word choice (“or”) lines up quite well with the symbol used (wedge), it makes little sense in the introduction, as the notion of declarations and members have non-colloquial meanings: members are refinements made in a class, and declarations are sets of constraints on said class by said refinements. In this light, the intersection of two types defined purely structurally, is the intersection of their structural refinements. This resulting set is strictly smaller or equal than any one individual set. However, this also means that the set of values inhabiting the types is larger, as it is less-constrained.

Another problematic issue seems to come from the fact that it is possible to think of subtyping as forming a kind of intersection type, where the base class is the natural intersection of all of its children, as these children can be used instead of any base class, but only in the sense defined within said base class. In example, if the child class introduces a new member, from the perspective of using it in a position where the base class was called for, that member would be inexistent. We learned that this, although true, does not get to be called an intersection type. This will be further elaborated in two weeks in the next, hopefully more fruitful escapade into reading computer science papers.

Of the things actually from the paper, and not sidelined by the above discussion, a quick note should be made with regards to the terms “type-sound” and “type-safe”. Type-safety, as described in the paper, is the ability of the semantics to not get stuck under any input. This is described as a different form of guarantee to those of progress and preservation, which guarantee that every step made by the semantics is either going to evaluate into a well-typed value, or be able to make another step: type-safety says that after some number of steps (marked by a ->\* symbol compared to the normal, triple overloaded -> symbol), a value will either be reached, or a step made further. I have to think about this a bit more, but hopefully, this too will be explored some more in a few weeks.

To give a short description of what I learned while preparing for this, if not presenting: it was interesting to see types as very black-and-white lattice-forming refinements between bottom and top. The only way to start off a typing session in DOT is to say that some type is a refinement of ⊥ .. ⊤ , which are the only two built-in type terms. The refinements formed are path declarations, including members (nested type declarations with a subtyping relation), fields and methods. Types are thus path-dependent, and I think I’m still trying to understand what this means in a context of talking about the word “dependent” in our field. Can we exploit this for actually doing Idris-style dependently-typed things? I think the answer is not simply, but it would be nice to see an experiment in that direction.

Lawton asked the question of why the particularly noteworthy type:

A = new ⊤ { type T <: A }
B = new ⊤ { type T <: B }
A with B { type T <: A with B { type T <: ... } }

actually is the greatest lower bound type for A and B, and in my panicked state, I didn’t remember that previously I thought of Lawton when first reading this: this form of greatest lower boundedness is almost exactly the categorical product applied to posets, if you treat posets as categories. In that sense, we can try to prove that this is indeed the greatest lower bound for A and B by following universal construction of the product: let us say there exists a T' such that it is the greatest lower bound for A and B in the following sense:

A with B { type T <: A with B { type T <: T' } }

Having defined T in A and B as subtypes of both of them, T' would have to be a composition of the form f o (A with B), where f is a set of refinements on top of A with B. If this set is empty, then T' = A with B, meaning that the recursive definition requires us to define another level of T, where we can exploit this property once again ad infinitum. If f is not empty, however, then it is not a part of A with B, and thus A with B is indeed a lower bound for every level of recursion. As Ben said it, without referring to category theory and universal construction, any finite type T' would be less precise than A with B { type T <: A with B { ... } }, at any level of recursion. I’m not good on my feet, sorry for that.

To quote the paper and end on “a disturbing note”, the paper actually never formally explains what the title means. I still have no idea whether there’s a hyphen missing in there or not. Are these “dependent object-types” or dependent-object types“? I can see both being true, which may indeed be the reason behind not explaining it, but having never seen types represented as objects so cleanly, it would have been a nice thing to, at the least, mention it.