Каковы некоторые убедительные примеры использования зависимых типов методов?

более или менее любое использование члена (т. е. вложенные) типы могут вызвать необходимость в зависимых типах методов. В частности, я утверждаю, что без зависимых типов методов классический шаблон торта ближе к анти-шаблону.

так в чем проблема? Вложенные типы в 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
}

это пример классической модели торта: у нас есть семейство абстракций, которые постепенно уточняются через наследственность (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)

обратите внимание, что зависимость пути означает, что компилятор гарантирует, что testHash и testDuplicates методы NetworkFileManager можно назвать только с аргументами, которые ему соответствуют, т. е.. это свой RemoteFiles, и больше ничего.

это бесспорно a желательное свойство, но предположим, что мы хотим переместить этот тестовый код в другой исходный файл? С зависимыми типами методов тривиально легко переопределить эти методы вне 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)

после недолгой борьбы с этим вы, вероятно, узнаете, почему я (или, может быть, это был Дэвид Макивер, мы не можем вспомнить, кто из нас придумал этот термин) называю это пекарней судьбы.

Edit: консенсус в том, что пекарня судьбы была Дэвидом Макивером чеканка. ..

для бонуса: форма зависимых типов Scala в целом (и зависимые типы методов как ее часть) была вдохновлена языком программирования бета ... они возникают естественным образом из последовательной семантики вложенности бета. Я не знаю ни одного другого даже слегка основного языка программирования, который имеет зависимые типы в этой форме. Языки, такие как Coq, Cayenne, Epigram и Agda, имеют другую форму зависимой типизации, которая в некотором роде больше общее, но которое значительно отличается тем, что является частью систем типов, которые, в отличие от Scala, не имеют подтипов.