數據族vs內注類族

既然我們有內射類型族，那麼在類型族中使用數據族還有什麼用例嗎？數據族vs內注類族

回顧過去有關數據族的StackOverflow問題，幾年前有this question討論類型族和數據族之間的區別，以及this answer關於數據族的用例。兩者都表示數據家族的注入是他們最大的優勢。

看着docs on data families，我看到理由不重寫使用injective type families的數據族的所有用途。

例如，說我有一個數據家人（我已經從合併的文檔一些例子來嘗試在所有數據家庭的功能擠）

data family G a b 
data instance G Int Bool = G11 Int | G12 Bool deriving (Eq) 
newtype instance G() a = G21 a 
data instance G [a] b where 
    G31 :: c -> G [Int] b 
    G32 :: G [a] Bool

我還不如把它改寫爲

type family G a b = g | g -> a b 
type instance G Int Bool = G_Int_Bool 
type instance G() a = G_Unit_a a 
type instance G [a] b = G_lal_b a b 

data G_Int_Bool = G11 Int | G12 Bool deriving (Eq) 
newtype G_Unit_a a = G21 a 
data G_lal_b a b where 
    G31 :: c -> G_lal_b [Int] b 
    G32 :: G_lal_b [a] Bool

不言而喻，數據族的關聯實例對應於具有相同類型族的關聯實例。那麼剩下的唯一區別就是我們在類型名稱空間中的東西少了嗎？

作爲後續，在類型命名空間中擁有更少的東西是否有益處？所有我能想到的是，這將成爲調試地獄的人玩這個在ghci - 構造函數的類型似乎都表明，構造函數都在一個GADT ...

來源

2016-09-26 Alec

我認爲[this]（https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#constraints-in-kinds）可以用數據族完成，而不是type家族，但它甚至不適用於數據族 - 您可以聲明這樣的數據族，但試圖聲明任何實例導致錯誤。 – user2407038

@ user2407038我不確定我是否理解 - 該示例顯然適用於類型系列（正如您提供的鏈接所述），我也可以將它與數據系列一起使用，但我沒有看到它的好處。（數據族T :: a - > *;數據實例T 42 = MkNat;數據實例T「不要恐慌！」= MkSymbol'） – Alec

這些是完全不同的類型;用戶指南中的示例是關於* type *構造函數（不是值構造函數）中的等式約束（'IsTypeLit a〜True'）。你不能對類型族有任何約束，你可以聲明'數據族T :: forall a。（IsTypeLit a〜'True）=> a - > *'但從來沒有任何'T'的實例。 – user2407038

type family T a = r | r -> a 
data family D a

內射型家庭T滿足注入公理

如果T a ~ T b然後a ~ b

但數據系列滿足更強大的生成性公理

如果D a ~ g b然後D ~ g和a ~ b

（如果你喜歡：因爲D實例定義新的類型，可從任何現有的類型不同）

其實D本身是在類型系統中一個合法的類型，不像像T這樣的類型家族，它只能出現在完全飽和的應用中，如T a。這意味着

D可以是參數爲另一種類型的構造，如MaybeT D。（MaybeT T是非法的。）
您可以爲D定義實例，如instance Functor D。（您無法爲類型系列Functor T定義實例，並且無論如何它將無法使用，因爲例如map :: Functor f => (a -> b) -> f a -> f b的實例選擇依賴於從f a類型中可以確定f和a這兩個事實;對於此工作，f不能被允許改變類型系列，甚至內射型）。

來源

2016-09-27 03:28:26

啊哈！這是我失蹤的一塊。非常感謝你 - 這實際上最終導致了我一直在關於生成性（和理查德艾森伯格論文中的「可匹配性」）的混亂。 – Alec

你錯過了另一個細節 - 數據族創建新類型。類型系列只能引用其他類型。特別是，數據族的每個實例都聲明新的構造函數。它很好通用。如果你想要newtype語義，你可以用newtype instance創建一個數據實例。你的實例可以是一個記錄。它可以有多個構造函數。如果你願意，它甚至可以成爲GADT。

這正是type和data/newtype關鍵字之間的差異。內射型家族不會給你新的類型，在你需要的情況下使它們無用。

我明白你來自哪裏。最初我對這個差異有同樣的問題。然後，我終於遇到了一個用例，他們很有用，即使沒有參與類型課程。

我想在不使用類的情況下編寫一個API用於在幾個不同的上下文中處理可變單元格。我知道我想用一個免費的單片機與IO,ST中的解釋器一起使用，也許一些可怕的黑客用unsafeCoerce甚至可以將它鎖到State。當然，這並不是出於任何實際目的 - 我只是在探索API設計。

所以我有這樣的事情：

data MutableEnv (s :: k) a ... 

newRef :: a -> MutableEnv s (Ref s a) 
readRef :: Ref s a -> MutableEnv s a 
writeRef :: Ref s a -> a -> MutableEnv s()

的MutableEnv定義並不重要。只是標準的免費/操作monad的東西與構造函數匹配在API中的三個功能。

但我被卡在什麼定義參考爲。就類型系統而言，我不想要某種類，我希望它是一個具體類型。

那麼晚了一個晚上，我出去散步，它打我 - 我基本上想要的是一個類型的構造函數索引的參數類型。但它必須是開放的，與GADT不同 - 新的口譯員可以隨意添加。然後它就撞到了我。這正是數據家族的特徵。一個開放的，類型索引的數據值家族。我可以通過以下操作完成api：

data family Ref (s :: k) :: * -> *

然後，處理Ref的基礎表示形式並沒有什麼大不了的。只要定義了一個解釋器MutableEnv，就可以創建一個數據實例（或者更可能是newtype實例）。

這個確切的例子並不是很有用。但它清楚地說明了數據族可以做的事情，即內射型家族無法做到的事情。

來源

2016-09-27 01:12:12 Carl

謝謝，這是一個非常有趣的例子（實際上我很想看看你最終有了這些想法）！也就是說，我仍然不確定我從技術角度看到爲什麼'Ref'不可能是每個實例的新數據類型或新類型的類型族（大概，儘管不一定）。 – Alec

在某種程度上，除了數據族指向的數據類型沒有其他名稱之外，數據族和常規類型之間沒有區別。這不像你可以對來自不同數據實例的構造函數或類似的GADT模式匹配。有時候，您只是想強制數據族名稱是該類型的唯一名稱。 – Carl

那麼這就是這個問題的關鍵 - 我不太確定數據族和類型族+數據/新類型聲明之間沒有其他區別。我懷疑這裏有更多的東西比滿足眼睛。 – Alec

answer by Reid Barton完全解釋了我的兩個例子之間的區別。它讓我想起了我在Richard Eisenberg的thesis中讀到的一些關於向Haskell添加依賴類型的內容，我認爲既然這個問題的核心是注入性和生成性，那麼值得一提的是DependentHaskell將如何處理這個問題（當它最終得到實現時，如果現在提出的量詞是最終實施的量詞）。

接下來是基於第56和57頁（4.3。4匹配性）上述thesis的：

定義（生成性）。如果f和g是生成，然後f a ~ g b意味着f ~ g

定義（注水井）。如果f是單射，則意味着f a ~ f ba ~ b

定義（匹配性）。函數f是可匹配當且僅當它是生成與內射

在Haskell，因爲我們現在知道它（8.0.1）的可匹配（類型級）的功能包括準確NEWTYPE，數據和數據家人類型的構造函數。在將來，根據DependentHaskell，我們將得到的新量詞之一將是'->，這將用於表示可匹配的函數。換句話說，有一種方法可以告訴編譯器一個類型級別的函數是生成的（目前只能通過確保該函數是一個類型構造函數來完成）。

來源

2016-09-27 04:38:22 Alec

數據族vs內注類族

回答

相關問題