Existential types и dependent types — это два разных подхода к работе с абстракцией и типовой системой в языке программирования. Оба механизма позволяют выразить более гибкие и мощные гарантии типов, но делают это принципиально разными способами.

Existential Types (экзистенциальные типы)

Суть: экзистенциальный тип говорит: "Существует какой-то тип T, но мне не нужно знать, что это за тип, только то, что он удовлетворяет некоторым свойствам."

Пример на человеческом языке:

"У меня есть некий контейнер, в котором лежит что-то, но я не знаю, что это. Я лишь знаю, что это соответствует определённому интерфейсу или контракту."

Синтаксис в Scala:

trait Animal {
def speak(): String
}
val zoo: List\[Animal\] = List(new Dog, new Cat) // тип известен — Animal
val something: List\[_ <: Animal\] = List(new Dog, new Cat) // экзистенциальный тип

Другой пример:

def processList(xs: List\[\_\]): Unit = {
xs.foreach(println)
}

В этом случае List[_] означает: список чего-то, и это "что-то" — существует, но тип неизвестен.

Более формально:

trait Wrapper {
type A
val value: A
}

Здесь A — экзистенциальный тип, он существует, но вне Wrapper мы не знаем, что это за тип.

Когда это полезно:

• Когда ты хочешь скрыть конкретный тип, но гарантировать, что он существует.

• Когда важно абстрагироваться от типа в API, не раскрывая конкретику.

• При проектировании обобщённых интерфейсов, плагинов, обёрток, DSL-ов.

Dependent Types (зависимые типы)

Суть: тип может зависеть от значения. Это принципиально более мощная концепция, чем у экзистенциальных типов.

Пример на человеческом языке:

"Тип возвращаемого значения зависит от входного значения."
Или: "Если я передал n = 5, то возвращаемый тип должен отражать, что длина массива — ровно 5."

Dependent types — не часть Scala напрямую (но поддерживаются частично), а основной элемент языков вроде Idris, Agda, Coq, частично в Dotty (Scala 3).

Пример на теоретическом уровне:

Vec : Type -> Nat -> Type -- Вектор с длиной, зашитой в тип

В Idris можно написать:

append : Vec a n -> Vec a m -> Vec a (n + m)

Тип возвращаемого вектора зависит от значений n и m, переданных как параметры.

Частичная поддержка в Scala:

В Scala можно получить зависимость типов от значений через path-dependent types:

class Outer {
class Inner
}
val outer1 = new Outer
val outer2 = new Outer
val x: outer1.Inner = new outer1.Inner // OK
val y: outer2.Inner = new outer2.Inner // OK
// val z: outer1.Inner = new outer2.Inner // Ошибка: другой тип

Здесь тип Outer#Inner зависит от конкретного значения outer1 или outer2.

Ещё пример:

trait Container {
type Elem
def get: Elem
}

Тип Elem зависит от экземпляра Container. Это path-dependent type, одна из форм зависимых типов в Scala.

Сравнение

Использование в практике

• Existential types часто применяются в Scala 2, особенно в случаях, где тип должен быть скрыт, но важно, что он есть.

• Dependent types позволяют доказать корректность программ на уровне компиляции, но в Scala применяются ограниченно, зато широко — в языках, ориентированных на формальную верификацию и доказательства.

Существуют и гибридные подходы. Scala 3/Dotty стремится расширить поддержку зависимых типов и выразительных типов вообще.