13

函数式语言中的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 ... */
4

2 回答 2

14

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

在这里，“开放”意味着您以后可以随时添加更多子类，因此编译器不能假定可以访问给定类的所有子类。（有一些例外情况，例如 Javafinal会阻止任何子类化，以及 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 可以确保这一点。如果我们尝试使用 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>您仍然不知道那是否是 a 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然后该类仅在 case A=B( implements Teq<A,A>) 中实现Teq1。该接口需要一个foo从Ato的转换函数B和一个“传递性证明” trans，给定this的类型Teq<A,B>和x类型Teq<B,C>可以产生一个对象Teq<A,C>。这是与上面使用 GADT 的 Haskell 代码类似的 Java。

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

于 2015-04-05T07:03:19.030 回答
6

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

  广义代数数据类型和面向对象编程
  Andrew Kennedy, Claudio Russo。OOPSLA 2005。

于 2015-04-05T09:14:41.740 回答