GADT提供的OOP和泛型不能做什么？

是GADTs功能语言相当于传统的OOP +泛型，或者有一种情况下GADT容易实施正确性约束，但使用Java或C＃很难或不可能实现？GADT提供的OOP和泛型不能做什么？

例如，这种“良好类型的解释”哈斯克尔程序：

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 ... */

来源

2015-04-05 Alex

有趣的问题。也许平等证人？我不确定它们是否可以用Java表示。 – gsg 2015-04-05 06:00:27

没有太多不共享的东西，但GADT使得Java中不可能实现的东西变得非常简单。我曾经用Java编写过'Maybe'类型的代码，总共有70行代码。在Haskell中，如果包含monad/functor实例，则它不会超过10_。 – AJFarmar 2015-04-05 07:26:46

@AJFarmar同意。虽然在Scala中它不像Java那么长。 – chi 2015-04-05 10:28:44

面向对象的类是开放的，GADT是封闭的（就像普通的ADT）。

这里，“开放”意味着你可以随时在以后添加更多的子类，因此编译器不能假设有一个给定类的所有子类访问。（有一些例外，例如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和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，然后将其由类Teq1只执行的情况下A=B（implements Teq<A,A>）的接口。接口需要一个转换函数foo从A到B，和一个“及物证明” trans，这给定Teq<A,B>类型的this和 Teq<B,C>类型的x可以生成一个对象Teq<A,C>。这就是上面使用GADT的Haskell代码的Java类似。

当我看到A/=B时，该类不能安全实现：它需要返回空值或作非终止作弊。

来源

2015-04-05 07:03:19 chi

这里“开放”和“关闭”是什么意思？ – Sibi 2015-04-05 07:46:05

@Sibi编辑包括。 – chi 2015-04-05 07:59:30

啊，我想我现在明白了。谢谢！ – gsg 2015-04-05 08:17:02

泛型不提供类型相等约束。没有他们，你需要依靠沮丧，即失去安全。此外，特定的调度–，访问者模式–不能安全地实施，并且具有适用于类似GADT的泛型的适当界面。请参阅本文中，调查非常问题：

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

来源

2015-04-05 09:14:41

GADT提供的OOP和泛型不能做什么？

回答

相关问题