Гарантирует ли Scala согласованность при наличии последствий? - PullRequest
Новая
       59

Гарантирует ли Scala согласованность при наличии последствий?

0 голосов
/ 02 марта 2019

Статья Классы типов: слияние, когерентность и глобальная уникальность подчеркивает следующие моменты -

[Coherence] утверждает, что каждый разный действительный типизированный вывод программы приводит китоговая программа с такой же динамической семантикой.

[..]

Итак, на что часто ссылаются люди, сравнивая классы типа Scala с классами типа Haskell?Я собираюсь обозначить это как глобальная уникальность экземпляров , определяя, что в полностью скомпилированной программе для любого типа существует не более одного разрешения экземпляра для данного класса типов.Языки с экземплярами классов локальных типов, такими как Scala, обычно не имеют этого свойства, но в Haskell мы находим, что это свойство очень удобно при построении абстракций, таких как наборы.

Если вы посмотрите на эту статьюна Модульные импликации , он заявляет -

[..] Когерентность Scala может опираться на более слабое свойство не двусмысленности вместо каноничности.Это означает, что вы можете определить несколько неявных объектов типа Showable [Int] в вашей программе, не вызывая ошибки.Вместо этого Scala выдает ошибку, если разрешение неявного параметра неоднозначно.Например, если два неявных объекта типа Showable [Int] находятся в области действия, когда show применяется к Int, тогда компилятор сообщит об ошибке неоднозначности.

Оба из них создают впечатление, что Scala делаетобеспечивает согласованность, но не обеспечивает глобальную уникальность экземпляров.

Однако, если вы посмотрите на комментарии Мартина Одерского ( 1 , 2 ), то, по-видимому, термин согласованностьиспользуется как сокращение для «уникальности экземпляров», которая объясняет термины «локальная согласованность» и «глобальная согласованность».

  1. Является ли это просто неудачным случаем того же терминаимел в виду две разные вещи?Они, безусловно, различны - модульные импликации OCaml обеспечивают согласованность (согласно первому определению), но не глобальную уникальность экземпляров.

  2. Гарантирует ли Scala согласованность (согласно первому определению) вналичие причастности?

1 Ответ

0 голосов
/ 02 марта 2019

Я думаю, что они имеют в виду одно и то же.Согласованность ставится под сомнение только тогда, когда у вас есть несколько способов получения значения экземпляра / неявного значения;«Каждый другой действительный типизированный вывод» интересен только тогда, когда является более чем один раз типизирующим производным.И Scala, и Haskell не разрешают создавать экземпляры во время компиляции, которые могут привести к неоднозначным выводам.

Scala

В комментарии Одерского говорится о Scala: существует только один локальный способразрешающие случаи.Другими словами, существует только один действительный вывод локальной типизации.Достаточно тривиально, это согласуется с самим собой.Мне не ясно, что даже имеет смысл говорить о глобальной согласованности в Scala, но, если это так, у Scala ее точно нет: 

object Object1 {
  implicit val i: Int  = 9
  println(implicitly[Int])    // valid typing derivation of `Int` => printing 9
}
object Object2 {
  implicit val i: Int  = 10
  println(implicitly[Int])    // valid typing derivation of `Int` => printing 10
}

Haskell

Поскольку экземпляры Haskell являются глобальными, нет смысла различать локальную / глобальную согласованность.

Во время компиляции Haskell запрещает иметь два экземпляра, в которых один заголовок экземпляра перекрывается с другим.Это превращает поиск производных типов в однозначную задачу поиска без обратной проверки.Не неоднозначность - это то, что снова дает нам согласованность.

Интересно, что GHC позволяет ослабить это требование с помощью -XIncoherentInstances, позволяя писать локально несмежные экземпляры, что потенциально может нарушить глобальную согласованность.

...