依赖方法类型有哪些引人注目的用例？

Question

依赖方法类型，以前是一个实验性的特性，现在已经变成了enabled by default in the trunk，显然这似乎在Scala社区中创建了some excitement。

乍一看，这有什么用还不是一目了然。Heiko Seeberger发布了一个依赖方法类型here的简单示例，可以在注释中看到，它可以很容易地在方法上使用类型参数重现。所以这不是一个很有说服力的例子。(我可能遗漏了一些明显的东西。如果是这样，请纠正我。)

依赖方法类型的一些实用和有用的用例有哪些明显优于备选方法的示例？

我们可以用它们做些以前不可能/容易做的有趣的事情吗？

与现有的类型系统特性相比，它们给我们带来了什么？

此外，依赖方法类型是否与其他高级类型语言(如Haskell、OCaml )的类型系统中的任何功能相似或从中汲取灵感？

Answer 1

或多或少使用任何成员(例如，嵌套)类型可能导致对依赖方法类型的需求。特别是，我坚持认为，如果没有依赖方法类型，经典的蛋糕模式更接近于反模式。

那么问题出在哪里呢？Scala中的嵌套类型依赖于它们的封闭实例。因此，在没有依赖方法类型的情况下，尝试在该实例之外使用它们可能非常困难。这可能会把最初看起来优雅和吸引人的设计变成可怕的僵化和难以重构的怪物。

我将通过我在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
}

这是一个经典的蛋糕模式的例子:我们有一个抽象家族，通过层级结构逐步改进(ResourceManager/Resource由FileManager/File改进，而后者又由NetworkFileManager/RemoteFile改进)。这只是一个玩具示例，但其模式是真实的:它在整个Scala编译器中使用，并在Scala Eclipse插件中广泛使用。

这是一个使用中的抽象的例子，

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

请注意，路径依赖意味着编译器将保证NetworkFileManager上的testHash和testDuplicates方法只能通过与其对应的参数调用，即。这是它自己的RemoteFiles，没有其他东西。

不可否认，这是一个理想的属性，但假设我们想要将此测试代码移动到不同的源文件中？对于依赖方法类型，很容易在ResourceManager层次结构之外重新定义这些方法，

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

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

请注意此处依赖方法类型的用法:第二个参数(rm.Resource)的类型取决于第一个参数(rm)的值。

在没有依赖方法类型的情况下也可以做到这一点，但这非常笨拙，机制也相当不直观:我教授这门课程已经将近两年了，在这段时间里，没有人在没有提示的情况下提出了一个可行的解决方案。

自己试试吧.

// 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)

经过一小段时间的努力，你可能会发现为什么我(或者可能是David MacIver，我们不记得是谁创造了这个术语)称它为末日面包房。

编辑：的共识是末日面包房是David MacIver的创造……

额外的好处:Scala的依赖类型形式(以及依赖方法类型作为其中的一部分)的灵感来自于编程语言Beta……它们是由Beta一致的嵌套语义自然产生的。我不知道还有没有其他主流编程语言有这种形式的依赖类型。像Coq，Cayenne，Epigram和Agda这样的语言有不同形式的依赖类型，在某些方面更通用，但它是类型系统的一部分，与Scala不同，它没有子类型。

Answer 2

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

在其他地方，我们可以静态地保证我们不会混淆来自两个不同图的节点，例如：

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

当然，如果在Graph中定义的话，这已经可以工作了，但是假设我们不能修改Graph，并且正在为它编写一个"pimp my library“扩展。

关于第二个问题:此功能支持的类型比完全依赖的类型弱得多(有关这方面的信息，请参阅Dependently Typed Programming in Agda )。我想我以前没见过这样的类比。

Answer 3

当具体的abstract type members are used instead of type parameters时需要这个新功能。当使用类型参数时，family polymorphism类型依赖关系可以在最新版本和一些较旧版本的Scala中表达，如下面的简化示例所示。

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, "")
         ^