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

mis*_*tor 124 haskell type-systems programming-languages scala dependent-method-type

依赖方法类型以前曾是一个实验性功能,现在默认情况下已在中继中启用,显然这似乎在Scala社区中引起了一些兴奋.

初看起来,这并不是显而易见的.Heiko Seeberger在这里发布了一个简单的依赖方法类型示例,从评论中可以看出,可以很容易地在方法上使用类型参数进行复制.所以这不是一个非常引人注目的例子.(我可能会遗漏一些明显的东西.如果是这样,请纠正我.)

对于依赖方法类型的用例有哪些实用且有用的例子,它们明显优于替代方法?

我们可以用以前不可能/容易的事情做些什么有趣的事情?

他们通过现有的类型系统功能为我们买了什么?

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

Mil*_*bin 111

或多或少地使用成员(即嵌套)类型可能引起对依赖方法类型的需求.特别是,我认为没有依赖方法类型,经典蛋糕模式更接近于反模式.

所以有什么问题?Scala中的嵌套类型取决于它们的封闭实例.因此,在没有依赖方法类型的情况下,尝试在该实例之外使用它们会令人沮丧地困难.这可以将最初看起来优雅且吸引人的设计转变为怪异的,这些怪物是苛刻的,并且难以重构.

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

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
}
Run Code Online (Sandbox Code Playgroud)

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

这是一个使用抽象的例子,

val nfm = new NetworkFileManager
val rf : nfm.Resource = nfm.create
nfm.testHash(rf)
nfm.testDuplicates(rf)
Run Code Online (Sandbox Code Playgroud)

请注意,路径依赖性意味着编译器将保证只能使用与其对应的参数调用testHashtestDuplicateson方法NetworkFileManager,即.它是自己的RemoteFiles,没有别的.

这无疑是一个理想的属性,但是假设我们想将这个测试代码移到另一个源文件中?使用依赖的方法类型,在ResourceManager层次结构之外重新定义这些方法非常容易,

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

def testDuplicates4(rm : ResourceManager)(r : rm.Resource) = 
  assert(r.duplicates(r))
Run Code Online (Sandbox Code Playgroud)

请注意依赖方法类型的使用:第二个参数(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)
Run Code Online (Sandbox Code Playgroud)

经过一段时间的努力,你可能会发现为什么我(或者也许是David MacIver,我们不记得我们中的哪个人创造了这个词)称之为"毁灭面包店".

编辑:共识是,面对面的厄运是David MacIver的造币......

对于奖励:Scala的一般依赖类型(以及作为其一部分的依赖方法类型)受编程语言Beta的启发......它们自然地来自Beta的一致嵌套语义.我不知道任何其他甚至微弱的主流编程语言,它具有这种形式的依赖类型.像Coq,Cayenne,Epigram和Agda这样的语言有一种不同形式的依赖类型,这在某种程度上更为通用,但与作为Scala不具有子类型的类型系统的一部分有很大不同.

  • 创造这个词的是David MacIver,但无论如何,它都是描述性的.这是一个很棒的*解释为什么依赖方法类型如此令人兴奋.干得好! (2认同)

Ale*_*nov 52

trait Graph {
  type Node
  type Edge
  def end1(e: Edge): Node
  def end2(e: Edge): Node
  def nodes: Set[Node]
  def edges: Set[Edge]
}
Run Code Online (Sandbox Code Playgroud)

在其他地方,我们可以静态地保证我们不会混合来自两个不同图形的节点,例如:

def shortestPath(g: Graph)(n1: g.Node, n2: g.Node) = ... 
Run Code Online (Sandbox Code Playgroud)

当然,如果在内部定义,这已经有效Graph,但是说我们无法修改Graph并正在为它编写"pimp my library"扩展.

关于第二个问题:由此功能启用的类型远远弱于完全依赖类型(请参阅Agda中的依赖类型编程以了解其中的风格.)我认为我之前没有看到类比.


She*_*III 6

当使用具体的 抽象类型成员而不是类型参数时,需要此新功能.使用类型参数时,族多态类型依赖关系可以在最新版本和一些旧版本的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, "")
         ^
Run Code Online (Sandbox Code Playgroud)