Kết hợp mẫu Haskell trên GADT với kiểu dữ liệu

Question

Tôi thấy rằng tôi thực sự thích kết hợp GADT với kiểu dữ liệu, vì nó mang lại cho tôi sự an toàn hơn trước đây (đối với hầu hết các công dụng, gần như tốt như Coq, Agda và cộng sự). Đáng buồn thay, việc khớp mẫu không thành công trên các ví dụ đơn giản nhất, và tôi có thể nghĩ không có cách nào để viết các hàm của tôi ngoại trừ các lớp kiểu.

Dưới đây là một ví dụ để giải thích nỗi buồn của tôi:

data Nat = Z | S Nat deriving Eq 

data Le :: Nat -> Nat -> * where 
    Le_base :: Le a a 
    Le_S :: Le a b -> Le a (S b) 

class ReformOp n m where 
    reform :: Le (S n) (S m) -> Le n m 

instance ReformOp a a where 
    reform Le_base = Le_base 

instance ReformOp a b => ReformOp a (S b) where 
    reform (Le_S p) = Le_S $ reform p 

class TransThm a b c where 
    trans :: Le a b -> Le b c -> Le a c 

instance TransThm a a a where 
    trans = const 

instance TransThm a a b => TransThm a a (S b) where 
    trans Le_base (Le_S p) = Le_S $ trans Le_base p 

instance (TransThm a b c, ReformOp b c) => TransThm a (S b) (S c) where 
    trans (Le_S p) q = Le_S $ trans p $ reform q 

Chúng tôi có 2 lớp kiểu (một cho định lý, một cho một hoạt động tiện ích) và 5 trường hợp - chỉ dành riêng cho một định lý tầm thường. Lý tưởng nhất, Haskell có thể nhìn vào chức năng này:

-- not working, I understand why 
trans :: Le a b -> Le b c -> Le a c 
trans Le_base Le_base = Le_base 
trans Le_base (Le_S p) = Le_S $ trans Le_base p 
trans (Le_S p) q = Le_S $ trans p $ reform q 

Và kiểu kiểm tra từng khoản ngày của riêng mình, và mỗi gọi quyết định các trường hợp có thể xảy ra (do đó giá trị cố gắng để phù hợp) và không nên khi gọi trans Le_base Le_base Haskell sẽ nhận thấy rằng chỉ có trường hợp đầu tiên cho phép ba biến số giống nhau và chỉ thử khớp với mệnh đề đầu tiên.

Answer 1

Tôi không thấy định nghĩa phù hợp với mẫu của bạn là trans sẽ hoạt động như thế nào trong Agda hoặc Coq.

Nếu bạn viết như sau thay vào đó, nó hoạt động:

reform :: Le (S n) (S m) -> Le n m 
reform Le_base   = Le_base 
reform (Le_S Le_base) = Le_S Le_base 
reform (Le_S (Le_S p)) = Le_S (reform (Le_S p)) 

trans :: Le a b -> Le b c -> Le a c 
trans Le_base q  = q 
trans (Le_S p) Le_base = Le_S p 
trans (Le_S p) (Le_S q) = Le_S (trans p (reform (Le_S q))) 

Tất nhiên, bạn cũng có thể trực tiếp hơn xác định:

trans :: Le a b -> Le b c -> Le a c 
trans p Le_base = p 
trans p (Le_S q) = Le_S (trans p q)