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

Зависимые типы методов, которые раньше были экспериментальной функцией, теперь включены по умолчанию в магистрали , и, по-видимому, это, похоже, вызвало некоторое волнение в сообществе Scala.

На первый взгляд не сразу понятно, для чего это может быть полезно. Хайко Seeberger опубликовал простой пример зависимых типов методов здесь , которые , как можно видеть , в комментарии может быть легко воспроизведен с параметрами типа по методам. Так что это был не очень убедительный пример. (Возможно, мне не хватает чего-то очевидного. Поправьте меня, если это так.)

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

Что интересного мы можем сделать с ними, что раньше было невозможно / легко?

Что они покупают нам по сравнению с существующими функциями системы типов?

Кроме того, являются ли типы зависимых методов аналогичными или черпают вдохновение в каких-либо функциях систем типов других продвинутых типизированных языков, таких как Haskell, OCaml?

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

Так в чем проблема? Вложенные типы в Scala зависят от их включающего экземпляра. Следовательно, при отсутствии зависимых типов методов попытки использовать их вне этого экземпляра могут быть удручающе трудными. Это может превратить дизайн, который поначалу казался элегантным и привлекательным, в чудовищно жесткие и трудно поддающиеся рефакторингу.

Я проиллюстрирую это упражнением, которое я даю во время моего учебного курса Advanced 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)

Обратите внимание, что зависимость пути означает, что компилятор гарантирует, что testHashtestDuplicates методы и 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))

Обратите внимание на использование типов зависимых методов здесь: тип второго аргумента (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)

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

Изменить: консенсус заключается в том, что Bakery of Doom была монетой Дэвида Макивера ...

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

trait Graph {
  type Node
  type Edge
  def end1(e: Edge): Node
  def end2(e: Edge): Node
  def nodes: Set[Node]
  def edges: Set[Edge]
}

Где-то еще мы можем статически гарантировать, что мы не смешиваем узлы из двух разных графов, например:

def shortestPath(g: Graph)(n1: g.Node, n2: g.Node) = ... 

Конечно, это уже работало, если оно определено внутри Graph, но скажем, что мы не можем модифицировать Graphи пишем для него расширение «pimp my library».

По поводу второго вопроса: типы, поддерживаемые этой функцией, намного слабее, чем полные зависимые типы (см. « Зависимо типизированное программирование» в Agda, чтобы понять это.) Я не думаю, что видел аналогию раньше.

Эта новая функция необходима, когда вместо параметров типа используются конкретные элементы абстрактного типа . Когда используются параметры типа, зависимость типа полиморфизма семейства может быть выражена в последней и некоторых более старых версиях 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, "")
         ^

Я разрабатываю модель взаимодействия формы декларативного программирования с состоянием среды. Детали здесь не актуальны (например, подробности об обратных вызовах и концептуальном сходстве с моделью Актера в сочетании с Сериализатором).

Актуальная проблема заключается в том, что значения состояний хранятся в хэш-карте и на них ссылается значение хеш-ключа. Функции вводят неизменяемые аргументы, которые являются значениями из среды, могут вызывать другие такие функции и записывать состояние в среду. Но функциям не разрешено читать значения из среды (поэтому внутренний код функции не зависит от порядка изменения состояния и, таким образом, остается декларативным в этом смысле). Как это набрать в Scala?

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

Но если эти хэш-ключи являются строками или целочисленными значениями хеш-функции, статическая типизация типа элемента хэш-карты относится к Any или AnyRef (код хэш-карты не показан ниже), и, таким образом, может возникнуть несоответствие во время выполнения, т.е. для помещения любого типа значения в хеш-карту для данного хеш-ключа.

trait Env {
...
  def callit[A](func: Env => Any => A, arg1key: String): A
  def callit[A](func: Env => Any => Any => A, arg1key: String, arg2key: String): A
}

Хотя я не тестировал следующее, теоретически я могу получить хэш-ключи из имен классов во время выполнения classOf, поэтому хеш-ключ - это имя класса, а не строка (с использованием обратных ссылок Scala для вставки строки в имя класса).

trait DependentHashKey {
  type ValueType
}
trait `the hash key string` extends DependentHashKey {
  type ValueType <: SomeType
}

Таким образом достигается безопасность статического типа.

def callit[A](arg1key: DependentHashKey)(func: Env => arg1key.ValueType => A): A