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

Ответ 1

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

Так в чем проблема? Вложенные типы в 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, и ничего больше.

Это бесспорно желательное свойство, но предположим, что мы хотим, чтобы переместить этот тестовый код на другой исходный файл? С зависимыми типами методов тривиально легко переопределить эти методы вне иерархии 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... они естественным образом возникают из согласованной семантики вложенности Бета. Я не знаю ни одного другого, даже слабого основного языка программирования, который имеет зависимые типы в этой форме. Языки, такие как Coq, Cayenne, Epigram и Agda, имеют различную форму зависимой типизации, которая в некотором роде более общая, но которая существенно отличается, будучи частью систем типов, которые, в отличие от Scala, не имеют подтипов.

Ответ 2

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 и написали для него расширение "сутенер моей библиотеки".

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

Ответ 3

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

Ответ 4

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

Соответствующая проблема - это значения состояния, которые хранятся в хэш-карте и обозначаются значением хэш-ключа. Функции вводят неизменяемые аргументы, которые являются значениями из среды, могут вызывать другие такие функции и записывать состояние в среду. Но функциям не разрешено считывать значения из среды (поэтому внутренний код функции не зависит от порядка изменений состояния и, следовательно, остается декларативным в этом смысле). Как ввести это в 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