What are some compelling use cases for dependent m

Question

Dependent method types, which used to be an experimental feature before, has now been enabled by default in the trunk, and apparently this seems to have created some excitement in the Scala community.

At first look, it's not immediately obvious what this could be useful for. Heiko Seeberger posted a simple example of dependent method types here, which as can be seen in the comment there can easily be reproduced with type parameters on methods. So that wasn't a very compelling example. (I might be missing something obvious. Please correct me if so.)

What are some practical and useful examples of use cases for dependent method types where they are clearly advantageous over the alternatives?

What interesting things can we do with them that weren't possible/easy before?

What do they buy us over the existing type system features?

Also, are dependent method types analogous to or drawing inspiration from any features found in the type systems of other advanced typed languages such as Haskell, OCaml?

Answer 1

I'm developing a model for the interoption of a form of declarative programming with environmental state. The details aren't relevant here (e.g. details about callbacks and conceptual similarity to the Actor model combined with a Serializer).

The relevant issue is state values are stored in a hash map and referenced by a hash key value. Functions input immutable arguments that are values from the environment, may call other such functions, and write state to the environment. But functions are not allowed to read values from the environment (so the internal code of the function is not dependent on the order of state changes and thus remains declarative in that sense). How to type this in Scala?

The environment class must have an overloaded method which inputs such a function to call, and inputs the hash keys of the arguments of the function. Thus this method can call the function with the necessary values from the hash map, without providing public read access to the values (thus as required, denying functions the ability to read values from the environment).

But if these hash keys are strings or integer hash values, the static typing of the hash map element type subsumes to Any or AnyRef (hash map code not shown below), and thus a run-time mismatch could occur, i.e. it would be possible to put any type of value in a hash map for a given hash key.

trait Env {
...
  def callit[A](func: Env => Any => A, arg1key: String): A
  def callit[A](func: Env => Any => Any => A, arg1key: String, arg2key: String): A
}

Although I didn't test the following, in theory I can get the hash keys from class names at runtime employing classOf, so a hash key is a class name instead of a string (using Scala's backticks to embed a string in a class name).

trait DependentHashKey {
  type ValueType
}
trait `the hash key string` extends DependentHashKey {
  type ValueType <: SomeType
}

So static type safety is achieved.

def callit[A](arg1key: DependentHashKey)(func: Env => arg1key.ValueType => A): A

Answer 2

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.

Answer 3

This new feature is needed when concrete abstract type members are used instead of type parameters. When type parameters are used, the family polymorphism type dependency can be expressed in the latest and some older versions of Scala, as in the following simplified example.

trait C[A]
def f[M](a: C[M], b: M) = b
class C1 extends C[Int]
class C2 extends C[String]

f(new C1, 0)
res0: Int = 0
f(new C2, "")
res1: java.lang.String = 
f(new C1, "")
error: type mismatch;
 found   : C1
 required: C[Any]
       f(new C1, "")
         ^

Answer 4

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.