Чем экзистенциальные типы отличаются от интерфейсов?

Учитывая экзистенциальный тип

T = ∃X.{op₁:X, op₂:X→boolean}

и этот общий интерфейс Java:

interface T<X> {
    X op₁();
    boolean op₂(X something);
}

Каковы принципиальные различия между экзистенциальным типом и интерфейсом Java?

Очевидно, что есть синтаксические различия и объектная ориентация Java (которая также включает такие детали, как скрытые thisпараметры и т. Д.). Меня не столько интересуют, сколько концептуальные и семантические различия - хотя, если кто-то хотел бы пролить свет на некоторые более тонкие моменты (такие как нотационная разница между Tпротив T<X>), это также было бы оценено.

Хм ... Это определение выглядит очень похоже на пример с Haskell, который я видел давно.

{-# LANGUAGE ExistentialQuantification #-}
data X = forall a . X { value :: a, viewValue :: a -> String }
instance Show X where show (X { value = x, viewValue = f}) = f x
sample :: [X]
sample = [X 3 show, X "abc" show, X 3.14 show]

Когда конструктор Xприменяется, фактически становится ∃. Обратите внимание, что когда вы вынимаете, valueвы не знаете тип и имеете пустой набор операций над ним. Но поскольку viewValueэто в некотором роде согласуется с valueэтим, к нему можно применить.

Я предполагаю, что основным отличием Java, которое interfaceвы предложили, является то, что вы должны знать промежуточный тип для передачи результата op₁в op₂. Т.е. правильная система для экзистенциального типа должна выбирать правильный тип, который гарантированно существует по условию. Т.е. вы должны быть в состоянии написать функцию с типом: ∀X. X→(X→boolean)→T. В предыдущем примере такая функция Xиспользуется в конструкторе X 3 show( showэто функция, которая принимает аргумент любого типа, который реализует Showи возвращает String)

Обновлено: я просто перечитал ваш вопрос и думаю, что у меня есть правильная конструкция для Java:

interface T {
    boolean op₂();
}
...
T x = new T() {
    private final int op₁ = ...;
    public boolean op₂() { return ((op₁ % 2) == 0); }
};
T y = new T() {
    private final char op₁ = ...;
    public boolean op₂() { return ('0' <= op₁ && op₁ <= '9'); }
};
if (x.op₂() && y.op₂()) ...

Вы правы насчет упоминания this- это на самом деле ваша работа.

Так что теперь я понял, что классические языки ООП (Java, C #, C ++ и т. Д.) Всегда реализуют экзистенциальный тип с одним значением thisи над ним функции, называемые «методами», которые неявно вызываются с этим значением :)

PS Извините, я не очень знаком с Java, но надеюсь, у вас есть идея.

Разница лишь в том, что интерфейс Java на самом деле что-то значит для компилятора Java.

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

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

Экзистенциальный тип скрывает тип в своей реализации от потребителя. Интуитивно понятно, что для X, чтобы быть экзистенциальным в T, идентичность X не может быть известна ни от одного потребителя; все, что должно быть известно, это набор операций, предоставляемых при определении. Существует один тип T для некоторого типа X.

Напротив, универсальный тип определяет операции, применимые ко всем типам, из которых потребитель может выбирать. Тип интерфейса T именно такой. X создается пользователем, который точно знает, какой тип X. Существует тип T для каждого типа X во вселенной.

Экзистенциалы на самом деле не представлены в Java как языковая конструкция, за исключением ограниченного случая подстановочных знаков ( List<?>). Но да, их можно эмулировать с помощью интерфейсов. Проблема тогда становится больше дизайна.

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