TypeRep與「類型」GADT之間的關係

Question

在Scrap your boilerplate reloaded中，作者描述了Scrap Your Boilerplate的新演示文稿，它應該與原文相同。

然而，一個區別是，它們假定一個有限的，閉集「基地」類型，具有GADT

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

在原始SYB，用於類型安全鑄造編碼，採用了Typeable實現類。

我的問題是：

• 什麼是這兩種方法之間的關係？
• 爲什麼選擇「SYB Reloaded」演示文稿的GADT表示形式？

Answer 1

[我的「SYB重裝上陣」論文的作者之一。]

TL; DR我們真的只是使用它，因爲它看起來更漂亮給我們。基於類的Typeable方法更實用。 Spine視圖可以與Typeable類組合使用，並且不依賴於Type GADT。

文章指出這在其結論：

我們實現處理泛型編程的兩個核心成分不同於原來的SYB紙：我們使用重載函數基於 明確的類型參數，而不是重載函數一個類型安全的 轉換1或基於類的可擴展方案[20];我們使用顯式脊柱 視圖而不是基於組合器的方法。兩者的變化都是彼此獨立的，並且考慮到清楚：我們認爲SYB方法的結構在我們的設置中更加明顯，並且PolyP和Generic Haskell的關係 變得更清晰。我們發現儘管 spine視圖在可編寫的通用函數類中是有限的，但它適用於非常大的一類數據類型（包括GADT），它是 。

因爲使用顯式類型參數的 重載函數的編碼需要Type的數據類型和諸如toSpine之類的函數的可擴展性，所以我們的方法不能輕易用作庫。然而，人們可以將Spine結合到SYB庫中，同時仍然使用SYB 論文的技術來編碼重載函數。

因此，使用GADT進行類型表示的選擇是我們主要爲了清晰起見而做出的選擇。正如Don在他的回答中所說的那樣，在這種表示中有一些明顯的優點，即它維護關於類型表示的類型的靜態信息，並且它允許我們在沒有任何進一步魔法的情況下實現施放，特別是沒有使用的unsafeCoerce。類型索引函數也可以直接通過在類型上使用模式匹配來實現，而不必返回到各種組合器，如mkQ或extQ。

事實是，我（和我認爲共同作者）根本不喜歡Typeable類。 （事實上​​，我仍然沒有，儘管它現在終於變得更加有紀律了，因爲GHC爲Typeable增加了自動派生，使其具有種類多態性，並且最終將刪除定義自己實例的可能性。）此外，Typeable還沒有像現在這樣廣爲人知，因此它似乎很有吸引力，可以用GADT編碼來「解釋」它。此外，當時我們還在考慮向Haskell添加open datatypes，從而緩解了GADT關閉的限制。總結：如果你實際上只需要一個封閉的宇宙的動態類型信息，我總是會選擇GADT，因爲你可以使用模式匹配來定義類型索引函數，而且你不必依靠unsafeCoerce也不是先進的編譯器魔術。然而，如果宇宙是開放的，但是這對於通用編程環境來說非常普遍，那麼GADT方法可能具有啓發性，但是不實際，並且使用Typeable是一條路。

然而，我們也是在本文的結論狀態下，Type超過Typeable選擇不是因爲我們正在做，即使用Spine視圖中的其他選擇，我認爲這是更重要的先決條件真的是論文的核心。

該論文本身顯示了（在第8節）一個靈感來源於"Scrap your Boilerplate with Class"論文的變體，該論文使用帶有類約束的Spine視圖。但我們也可以做一個更直接的發展，我將在下面展示。對於這一點，我們將使用Typeable從Data.Typeable，但定義我們自己Data類，爲簡單起見，只包含toSpine方法：

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

的Spine數據類型現在使用Data約束：

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

函數fromSpine與其他表示法一樣微不足道：

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

個

實例爲Data是微不足道的扁平類型，如Int：

instance Data Int where 
    toSpine = Constr 

而且他們還在爲結構化類型十分簡單，例如二叉樹：

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 

本文然後繼續和定義各種通用功能，例如mapQ。這些定義很難改變。我們只得到一流的約束Data a =>，其中紙具有​​函數參數：

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] 

更高級別的功能，如everything也剛剛失去了明確的類型參數（然後竟然長得一模一樣的原SYB） ：

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

正如我前面所說，如果我們現在要定義一個通用和功能總結所有Int事件，我們不能模式匹配了，但有回落到mkQ，但mkQ是在這些方面完全定義Typeable和完全獨立的Spine：

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

然後（又完全按照原來的SYB）：

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

sumQ :: Query Int 
sumQ = mkQ 0 id 

對於後面的紙一些東西（例如，添加構造信息），一個需要更多的工作，但這一切都可以完成。所以使用Spine真的不依賴於使用Type。

Answer 2

好吧，顯然Typeable的使用是開放的 - 可以在事後添加新的變體，而不需要修改原始定義。

雖然重要的變化是因爲TypeRep是無類型的。也就是說，運行時類型TypeRep與其編碼的靜態類型之間沒有關聯。使用GADT方法，我們可以對GADT Type a給出的類型a和它的Type之間的映射進行編碼。

因此，我們烘焙了類型rep與其來源類型靜態鏈接，並且可以使用Type a編寫靜態類型的動態應用程序（例如），作爲我們有運行時a的證據。

在舊的TypeRep案例中，我們沒有這樣的證據，它歸結爲運行時字符串相等，以及通過fromDynamic獲得最佳答案和希望。

比較簽名：

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

與GADT風格：

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

我不能假的我喜歡的類型證據，我可以重建的事情，當使用後，對如當我擁有的是Type a時，查找a的類型類實例。