What are some compelling use cases for dependent method types?

trait Graph {
  type Node
  type Edge
  def end1(e: Edge): Node
  def end2(e: Edge): Node
  def nodes: Set[Node]
  def edges: Set[Edge]
}

Somewhere else we can statically guarantee that we aren't mixing up nodes from two different graphs, e.g.:

def shortestPath(g: Graph)(n1: g.Node, n2: g.Node) = ... 

Of course, this already worked if defined inside Graph, but say we can't modify Graph and are writing a "pimp my library" extension for it.

About the second question: types enabled by this feature are far weaker than complete dependent types (See Dependently Typed Programming in Agda for a flavor of that.) I don't think I've seen an analogy before.


More or less any use of member (ie. nested) types can give rise to a need for dependent method types. In particular, I maintain that without dependent method types the classic cake pattern is closer to being an anti-pattern.

So what's the problem? Nested types in Scala are dependent on their enclosing instance. Consequently, in the absence of dependent method types, attempts to use them outside of that instance can be frustratingly difficult. This can turn designs which initially seem elegant and appealing into monstrosities which are nightmarishly rigid and difficult to refactor.

I'll illustrate that with an exercise I give during my Advanced Scala training course,

trait ResourceManager {
  type Resource <: BasicResource
  trait BasicResource {
    def hash : String
    def duplicates(r : Resource) : Boolean
  }
  def create : Resource

  // Test methods: exercise is to move them outside ResourceManager
  def testHash(r : Resource) = assert(r.hash == "9e47088d")  
  def testDuplicates(r : Resource) = assert(r.duplicates(r))
}

trait FileManager extends ResourceManager {
  type Resource <: File
  trait File extends BasicResource {
    def local : Boolean
  }
  override def create : Resource
}

class NetworkFileManager extends FileManager {
  type Resource = RemoteFile
  class RemoteFile extends File {
    def local = false
    def hash = "9e47088d"
    def duplicates(r : Resource) = (local == r.local) && (hash == r.hash)
  }
  override def create : Resource = new RemoteFile
}

It's an example of the classic cake pattern: we have a family of abstractions which are gradually refined through a heirarchy (ResourceManager/Resource are refined by FileManager/File which are in turn refined by NetworkFileManager/RemoteFile). It's a toy example, but the pattern is real: it's used throughout the Scala compiler and was used extensively in the Scala Eclipse plugin.

Here's an example of the abstraction in use,

val nfm = new NetworkFileManager
val rf : nfm.Resource = nfm.create
nfm.testHash(rf)
nfm.testDuplicates(rf)

Note that the path dependency means that the compiler will guarantee that the testHash and testDuplicates methods on NetworkFileManager can only be called with arguments which correspond to it, ie. it's own RemoteFiles, and nothing else.

That's undeniably a desirable property, but suppose we wanted to move this test code to a different source file? With dependent method types it's trivially easy to redefine those methods outside the ResourceManager hierarchy,

def testHash4(rm : ResourceManager)(r : rm.Resource) = 
  assert(r.hash == "9e47088d")

def testDuplicates4(rm : ResourceManager)(r : rm.Resource) = 
  assert(r.duplicates(r))

Note the uses of dependent method types here: the type of the second argument (rm.Resource) depends on the value of the first argument (rm).

It is possible to do this without dependent method types, but it's extremely awkward and the mechanism is quite unintuitive: I've been teaching this course for nearly two years now, and in that time, noone has come up with a working solution unprompted.

Try it for yourself ...

// Reimplement the testHash and testDuplicates methods outside
// the ResourceManager hierarchy without using dependent method types
def testHash        // TODO ... 
def testDuplicates  // TODO ...

testHash(rf)
testDuplicates(rf)

After a short while struggling with it you'll probably discover why I (or maybe it was David MacIver, we can't remember which of us coined the term) call this the Bakery of Doom.

Edit: consensus is that Bakery of Doom was David MacIver's coinage ...

For the bonus: Scala's form of dependent types in general (and dependent method types as a part of it) was inspired by the programming language Beta ... they arise naturally from Beta's consistent nesting semantics. I don't know of any other even faintly mainstream programming language which has dependent types in this form. Languages like Coq, Cayenne, Epigram and Agda have a different form of dependent typing which is in some ways more general, but which differs significantly by being part of type systems which, unlike Scala, don't have subtyping.