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