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

Question

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

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

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

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

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

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

Answer 1

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

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

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

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

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

Answer 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 и пишем для него расширение "pimp my library".

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

Answer 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, "")
         ^

Answer 4

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

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