Есть ли причина, по которой scala явно не поддерживает зависимые типы?

Существуют типы, зависящие от пути, и я думаю, что в Scala можно выразить почти все функции таких языков, как Epigram или Agda, но мне интересно, почему Scala не поддерживает это более явно, как это очень хорошо в других областях (скажем, , DSL)? Что-нибудь, что мне не хватает, например, «это не обязательно»?

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

Встроенная поддержка зависимых типов в 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 намного ближе к этим другим языкам, чем это обычно считается.

Несмотря на терминологию, типы зависимых сумм (также известные как типы сигма) - это просто пара значений, где тип второго значения зависит от первого значения. Это можно напрямую представить в 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 types).

Зависимые типы продуктов (также известные как 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 -свидетеля подтипа, а не =:=потому, что res2.typeи res3.typeявляются одноэлементными типами и, следовательно, более точными, чем типы, которые мы проверяем на RHS).

Однако на практике в Scala мы не начинаем с кодирования типов Sigma и Pi, а затем продолжаем оттуда, как в Agda или Idris. Вместо этого мы будем напрямую использовать типы, зависящие от пути, одиночные типы и имплициты. Вы можете найти множество примеров того, как это проявляется в бесформенных: типы с размерами , расширяемые записи , исчерпывающие списки HList , отбросьте свой шаблон , общие застежки-молнии и т. Д. И т. Д.

Единственное оставшееся возражение, которое я вижу, заключается в том, что в приведенном выше кодировании типов Pi мы требуем, чтобы одноэлементные типы зависимых значений были выражены. К сожалению, в Scala это возможно только для значений ссылочных типов, но не для значений не ссылочных типов (особенно, например, Int). Это позор, но не внутренняя трудность: тип проверки Scala представляет типы одноэлементные из не-эталонных значений внутри, и там было несколько из экспериментов сделать их непосредственно представимы. На практике мы можем обойти проблему с помощью довольно стандартного кодирования натуральных чисел на уровне типов .

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

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

Я считаю, что зависящие от пути типы в Scala могут представлять только Σ-типы, но не Π-типы. Это:

trait Pi[T] { type U }

не совсем Π-тип. По определению, Π-тип или зависимый продукт - это функция, тип результата которой зависит от значения аргумента, представляющего универсальный квантор, то есть ∀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 во что-то вроде Идриса (я думаю, очень сложно) или написать библиотеку, предлагающую более прямую поддержку возможностей, подобных Идрису (например, singletons пытается быть в Haskell).

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

Scala (аналогично Haskell) может кодировать множество вычислений на уровне типов. Это показывают библиотеки вроде shapeless. Эти библиотеки делают это с помощью действительно впечатляющих и умных приемов. Однако их код уровня типа (в настоящее время) сильно отличается от выражений уровня значений (я считаю, что этот пробел в Haskell несколько ближе). Идрис позволяет использовать выражение уровня значения на уровне типа КАК ЕСТЬ.

Очевидным преимуществом является повторное использование кода (вам не нужно кодировать выражения уровня типа отдельно от уровня значения, если они нужны в обоих местах). Должно быть намного проще писать код ценностного уровня. Должно быть проще не иметь дело с хаками, такими как синглтоны (не говоря уже о стоимости производительности). Вам не нужно изучать две вещи, вы узнаете одну вещь. На прагматическом уровне нам нужно меньше концепций. Синонимы типов, семейства типов, функции ... как насчет только функций? На мой взгляд, эти объединяющие преимущества гораздо глубже и заключаются не только в удобстве синтаксиса.

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

(Отредактировано 2018.8.10) Говоря о помощи с доказательствами, вот еще одна большая разница между Idris и Scala. В Scala (или Haskell) нет ничего, что могло бы помешать написанию расходящихся доказательств:

case class Void(underlying: Nothing) extends AnyVal //should be uninhabited
def impossible() : Void = impossible()

в то время как у Идриса есть totalключевое слово, предотвращающее компиляцию такого кода.

Библиотека Scala, которая пытается объединить код уровня значения и типа (например, Haskell singletons), могла бы стать интересным тестом для поддержки Scala зависимых типов. Можно ли сделать такую ​​библиотеку намного лучше в Scala из-за типов, зависящих от пути?

Я слишком новичок в Scala, чтобы сам отвечать на этот вопрос.