haskell - GADT 提供了什么是 OOP 和泛型无法做到的？

Question

函数式语言中的 GADT 是否等同于传统的 OOP + 泛型，或者存在这样的情况:GADT 可以轻松实现正确性约束，但使用 Java 或 C# 很难或不可能实现？

例如，这个“类型良好的解释器”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 类是开放的，GADT 是封闭的(就像普通的 ADT)。

在这里，“开放”意味着您以后可以随时添加更多子类，因此编译器不能假定可以访问给定类的所有子类。 (有一些异常(exception)情况，例如 Java 的 final 阻止任何子类化，以及 Scala 的密封类)。相反，ADT 是“关闭的”，因为您以后无法添加更多构造函数，并且编译器知道这一点(并且可以利用它来检查例如穷举性)。有关详细信息，请参阅“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是唯一的类型t哪一个可以同时产生 A t和 B t .关闭的 GADT 可以确保这一点。如果我们尝试使用 OOP 类来模仿这一点，我们会失败:

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可能是比单例更大的集合 Char .更糟糕的是，类是开放的，所以一旦添加一个新的子类，集合就会变得更大。

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

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

这里A<Char>必须是 A1 的父类(super class)和 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; }
}

上面的代码为所有类型对声明了一个接口(interface) A,B ，然后仅在 A=B 的情况下实现( implements Teq<A,A> ) 按类别 Teq1 .
接口(interface)需要转换函数foo来自 A至B ，以及“传递性证明”trans , 其中给出 this类型 Teq<A,B>和
一个 x类型 Teq<B,C>可以产生一个对象Teq<A,C> .这是与上面使用 GADT 的 Haskell 代码类似的 Java。
A/=B 时无法安全实现该类，据我所知:它需要返回空值或不终止作弊。