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

问题描述

以前曾是实验性功能的相关方法类型现在已启用默认情况下在中继线中，显然这似乎创造了一些令人兴奋的 < a>在Scala社区中。

起初看，这可能不是很明显。 Heiko Seeberger发布了一个依赖方法类型的简单示例，此处，这可以在评论中看到可以很容易地用方法的类型参数进行复制。所以这不是一个非常有说服力的例子。 （我可能会漏掉一些明显的东西，如果是这样的话，请纠正我。）

什么是依赖方法类型用例的实用和有用的例子，替代品？

我们可以对他们做些什么有趣的事情？

另外，它们是否与我们现有的类型系统功能相比，购买了我们的类型系统功能？或从其他高级类型语言（如Haskell，OCaml）的类型系统中找到的任何特征中获取灵感？解析方案

或多或少成员（即嵌套）类型的任何用法都可能引起对依赖方法类型的需要。特别是，我坚持认为，如果没有依赖方法类型，经典的蛋糕模式更接近于反模式。

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

我会在我的高级Scala培训课程，

  trait ResourceManager {
 type Resource< ;: BasicResource 
 trait BasicResource {
 def hash：String 
 def duplicateates（r：Resource）：Boolean 
} 
 def create：Resource 
 
 //测试方法：练习是将它们移到ResourceManager之外
 def testHash（r：Resource）= assert（r.hash == 9e47088d）
 def testDuplicates（r：Resource）= assert（r.duplicates（r））
} 
 
 trait FileManager扩展了ResourceManager {
 type Resource< ：文件
 trait文件扩展BasicResource {
 def local：Boolean 
} 
覆盖def create：Resource 
} 
 
 class Ne tworkFileManager扩展FileManager {
类型Resource = RemoteFile $ b $ class RemoteFile extends File {
 def local = false 
 def hash =9e47088d
 def duplicates（r：Resource） =（local == r.local）&& （hash == r.hash）
} 
覆盖def create：Resource = new RemoteFile 
} 
  

这是一个典型的蛋糕模式的例子：我们有一个抽象系列，通过一个渐变（ ResourceManager / Resource 通过 FileManager / File 进行改进， code> 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 层次结构外重新定义这些方法，

  assert（r.hash ==9e47088d）
 
 def testDuplicates4（rm：ResourceManager）（r ：rm.Resource）= 
 assert（r.duplicates（r））
  

第二个参数的类型（ rm.Resource ）取决于第一个参数的值（ rm

在不依赖方法类型的情况下做到这一点是可能的，但它非常尴尬，并且这种机制非常不直观：我一直在教这门课程近两年了，在那个时候，没有人提出了一个自发的解决方案。

为自己试试...

  //在
之外重新实现testHash和testDuplicates方法// ResourceManager层次结构wi使用依赖方法类型
 def testHash // TODO ... 
 def testDuplicates // TODO ... 
 
 testHash（rf）
 testDuplicates（rf）
  

经过一段时间的苦苦挣扎后，您可能会发现为什么我（或者也许是David MacIver，我们不记得我们当中哪个人创造了这个术语）称之为毁灭的面包。

编辑： David MacIver的造币...
$ b $ p为了获得奖金：Scala通常依赖类型的形式（以及依赖方法类型作为其一部分）受到了编程语言的启发<他们自然产生于Beta的一致嵌套语义。我不知道任何其他甚至微弱的主流编程语言，它具有这种形式的依赖类型。像Coq，Cayenne，Epigram和Agda这样的语言有不同的依赖打字形式，这在某种程度上更为通用，但是与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.

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?

解决方案

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.

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