GADTs so với MultiParamTypeClasses

Question

Tôi đang cố gắng nắm bắt GADTs và tôi đã xem GADTs example trong hướng dẫn sử dụng của GHC. Theo như tôi có thể nói, nó có thể làm điều tương tự với MultiParamTypeClasses:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, 
    FlexibleInstances, UndecidableInstances #-} 

class IsTerm a b | a -> b where 
    eval :: a -> b 

data IntTerm = Lit Int 
       | Succ IntTerm 
data BoolTerm = IsZero IntTerm 
data If p a = If p a a 
data Pair a b = Pair a b 

instance IsTerm IntTerm Int where 
    eval (Lit i)  = i 
    eval (Succ t)  = 1 + eval t 

instance IsTerm BoolTerm Bool where 
    eval (IsZero t) = eval t == 0 

instance (IsTerm p Bool, IsTerm a r) => IsTerm (If p a) r where 
    eval (If b e1 e2) = if eval b then eval e1 else eval e2 

instance (IsTerm a c, IsTerm b d) => IsTerm (Pair a b) (c, d) where 
    eval (Pair e1 e2) = (eval e1, eval e2) 

Lưu ý rằng chúng ta có các nhà thầu cùng chính xác và mã chính xác tương tự cho eval (lây lan qua các định nghĩa ví dụ) như trong Ví dụ GADTs của GHC.

Vì vậy, tất cả các fuzz về GADTs là gì? Tôi có thể làm gì với GADTs mà tôi không thể thực hiện với MultiParamTypeClasses không? Hay họ chỉ cung cấp một cách súc tích hơn để làm những việc mà tôi có thể làm với MultiParamTypeClasses thay vào đó?

Answer 1

Bạn có thể đặt giá trị GADT cùng loại nhưng với nhà thầu khác nhau vào một container thuận tiện,

map eval [Lit 1, If (IsZero (Lit 3)) (Lit 4) (Succ (Lit 6))] 

là đơn giản, nhưng để có được cùng sử dụng các loại khác nhau và MPTCs với phụ thuộc hàm là khó khăn tại ít nhất . Trong cách tiếp cận lớp kiểu Multiparameter của bạn, Lit và If là các hàm tạo của các kiểu khác nhau, do đó, chúng ta sẽ cần một kiểu trình bao bọc để đưa chúng vào cùng một vùng chứa. Các loại wrapper sẽ, như xa như tôi có thể thấy, cần phải là một kiểu hiện sinh à la

data Wrap t = forall a. (IsTerm a t) => Wrapper a 

với một

instance IsTerm (Wrap t) t where 
    eval (Wrapper e) = eval e 

để đảm bảo một số an toàn loại và khả năng map các chức năng như eval trên danh sách. Vì vậy, bạn đang nửa đường trở lại GADT, trừ đi sự tiện lợi.

Tôi không chắc chắn có bất kỳ GADT nào cho phép bạn thực hiện điều đó mà bạn không thể đạt được nếu không có chúng, nhưng một số thứ sẽ hi sinh rất nhiều của sự sang trọng.

Answer 2

GADTs chỉ cho phép bạn cung cấp cách xây dựng tự nhiên dễ dàng hơn và cho phép sử dụng khớp trên cấp loại và nhà xây dựng với nhau (là thứ bạn không thể làm mà không có nó).

{-# LANGUAGE GADTs #-} 
data Term a = (a ~ Bool) => IsZero (Term Int) 
      | (a ~ Int) => Lit Int 
eval :: Term a -> a 
eval (IsZero t) = eval t == 0 
eval (Lit a) = a