Mối quan hệ giữa TypeRep và "Loại" GADT

Question

Trong Scrap your boilerplate reloaded, các tác giả mô tả bản trình bày mới là Scrap Your Boilerplate, được cho là tương đương với bản gốc.

Tuy nhiên, một sự khác biệt là họ giả định một hữu hạn, đóng tập hợp các loại "cơ sở", mã hóa với một GADT

data Type :: * -> * where 
    Int :: Type Int 
    List :: Type a -> Type [a] 
    ... 

Trong SYB gốc, loại an toàn dàn diễn viên được sử dụng, thực hiện bằng cách sử dụng Typeable lớp học.

Câu hỏi của tôi là:

• mối quan hệ giữa hai phương pháp này là gì?
• Tại sao biểu diễn GADT được chọn cho bản trình bày "Đã tải lại SYB"?

Answer 1

[Tôi là một trong các tác giả của bài báo "SYB Reloaded".]

TL; DR Chúng tôi thực sự chỉ sử dụng nó bởi vì nó có vẻ đẹp hơn cho chúng tôi. Cách tiếp cận Typeable dựa trên lớp học thực tế hơn. Chế độ xem Spine có thể được kết hợp với lớp Typeable và không phụ thuộc vào Type GADT.

Các trạng thái giấy này trong kết luận của mình:

thực hiện của chúng tôi xử lý hai thành phần trung tâm của chương trình chung khác với giấy SYB gốc: chúng tôi sử dụng các chức năng quá tải với đối số kiểu tường minh thay vì chức năng quá tải dựa trên một loại an toàn truyền 1 hoặc lược đồ có thể mở rộng dựa trên lớp học [20]; và chúng tôi sử dụng cột sống rõ ràng xem thay vì cách tiếp cận dựa trên tổ hợp. Cả hai thay đổi là độc lập của nhau, và đã được thực hiện với sự rõ ràng trong tâm trí: chúng tôi nghĩ rằng cấu trúc của cách tiếp cận SYB là dễ thấy hơn trong thiết lập của chúng tôi, và quan hệ để PolyP và Generic Haskell trở nên rõ ràng hơn. Chúng tôi đã tiết lộ rằng trong khi chế độ xem cột sống bị giới hạn trong lớp chức năng chung có thể được viết, nó là áp dụng cho một loại rất lớn các loại dữ liệu, bao gồm GADT.

Cách tiếp cận của chúng tôi không thể sử dụng dễ dàng như thư viện, vì mã hóa của chức năng quá tải sử dụng đối số loại rõ ràng yêu cầu khả năng mở rộng loại dữ liệu kiểu và chức năng như toSpine. Tuy nhiên, người ta có thể kết hợp cột sống vào thư viện SYB trong khi vẫn sử dụng các kỹ thuật của các giấy tờ SYB để mã hóa các chức năng quá tải.

Vì vậy, việc lựa chọn sử dụng GADT cho biểu diễn kiểu là sự lựa chọn của chúng tôi chủ yếu để làm rõ. Như Don nói trong câu trả lời của mình, có một số lợi thế rõ ràng trong biểu diễn này, cụ thể là nó duy trì thông tin tĩnh về kiểu đại diện kiểu, và nó cho phép chúng ta thực hiện phép đúc mà không cần thêm bất kỳ phép thuật nào, và đặc biệt không sử dụng của unsafeCoerce. Các chức năng đánh chỉ mục cũng có thể được thực hiện trực tiếp bằng cách sử dụng đối sánh mẫu trên loại và không quay trở lại các bộ phối hợp khác nhau như mkQ hoặc extQ.

Sự thật là tôi (và tôi nghĩ rằng các đồng tác giả) không đơn giản là rất thích lớp học Typeable. (Trong thực tế, tôi vẫn không, mặc dù nó cuối cùng đã trở thành một chút kỷ luật hơn bây giờ trong đó GHC thêm tự động bắt nguồn cho Typeable, làm cho nó loại đa hình, và cuối cùng sẽ loại bỏ khả năng để xác định trường hợp của riêng bạn.) Ngoài ra, Typeable không hoàn toàn được thiết lập và được biết đến rộng rãi vì nó có lẽ bây giờ, do đó, nó dường như hấp dẫn để "giải thích" nó bằng cách sử dụng mã hóa GADT. Và hơn nữa, đây là lúc chúng tôi cũng nghĩ đến việc thêm open datatypes vào Haskell, do đó làm giảm bớt sự hạn chế mà GADT bị đóng. Vì vậy, để tóm tắt: Nếu bạn thực sự cần thông tin kiểu động chỉ cho một vũ trụ khép kín, tôi luôn đi cho GADT, bởi vì bạn có thể sử dụng mẫu phù hợp để xác định các hàm được lập chỉ mục kiểu, và bạn không phải dựa trên unsafeCoerce cũng không phải là phép thuật trình biên dịch tiên tiến. Tuy nhiên, nếu vũ trụ mở, khá phổ biến, chắc chắn đối với cài đặt lập trình chung, thì cách tiếp cận GADT có thể mang tính hướng dẫn, nhưng không thực tế và sử dụng Typeable là cách để thực hiện.

Tuy nhiên, vì chúng tôi cũng nêu trong kết luận của bài báo, lựa chọn Type trên Typeable không phải là điều kiện tiên quyết cho lựa chọn khác mà chúng tôi đang thực hiện, cụ thể là sử dụng chế độ xem Spine. và thực sự là cốt lõi của bài báo.

Bản thân giấy hiển thị (trong Phần 8) một biến thể lấy cảm hứng từ giấy "Scrap your Boilerplate with Class", sử dụng chế độ xem Spine với ràng buộc lớp thay thế. Nhưng chúng tôi cũng có thể thực hiện một sự phát triển trực tiếp hơn, mà tôi trình bày sau đây.Đối với điều này, chúng tôi sẽ sử dụng Typeable từ Data.Typeable, nhưng định nghĩa lớp Data riêng của chúng tôi mà, vì đơn giản, chỉ chứa toSpine phương pháp:

class Typeable a => Data a where 
    toSpine :: a -> Spine a 

Các Spine datatype bây giờ sử dụng các Data chế:

data Spine :: * -> * where 
    Constr :: a -> Spine a 
    (:<>:) :: (Data a) => Spine (a -> b) -> a -> Spine b 

Chức năng fromSpine là tầm thường như với các đại diện khác:

fromSpine :: Spine a -> a 
fromSpine (Constr x) = x 
fromSpine (c :<>: x) = fromSpine c x 

Instances cho Data là tầm thường với nhiều loại phẳng như Int:

instance Data Int where 
    toSpine = Constr 

Và họ vẫn hoàn toàn đơn giản với nhiều loại có cấu trúc như cây nhị phân:

data Tree a = Empty | Node (Tree a) a (Tree a) 

instance Data a => Data (Tree a) where 
    toSpine Empty  = Constr Empty 
    toSpine (Node l x r) = Constr Node :<>: l :<>: x :<>: r 

giấy này sau đó đi vào và định nghĩa các hàm chung khác nhau, chẳng hạn như mapQ. Những định nghĩa này hầu như không thay đổi. Chúng tôi chỉ nhận được những hạn chế lớp cho Data a => nơi giấy có đối số chức năng của Type a ->: chức năng

mapQ :: Query r -> Query [r] 
mapQ q = mapQ' q . toSpine 

mapQ' :: Query r -> (forall a. Spine a -> [r]) 
mapQ' q (Constr c) = [] 
mapQ' q (f :<>: x) = mapQ' q f ++ [q x] 

cao cấp như everything cũng chỉ mất đối số kiểu tường minh của họ (và sau đó thực sự nhìn chính xác giống như trong ban SYB) :

everything :: (r -> r -> r) -> Query r -> Query r 
everything op q x = foldl op (q x) (mapQ (everything op q) x) 

Như tôi đã nói ở trên, nếu bây giờ chúng tôi muốn xác định một hàm sum generic tổng hợp tất cả Int lần xuất hiện, chúng ta không thể mô hình phù hợp nữa, nhưng phải rơi trở lại mkQ, nhưng mkQ được xác định hoàn toàn về trong số Typeable và hoàn toàn độc lập Spine:

mkQ :: (Typeable a, Typeable b) => r -> (b -> r) -> a -> r 
(r `mkQ` br) a = maybe r br (cast a) 

Và rồi (một lần nữa chính xác như trong ban SYB):

sum :: Query Int 
sum = everything (+) sumQ 

sumQ :: Query Int 
sumQ = mkQ 0 id 

Đối với một số những thứ sau này trong bài báo (ví dụ, thêm thông tin constructor), một công việc nhiều hơn một chút là cần thiết, nhưng tất cả có thể được thực hiện. Do đó, việc sử dụng Spine thực sự không phụ thuộc vào việc sử dụng Type.

Answer 2

Vâng, rõ ràng việc sử dụng Typeable là mở - các biến thể mới có thể được thêm vào sau thực tế và không sửa đổi định nghĩa ban đầu.

Thay đổi quan trọng là mặc dù trong đó TypeRep không được nhập. Tức là, không có kết nối giữa kiểu thời gian chạy, TypeRep và loại tĩnh nó mã hóa. Với phương pháp GADT, chúng tôi có thể mã hóa ánh xạ giữa một loại a và Type của GADT do GADT Type a đưa ra.

Do đó, chúng tôi có bằng chứng cho loại đại diện được liên kết tĩnh với loại gốc và có thể viết ứng dụng động được nhập tĩnh (ví dụ) sử dụng Type a làm bằng chứng rằng chúng tôi có thời gian chạy a.

Trong trường hợp TypeRep cũ hơn, chúng tôi không có bằng chứng như vậy và nó đi xuống bình đẳng chuỗi thời gian chạy, và ép buộc và hy vọng cho tốt nhất thông qua fromDynamic.

Hãy so sánh chữ ký:

toDyn :: Typeable a => a -> TypeRep -> Dynamic 

so GADT phong cách:

toDyn :: Type a => a -> Type a -> Dynamic 

tôi không thể giả loại bằng chứng của tôi, và tôi có thể sử dụng sau khi xây dựng lại mọi thứ, để ví dụ tra cứu các thể loại lớp cho a khi tất cả tôi có là Type a.