GMapEither類型家庭的例子不是真的對應嗎？

Question

GHC用戶指南顯示了Data instance declarations節上型家庭這個例子：

data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v) 

我使用的Either類型用於每當我們要向左或向右價值，所以我希望GMapEither以某種方式提供任何向左或向右變體，但它似乎總是同時擁有：

{-# LANGUAGE TypeFamilies #-} 

module Main where 

import qualified Data.HashMap.Strict as H 

data family GMap k :: * -> * 

data instance GMap Int Int = GMapIntInt (H.HashMap Int Int) 
          deriving (Show, Eq) 

data instance GMap String Int = GMapStringInt (H.HashMap String 
                Int) 
           deriving (Show, Eq) 

data instance GMap (Either a b) v = GMapEither (GMap a v) 
               (GMap b v) 

main :: IO() 
main = do 
    let m = GMapIntInt H.empty 
    print m 
    let m2 = GMapStringInt H.empty 
    print m2 
    let m3 = GMapEither m m2 
    let (GMapEither m3l m3r) = m3 
    print m3l 
    print m3r 

我才明白這個正確的，這將是更適合在這裏使用一個元組，例如像這樣：

data instance GMap (a, b) v = GMapTuple (GMap a v) (GMap b v) 

我認爲這可能會給出更好的直覺。

Answer 1

當我們抽象時，它通常有所謂的「語義域」，這是抽象應該表示的東西。抽象的屬性應該匹配語義域的屬性。 （當抽象具有類型類時，這被稱爲type class morphism）。

GMap顯然試圖代表某種映射操作。映射的原型示例是一個函數。也有像Data.Map這樣的有限地圖，但它也假裝成一種特殊的功能。

因此，無論如何，我們應該預計GMap a b具有類似的功能a -> b。如果GMap (a,b) v被定義爲等於(GMap a v, GMap b v)，那麼我們應該期望在語義域中存在相應的同構。因此，只要將所有的GMap s轉換功能箭頭->，我們得到：

f' :: ((a,b) -> v) -> (a -> v, b -> v) 
g' :: (a -> v, b -> v) -> ((a,b) -> v) 

g'是很容易去進行類型檢查，但有兩個不同的實現，並沒有辦法選擇一個：

g' :: (a -> v, b -> v) -> ((a,b) -> v) 
g' = (tl, tr) (x,y) = tl x 
-- and 
g' = (tl, tr) (x,y) = tr y 

和f'是完全不可能的

f' :: ((a,b) -> v) -> (a -> v, b -> v) 
f' t = (\a -> ??? , \b -> ???) 

在左側???，我們有一個a，我們需要v，但我們只能構建v，如果我們給t這兩個a和b，我們沒有任何地方可以得到我們需要的b。同樣的事情發生在元組的正確組件中。

在(a,b) -> v對和一對函數之間來回移動之間沒有明確的方法。所以要聲明這兩件事情相同，因爲GMap看起來不正確。同樣的事情發生在像Data.Map這樣的有限地圖上（你可以得到某種類型的信息，但它不會最終成爲一個真正的同構因子，因爲f' . g' /= id（反之亦然，我不記得是哪個））。

儘管同構從(Either a b -> v) -> (a -> v, b -> v)很容易寫

f :: (Either a b -> v) -> (a -> v, b -> v) 
f t = (t . Left, t . Right) 

g :: (a -> v, b -> v) -> (Either a b -> v) 
g (l, r) (Left x) = l x 
g (l, r) (Right y) = r y 

---

這種語義領域的東西可以爲樸實的程序員有點抽象。爲什麼我們能寫這個同構還是不重要？但是當您嘗試使GMap做任何事情時，您會發現問題很快就會以實際的方式出現。

讓我們開始捆綁數據家庭一對夫婦非常簡單的操作中，我們應該能夠編寫：

class MapKey k where 
    data family GMap k :: * -> * 

    empty :: GMap k v 
    lookup :: GMap k v -> k -> Maybe v 
    insert :: k -> v -> GMap k v -> GMap k v 

和一個非常簡單的基本情況。如果我們試圖用

instance MapKey Int where 
    data GMap Int v = GMapInt (Int -> Maybe v) 
    empty = GMapInt (const Nothing) 
    lookup (GMapInt f) x = f x 
    insert x v (GMapInt f) = GMapInt (\y -> if x == y then Just v else f y) 

工作

instance (MapKey a, MapKey b) => MapKey (a,b) where 
    data GMap (a,b) v = GMapTuple (GMap a v) (GMap b v) 
    empty = GMapTuple empty empty 
    lookup (GMapTuple l r) (x,y) = 
     -- several implementations here, but maybe we could do 
     lookup l x `mplus` lookup r y 

    insert (x,y) v (GMapTuple l r) = GMapTuple (insert x v l) (insert y v r) 

看起來合理但它不起作用

>>> lookup (insert (1 :: Int, 2 :: Int) "value" empty) (1,3) 
Just "value" 

應該給Nothing因爲我們插入(1,2)，不(1,3)。你可以說這只是我實現中的一個錯誤，但我敢於寫一個工作。

---

類型和代數之間有一個美麗的對應關係，它將指導你如何轉換類型。這裏~~的意思是「類似於」：

Either a b ~~ a + b 
(a,b)  ~~ a * b 
a -> b  ~~ b^a 

所以

Map ((a,b) -> v) ~~ v^(a*b) 
        = (v^a)^b 
        ~~ Map b (Map a v) 

也就是說，我們應該期待的元組和嵌套地圖地圖之間的同構。同理：

Map (Either a b -> v) ~~ v^(a+b) 
         = v^a * v^b 
         ~~ (Map v a, Map v b) 

而且應該從副產品（Either）和對地圖的地圖之間的一個很好的同構。

這個過程非常有趣，值得一提的是與其他東西是同構的。

延伸閱讀：

• 克里斯·泰勒，The Algebra of Algebraic Data Types
• 丹Piponi，Memoizing Polymorphic Functions with High School Algebra and Quantifiers
• Conal埃利奧特，Denotational Design with Type Class Morphisms