Любая причина, почему Scala не поддерживает явно зависимые типы?
Существуют зависимые от пути типы, и я думаю, что в Scala можно выразить почти все особенности таких языков, как Epigram или Agda, но мне интересно, почему Scala не поддерживает это более явно, как это очень хорошо в других областях (скажем,, DSLs)? Что-то мне не хватает, как "это не нужно"?
4 ответа
Помимо синтаксического удобства, комбинация одноэлементных типов, зависимых от пути типов и неявных значений означает, что Scala имеет удивительно хорошую поддержку зависимой типизации, как я пытался продемонстрировать в бесформенной форме.
Внутренняя поддержка Scala для зависимых типов осуществляется через зависимые от пути типы. Они позволяют типу зависеть от пути селектора через граф объекта (то есть значения), например,
scala> class Foo { class Bar }
defined class Foo
scala> val foo1 = new Foo
foo1: Foo = Foo@24bc0658
scala> val foo2 = new Foo
foo2: Foo = Foo@6f7f757
scala> implicitly[foo1.Bar =:= foo1.Bar] // OK: equal types
res0: =:=[foo1.Bar,foo1.Bar] = <function1>
scala> implicitly[foo1.Bar =:= foo2.Bar] // Not OK: unequal types
<console>:11: error: Cannot prove that foo1.Bar =:= foo2.Bar.
implicitly[foo1.Bar =:= foo2.Bar]
На мой взгляд, вышесказанного должно быть достаточно, чтобы ответить на вопрос "Является ли Scala зависимым типом языка?" в позитиве: ясно, что здесь у нас есть типы, которые отличаются значениями, которые являются их префиксами.
Тем не менее, часто возражают, что Scala не является "полностью" зависимым языком типов, потому что он не имеет зависимой суммы и типов продуктов, которые можно найти в Agda, Coq или Idris в качестве встроенных. Я думаю, что это в некоторой степени отражает закрепление формы над основами, тем не менее, я постараюсь показать, что Scala намного ближе к этим другим языкам, чем это обычно признается.
Несмотря на терминологию, зависимые типы сумм (также известные как типы Sigma) представляют собой просто пару значений, в которых тип второго значения зависит от первого значения. Это прямо представимо в Scala,
scala> trait Sigma {
| val foo: Foo
| val bar: foo.Bar
| }
defined trait Sigma
scala> val sigma = new Sigma {
| val foo = foo1
| val bar = new foo.Bar
| }
sigma: java.lang.Object with Sigma{val bar: this.foo.Bar} = $anon$1@e3fabd8
и на самом деле, это важная часть кодирования зависимых типов методов, которая необходима для выхода из "Bakery of Doom" в Scala до 2.10 (или ранее через опцию компилятора Scala для экспериментальных типов -Ydependent-method).
Зависимые типы продуктов (также называемые типами Pi) по существу являются функциями от значений до типов. Они являются ключом к представлению векторов статического размера и других потомков для зависимых языков программирования. Мы можем кодировать типы Pi в Scala, используя комбинацию зависимых от пути типов, одноэлементных типов и неявных параметров. Сначала мы определяем признак, который будет представлять функцию от значения типа T до типа U,
scala> trait Pi[T] { type U }
defined trait Pi
Мы можем определить полиморфный метод, который использует этот тип,
scala> def depList[T](t: T)(implicit pi: Pi[T]): List[pi.U] = Nil
depList: [T](t: T)(implicit pi: Pi[T])List[pi.U]
(обратите внимание на использование зависимого от пути типа pi.U в типе результата List[pi.U]). При заданном значении типа T эта функция вернет (n пустой) список значений типа, соответствующего этому конкретному значению T.
Теперь давайте определим некоторые подходящие значения и неявных свидетелей для функциональных отношений, которые мы хотим поддерживать,
scala> object Foo
defined module Foo
scala> object Bar
defined module Bar
scala> implicit val fooInt = new Pi[Foo.type] { type U = Int }
fooInt: java.lang.Object with Pi[Foo.type]{type U = Int} = $anon$1@60681a11
scala> implicit val barString = new Pi[Bar.type] { type U = String }
barString: java.lang.Object with Pi[Bar.type]{type U = String} = $anon$1@187602ae
А теперь вот наша функция с использованием Pi-типа в действии,
scala> depList(Foo)
res2: List[fooInt.U] = List()
scala> depList(Bar)
res3: List[barString.U] = List()
scala> implicitly[res2.type <:< List[Int]]
res4: <:<[res2.type,List[Int]] = <function1>
scala> implicitly[res2.type <:< List[String]]
<console>:19: error: Cannot prove that res2.type <:< List[String].
implicitly[res2.type <:< List[String]]
^
scala> implicitly[res3.type <:< List[String]]
res6: <:<[res3.type,List[String]] = <function1>
scala> implicitly[res3.type <:< List[Int]]
<console>:19: error: Cannot prove that res3.type <:< List[Int].
implicitly[res3.type <:< List[Int]]
(обратите внимание, что здесь мы используем Scala's <:< оператор-подвид =:= так как res2.type а также res3.type являются одноэлементными типами и, следовательно, более точными, чем типы, которые мы проверяем на RHS).
На практике, однако, в Scala мы не начинали бы с кодирования типов Sigma и Pi, а затем продолжали бы, как в Agda или Idris. Вместо этого мы будем использовать зависимые от пути типы, одноэлементные типы и импликации напрямую. Вы можете найти множество примеров того, как это проявляется в бесформенных формах: размерные типы, расширяемые записи, подробные списки HL, ненужные шаблоны, универсальные молнии и т. Д. И т. Д. И т. Д.
Единственное оставшееся возражение, которое я вижу, состоит в том, что в приведенной выше кодировке типов Pi мы требуем, чтобы одноэлементные типы зависимых значений были выражаемыми. К сожалению, в Scala это возможно только для значений ссылочных типов, но не для значений не ссылочных типов (особенно, например, Int). Это позор, но не внутренняя трудность: средство проверки типов в Scala представляет собой единичные типы нереферентных значений внутри, и была проведена пара экспериментов по их прямому выражению. На практике мы можем обойти проблему с помощью довольно стандартного кодирования натуральных чисел на уровне типов.
В любом случае, я не думаю, что это небольшое ограничение домена может быть использовано как возражение против статуса Scala как языка с независимой типизацией. Если это так, то то же самое можно сказать и о зависимой ML (которая допускает зависимости только от значений натуральных чисел), что было бы странным выводом.
Я бы предположил, что это потому, что (как я знаю из опыта, используя зависимые типы в Coq Proof Assistant, который полностью поддерживает их, но все же не очень удобно), зависимые типы - очень продвинутая функция языка программирования, которую действительно трудно получить право - и может привести к экспоненциальному увеличению сложности на практике. Они все еще являются темой компьютерных исследований.
Я считаю, что зависящие от пути типы Scala могут представлять только Σ-типы, но не Π-типы. Это:
trait Pi[T] { type U }
это не совсем Π-тип. По определению, type-тип или зависимый продукт - это функция, тип результата которой зависит от значения аргумента, представляющий универсальный квантификатор, т. Е. ∀x: A, B(x). Однако в вышеприведенном случае это зависит только от типа T, но не от некоторого значения этого типа. Черта Pi сама по себе является Σ-типом, экзистенциальным квантором, т. Е. ∃x: A, B(x). Само-ссылка объекта в этом случае действует как количественная переменная. Однако, когда он передается как неявный параметр, он сводится к функции обычного типа, поскольку он разрешается по типу. Кодировка для зависимого продукта в Scala может выглядеть следующим образом:
trait Sigma[T] {
val x: T
type U //can depend on x
}
// (t: T) => (∃ mapping(x, U), x == t) => (u: U); sadly, refinement won't compile
def pi[T](t: T)(implicit mapping: Sigma[T] { val x = t }): mapping.U
Недостающим элементом здесь является возможность статически ограничить поле x ожидаемым значением t, эффективно формируя уравнение, представляющее свойство всех значений, населяющих тип T. Вместе с нашими Σ-типами, используемыми для выражения существования объекта с данным свойством, формируется логика, в которой наше уравнение является теоремой, подлежащей доказательству.
Примечательно, что в реальном случае теорема может быть весьма нетривиальной, вплоть до того момента, когда она не может быть автоматически получена из кода или решена без значительных усилий. Можно даже сформулировать гипотезу Римана таким образом, только чтобы найти сигнатуру, которую невозможно реализовать, фактически не доказав ее, не зацикливая навсегда или не создавая исключение.
Вопрос заключался в том, чтобы использовать функцию зависимой типизации более напрямую, и, на мой взгляд, было бы полезно иметь более прямой подход зависимой типизации, чем тот, который предлагает Scala.
Текущие ответы пытаются поставить вопрос на теоретическом уровне. Я хочу сделать это более прагматичным. Это может объяснить, почему люди разделяются по уровню поддержки зависимых типов в языке Scala. Мы можем иметь в виду несколько иные определения. (не сказать, что один прав, а другой неправ).
Это не попытка ответить на вопрос, насколько легко было бы превратить Scala в нечто вроде Idris (я думаю, что это очень сложно) или написать библиотеку, предлагающую более прямую поддержку возможностей, подобных Idris (например, singletons пытается быть в Хаскеле).
Вместо этого я хочу подчеркнуть прагматическую разницу между Scala и таким языком, как Идрис.
Что такое биты кода для выражений уровня и типа? Идрис использует один и тот же код, а Scala - совсем другой.
Scala (подобно Haskell) может кодировать множество вычислений на уровне типов. Это показано такими библиотеками, как shapeless, Эти библиотеки делают это, используя действительно впечатляющие и умные приемы. Тем не менее, их код уровня типа (в настоящее время) довольно сильно отличается от выражений уровня значений (я считаю, что этот пробел в Хаскеле несколько ближе). Идрис позволяет использовать выражение уровня значения на уровне типа КАК ЕСТЬ.
Очевидным преимуществом является повторное использование кода (вам не нужно кодировать выражения уровня типа отдельно от уровня значения, если они нужны в обоих местах). Должно быть намного проще написать код уровня значения. Должно быть проще не иметь дело с взломами типа синглетонов (не говоря уже о стоимости производительности). Вам не нужно учить две вещи, вы узнаете одну вещь. На прагматическом уровне нам нужно меньше понятий. Тип синонимов, семейства типов, функции,... как насчет просто функций? На мой взгляд, это объединяющее преимущество гораздо глубже и больше, чем синтаксическое удобство.
Рассмотрим проверенный код. Увидеть:
https://github.com/idris-lang/Idris-dev/blob/v1.3.0/libs/contrib/Interfaces/Verified.idr
Средство проверки типов проверяет доказательства монадических / функторных / аппликативных законов, и доказательства касаются фактических реализаций монады / функтора / аппликативного, а не некоторого зашифрованного эквивалента уровня типа, который может быть одинаковым или не одинаковым. Большой вопрос в том, что мы доказываем?
То же самое можно сделать с помощью хитрых трюков с кодировкой (см. Ниже для версии на Haskell, я не видел ни одного для Scala)
https://blog.jle.im/entry/verified-instances-in-haskell.html
https://github.com/rpeszek/IdrisTddNotes/wiki/Play_FunctorLaws
за исключением того, что типы настолько сложны, что трудно увидеть законы, выражения уровня значений преобразуются (автоматически, но все же) в вещи уровня типов, и вам также нужно доверять этому преобразованию. Во всем этом есть место для ошибки, которая как бы противоречит цели компилятора, выполняющего роль помощника по проверке.
(EDITED 2018.8.10) Говоря о помощи в доказательстве, здесь есть еще одно большое различие между Идрисом и Скалой. В Scala (или Haskell) нет ничего, что могло бы помешать написанию расходящихся доказательств:
case class Void(underlying: Nothing) extends AnyVal //should be uninhabited
def impossible() : Void = impossible()
в то время как Идрис total ключевое слово, предотвращающее компиляцию кода, подобного этому.
Библиотека Scala, которая пытается унифицировать код значения и уровня типа (например, Haskell singletons) было бы интересным тестом для поддержки Scala зависимых типов. Может ли такая библиотека быть намного лучше в Scala из-за зависимых от пути типов?
Я слишком новичок в Скале, чтобы ответить на этот вопрос сам.