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

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) 的值。

无需依赖方法类型就可以做到这一点，但这非常尴尬，而且机制也很不直观:我已经教授这门类(class)近两年了，在那段时间里，没有人提出一个可行的方法无提示解决方案。

亲自尝试一下...

// 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 的创造......

额外的好处:Scala 的依赖类型形式(以及依赖方法类型作为其中的一部分)受到编程语言 Beta 的启发。 ...它们自然地源于 Beta 一致的嵌套语义。我不知道有任何其他甚至微弱的主流编程语言具有这种形式的依赖类型。 Coq、Cayenne、Epigram 和 Agda 等语言具有不同形式的依赖类型，这种形式在某些方面更为通用，但由于属于类型系统的一部分而存在显着差异，与 Scala 不同，类型系统没有子类型。