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一样).

这里,"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可以确保这一点.如果我们尝试使用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和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从A对B,和一个"证明传递" trans,其给定的this类型的Teq<A,B>和x类型的Teq<B,C>能产生一个对象Teq<A,C>.这是类似于上面使用GADT的Haskell代码的Java.

A/=B就我所见,这个类无法安全地实现:它需要返回空值或者使用非终止作弊.

Answer 2

泛型不提供类型相等约束.如果没有它们,你需要依赖垂头丧气,即失去类型安全.此外,某些调度 - 特别是访问者模式 - 不能安全地实现,并且具有适用于GADT的泛型的适当接口.查看本文,调查这个问题:

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