依赖方法类型有哪些引人注目的用例? [英] What are some compelling use cases for dependent method types?

问题描述

依赖方法类型，以前是一个实验性功能，现在已经启用默认在后备箱中，显然这似乎创造了一些兴奋在 Scala 社区中.

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.

乍一看，这有什么用并不是很明显.Heiko Seeberger 发布了一个简单的依赖方法类型示例这里，可以在那里的评论中看到可以使用方法的类型参数轻松重现.所以这不是一个很有说服力的例子.(我可能遗漏了一些明显的东西.如果有，请纠正我.)

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?

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

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?

推荐答案

任何成员(即嵌套)类型的使用或多或少都会导致对依赖方法类型的需求.特别是，我认为没有依赖方法类型的经典蛋糕模式更接近于反模式.

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.

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

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.

我将通过我在高级 Scala 培训课程中进行的练习来说明这一点，

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
}

这是经典蛋糕模式的一个例子:我们有一系列通过层次结构逐渐细化的抽象(ResourceManager/Resource 由 FileManager 细化/File 依次由 NetworkFileManager/RemoteFile 细化).这是一个玩具示例，但模式是真实的:它在整个 Scala 编译器中使用，并在 Scala Eclipse 插件中广泛使用.

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)

请注意，路径依赖意味着编译器将保证NetworkFileManager 上的testHash 和testDuplicates 方法只能使用以下参数调用对应它，即.它是自己的 RemoteFiles，没有别的.

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.

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

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

注意这里依赖方法类型的使用:第二个参数(rm.Resource)的类型取决于第一个参数(rm)的值.

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.

自己试试...

// 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，我们不记得我们中谁创造了这个词)称其为末日面包店.

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.

一致认为末日面包店是大卫·麦基弗的造币......

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

额外奖励:Scala 的依赖类型形式(以及依赖方法类型作为其中的一部分)的灵感来自于编程语言 Beta ... 它们自然产生于 Beta 的一致嵌套语义.我不知道任何其他甚至微弱的主流编程语言都具有这种形式的依赖类型.Coq、Cayenne、Epigram 和 Agda 等语言具有不同形式的依赖类型，这在某些方面更通用，但由于是类型系统的一部分，与 Scala 不同，它没有子类型.

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.

这篇关于依赖方法类型有哪些引人注目的用例?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！