GMapEitherタイプの家族の例は実際には対応していませんどちらの直感ですか？

Question

GHCユーザガイドは、Type家族に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の変換、我々が得る：

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

g'はです。TypeCheckするために取得するのは簡単ですが、二つの異なる実装といずれかを選択する方法があります

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 -> ???) 

実に不可能ですがあり、vが必要ですが、tにaとbの両方を指定すると、vしか作成できません。また、bが必要です。タプルの右のコンポーネントでも同じことが起こります。

ペアの関数(a,b) -> vと関数のペア間を行き来する明確な方法はありません。したがって、これら2つのものを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) 

妥当と思われますが、動作しません。

我々は (1,2)、ない (1,3)を挿入するので Nothingを与えているはずです

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

。私の実装では単なるバグだと言えるかもしれませんが、私はあなたに挑戦してください。

---

タイプの変換方法については、タイプと代数の間に美しい対応があります。ここで~~は「に類似した」を意味：

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