Что предлагает GADT, что нельзя сделать с ООП и дженериками?

Являются ли GADT в функциональных языках эквивалентными традиционным OOP + generics, или существует сценарий, в котором существуют ограничения корректности, которые легко выполняются GADT, но трудно или невозможно достичь с помощью Java или С#?

Например, этот "хорошо типизированный интерпретатор" программы Haskell:

data Expr a where
  N :: Int -> Expr Int
  Suc :: Expr Int -> Expr Int
  IsZero :: Expr Int -> Expr Bool
  Or :: Expr Bool -> Expr Bool -> Expr Bool

eval :: Expr a -> a
eval (N n) = n
eval (Suc e) = 1 + eval e
eval (IsZero e) = 0 == eval e
eval (Or a b) = eval a || eval b

можно записать эквивалентно в Java с использованием дженериков и соответствующей реализации каждого подкласса, хотя гораздо более подробный:

interface Expr<T> {
    public <T> T eval();
}

class N extends Expr<Integer> {
    private Integer n;

    public N(Integer m) {
        n = m;
    }

    @Override public Integer eval() {
        return n;
    }
}

class Suc extends Expr<Integer> {
    private Expr<Integer> prev;

    public Suc(Expr<Integer> aprev) {
        prev = aprev;
    }

    @Override public Integer eval() {
        return 1 + prev.eval()
    }
}


/** And so on ... */

Ответ 1

OOP классы открыты, GADT закрыты (например, простые ADT).

Здесь "open" означает, что вы всегда можете добавить дополнительные подклассы позже, поэтому компилятор не может предполагать, что он имеет доступ ко всем подклассам данного класса. (Есть несколько исключений, например Java final, которые, тем не менее, предотвращают любые подклассы и Scala закрытые классы). Вместо этого ADT "закрыты" в том смысле, что позднее вы не можете добавлять дополнительные конструкторы, и компилятор знает это (и может использовать его для проверки, например, исчерпывающей). Для получения дополнительной информации см. Проблему .

Рассмотрим следующий код:

data A a where
  A1 :: Char -> A Char
  A2 :: Int  -> A Int

data B b where
  B1 :: Char   -> B Char
  B2 :: String -> B String

foo :: A t -> B t -> Char
foo (A1 x) (B1 y) = max x y

Приведенный выше код основан на Char, единственном типе t, для которого можно создать как A t, так и B t. GADT, будучи закрытыми, могут обеспечить это. Если мы попытались сопоставить это с использованием классов ООП, мы не получим:

class A1 extends A<Char>   ...
class A2 extends A<Int>    ...
class B1 extends B<Char>   ...
class B2 extends B<String> ...

<T> Char foo(A<T> a, B<T> b) {
      // ??
}

Здесь я думаю, что мы не можем реализовать одно и то же, если не прибегать к небезопасным типам операций, например, к типам. (Более того, они в Java даже не рассматривают параметр t из-за стирания типа.) Мы могли бы подумать о добавлении некоторого общего метода в A или B, чтобы это разрешить, но это заставило бы нас реализовать метод для Int и/или String.

В этом конкретном случае можно просто прибегнуть к не общей функции:

Char foo(A<Char> a, B<Char> b) // ...

или, что то же самое, добавить к этим классам не общий метод. Однако типы, разделяемые между A и B, могут быть более крупными, чем singleton Char. Хуже того, классы открыты, поэтому набор может увеличиться, как только добавится новый подкласс.

Кроме того, даже если у вас есть переменная типа A<Char>, вы по-прежнему не знаете, есть ли это A1 или нет, и из-за этого вы не можете получить доступ к полям A1, кроме как с помощью приведения типов. Приведенный здесь тип будет безопасен только потому, что программист не знает другого подкласса A<Char>. В общем случае это может быть неверно, например

data A a where
  A1 :: Char -> A Char
  A2 :: t -> t -> A t

Здесь A<Char> должен быть суперклассом как A1, так и A2<Char>.

@gsg спрашивает в комментарии о свидетелях равенства. Рассмотрим

data Teq a b where
   Teq :: Teq t t

foo :: Teq a b -> a -> b
foo Teq x = x

trans :: Teq a b -> Teq b c -> Teq a c
trans Teq Teq = Teq

Это можно перевести как

interface Teq<A,B> {
  public B foo(A x);
  public <C> Teq<A,C> trans(Teq<B,C> x);
}
class Teq1<A> implements Teq<A,A> {
  public A foo(A x) { return x; }
  public <C> Teq<A,C> trans(Teq<A,C> x) { return x; }
}

Приведенный выше код объявляет интерфейс для всех пар типов A,B, который затем реализуется только в случае A=B (implements Teq<A,A>) классом Teq1. Для интерфейса требуется функция преобразования foo от A до B и "доказательство транзитивности" trans, которое задано this типа Teq<A,B> и a x типа Teq<B,C> может создать объект Teq<A,C>. Это Java, аналогичный коду Haskell, использующий GADT справа.

Класс не может быть безопасно реализован при A/=B, насколько я могу видеть: для него потребовалось бы либо возвращать нули, либо обманывать без прерывания.

Ответ 2

Дженерики не предоставляют ограничений на равенство типов. Без них вам нужно полагаться на понижение, т.е. Потерять безопасность типа. Кроме того, определенная отправка – в частности, шаблон посетителя – не могут быть реализованы безопасно и с надлежащим интерфейсом для дженериков, похожих на GADT. См. Эту статью, исследуя сам вопрос:

Обобщенные алгебраические типы данных и объектно-ориентированное программирование
Эндрю Кеннеди, Клаудио Руссо. OOPSLA 2005.