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和泛型不能做什麼？

回答

相關問題