GADT 提供了哪些 OOP 和泛型无法实现的功能？

Question

函数式语言中的 GADTs 等同于传统的 OOP + generics，或者在某些情况下，正确性约束很容易被强制执行GADT 但很难或不可能使用 Java 或 C#?

例如，这个"well-typed interpreter"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 ... */

Answer 1

OOP classes 是开放的，GADT 是封闭的（就像普通的 ADT）。

在这里，"open" 意味着你以后总是可以添加更多的子classes，因此编译器不能假设可以访问给定 class 的所有子classes =85=]。（有一些例外，例如 Java 的 final 会阻止任何子 classing，以及 Scala 的密封 classes）。相反，从某种意义上说，ADT 是 "closed"，您以后不能添加更多的构造函数，并且编译器知道这一点（并且可以利用它来检查例如详尽性）。有关详细信息，请参阅“expression problem”。

考虑以下代码：

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 是唯一可以同时生成 A t 和 B t 的类型 t。关闭的 GADT 可以确保这一点。如果我们尝试使用 OOP classes 来模仿它，我们会失败：

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 and/or String 实现所述方法。

在这种特定情况下，可以简单地求助于非通用函数：

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

或者，等效地，向那些 classes 添加一个非泛型方法。但是，A 和 B 之间共享的类型可能比单例 Char 更大。更糟糕的是，classes 是开放的，所以一旦添加一个新的 subclass.

，集合就会变大

此外，即使你有一个 A<Char> 类型的变量，你仍然不知道它是否是 A1，因此你无法访问 A1' s 字段，除非使用类型转换。此处的类型转换是安全的，因为程序员知道 A<Char> 没有其他子 class。在一般情况下，这可能是错误的，例如

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

此处 A<Char> 必须是 A1 和 A2<Char> 的超class。

@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>) 的情况下由 class Teq1. 该接口需要一个从 A 到 B 的转换函数 foo，以及一个 "transitivity proof" trans，给定 this 类型 Teq<A,B> 和 Teq<B,C> 类型的 x 可以生成一个对象 Teq<A,C>。这是 Java 类似于上面使用 GADT 的 Haskell 代码。

class 在 A/=B 时无法安全实施，据我所知：它需要返回空值或不终止作弊。

Answer 2

泛型不提供类型相等约束。没有它们，您需要依赖向下转换，即失去类型安全性。此外，某些调度——尤其是访问者模式——无法安全地实现，也无法使用类似于 GADT 的泛型的适当接口。请参阅本文，调查这个问题：

Generalized Algebraic Data Types and Object-Oriented Programming
安德鲁·肯尼迪，克劳迪奥·罗素。 OOPSLA 2005.

GADT 提供了哪些 OOP 和泛型无法实现的功能？

What does GADT offer that cannot be done with OOP and generics?

generics

ocaml

haskell

type-theory

gadt