{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE TypeSynonymInstances   #-}
{-# LANGUAGE UndecidableInstances   #-}

--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Ops
-- Copyright   :  (c) 2011 Patrick Bahr
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module provides operators on higher-order functors. All definitions are
-- generalised versions of those in "Data.Comp.Ops".
--
--------------------------------------------------------------------------------

module Data.Comp.Multi.Ops 
    ( module Data.Comp.Multi.Ops
    , (O.:*:)(..)
    , O.ffst
    , O.fsnd
    ) where


import Control.Monad
import Data.Comp.Multi.HFoldable
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.HTraversable
import qualified Data.Comp.Ops as O

import Data.Comp.SubsumeCommon

infixr 6 :+:


-- |Data type defining coproducts.
data (f :+: g) (h :: * -> *) e = Inl (f h e)
                               | Inr (g h e)

{-| Utility function to case on a higher-order functor sum, without exposing the
  internal representation of sums. -}
caseH :: (f a b -> c) -> (g a b -> c) -> (f :+: g) a b -> c
caseH :: (f a b -> c) -> (g a b -> c) -> (:+:) f g a b -> c
caseH f a b -> c
f g a b -> c
g (:+:) f g a b
x = case (:+:) f g a b
x of
                Inl f a b
x -> f a b -> c
f f a b
x
                Inr g a b
x -> g a b -> c
g g a b
x

instance (HFunctor f, HFunctor g) => HFunctor (f :+: g) where
    hfmap :: (f :-> g) -> (:+:) f g f :-> (:+:) f g g
hfmap f :-> g
f (Inl f f i
v) = f g i -> (:+:) f g g i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
f h e -> (:+:) f g h e
Inl (f g i -> (:+:) f g g i) -> f g i -> (:+:) f g g i
forall a b. (a -> b) -> a -> b
$ (f :-> g) -> f f i -> f g i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap f :-> g
f f f i
v
    hfmap f :-> g
f (Inr g f i
v) = g g i -> (:+:) f g g i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
g h e -> (:+:) f g h e
Inr (g g i -> (:+:) f g g i) -> g g i -> (:+:) f g g i
forall a b. (a -> b) -> a -> b
$ (f :-> g) -> g f i -> g g i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap f :-> g
f g f i
v

instance (HFoldable f, HFoldable g) => HFoldable (f :+: g) where
    hfold :: (:+:) f g (K m) :=> m
hfold (Inl f (K m) i
e) = f (K m) i -> m
forall (h :: (* -> *) -> * -> *) m.
(HFoldable h, Monoid m) =>
h (K m) :=> m
hfold f (K m) i
e
    hfold (Inr g (K m) i
e) = g (K m) i -> m
forall (h :: (* -> *) -> * -> *) m.
(HFoldable h, Monoid m) =>
h (K m) :=> m
hfold g (K m) i
e
    hfoldMap :: (a :=> m) -> (:+:) f g a :=> m
hfoldMap a :=> m
f (Inl f a i
e) = (a :=> m) -> f a i -> m
forall (h :: (* -> *) -> * -> *) m (a :: * -> *).
(HFoldable h, Monoid m) =>
(a :=> m) -> h a :=> m
hfoldMap a :=> m
f f a i
e
    hfoldMap a :=> m
f (Inr g a i
e) = (a :=> m) -> g a i -> m
forall (h :: (* -> *) -> * -> *) m (a :: * -> *).
(HFoldable h, Monoid m) =>
(a :=> m) -> h a :=> m
hfoldMap a :=> m
f g a i
e
    hfoldr :: (a :=> (b -> b)) -> b -> (:+:) f g a :=> b
hfoldr a :=> (b -> b)
f b
b (Inl f a i
e) = (a :=> (b -> b)) -> b -> f a i -> b
forall (h :: (* -> *) -> * -> *) (a :: * -> *) b.
HFoldable h =>
(a :=> (b -> b)) -> b -> h a :=> b
hfoldr a :=> (b -> b)
f b
b f a i
e
    hfoldr a :=> (b -> b)
f b
b (Inr g a i
e) = (a :=> (b -> b)) -> b -> g a i -> b
forall (h :: (* -> *) -> * -> *) (a :: * -> *) b.
HFoldable h =>
(a :=> (b -> b)) -> b -> h a :=> b
hfoldr a :=> (b -> b)
f b
b g a i
e
    hfoldl :: (b -> a :=> b) -> b -> (:+:) f g a :=> b
hfoldl b -> a :=> b
f b
b (Inl f a i
e) = (b -> a :=> b) -> b -> f a i -> b
forall (h :: (* -> *) -> * -> *) b (a :: * -> *).
HFoldable h =>
(b -> a :=> b) -> b -> h a :=> b
hfoldl b -> a :=> b
f b
b f a i
e
    hfoldl b -> a :=> b
f b
b (Inr g a i
e) = (b -> a :=> b) -> b -> g a i -> b
forall (h :: (* -> *) -> * -> *) b (a :: * -> *).
HFoldable h =>
(b -> a :=> b) -> b -> h a :=> b
hfoldl b -> a :=> b
f b
b g a i
e

    hfoldr1 :: (a -> a -> a) -> (:+:) f g (K a) :=> a
hfoldr1 a -> a -> a
f (Inl f (K a) i
e) = (a -> a -> a) -> f (K a) i -> a
forall (h :: (* -> *) -> * -> *) a.
HFoldable h =>
(a -> a -> a) -> h (K a) :=> a
hfoldr1 a -> a -> a
f f (K a) i
e
    hfoldr1 a -> a -> a
f (Inr g (K a) i
e) = (a -> a -> a) -> g (K a) i -> a
forall (h :: (* -> *) -> * -> *) a.
HFoldable h =>
(a -> a -> a) -> h (K a) :=> a
hfoldr1 a -> a -> a
f g (K a) i
e
    hfoldl1 :: (a -> a -> a) -> (:+:) f g (K a) :=> a
hfoldl1 a -> a -> a
f (Inl f (K a) i
e) = (a -> a -> a) -> f (K a) i -> a
forall (h :: (* -> *) -> * -> *) a.
HFoldable h =>
(a -> a -> a) -> h (K a) :=> a
hfoldl1 a -> a -> a
f f (K a) i
e
    hfoldl1 a -> a -> a
f (Inr g (K a) i
e) = (a -> a -> a) -> g (K a) i -> a
forall (h :: (* -> *) -> * -> *) a.
HFoldable h =>
(a -> a -> a) -> h (K a) :=> a
hfoldl1 a -> a -> a
f g (K a) i
e

instance (HTraversable f, HTraversable g) => HTraversable (f :+: g) where
    htraverse :: NatM f a b -> NatM f ((:+:) f g a) ((:+:) f g b)
htraverse NatM f a b
f (Inl f a i
e) = f b i -> (:+:) f g b i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
f h e -> (:+:) f g h e
Inl (f b i -> (:+:) f g b i) -> f (f b i) -> f ((:+:) f g b i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NatM f a b -> f a i -> f (f b i)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Applicative f) =>
NatM f a b -> NatM f (t a) (t b)
htraverse NatM f a b
f f a i
e
    htraverse NatM f a b
f (Inr g a i
e) = g b i -> (:+:) f g b i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
g h e -> (:+:) f g h e
Inr (g b i -> (:+:) f g b i) -> f (g b i) -> f ((:+:) f g b i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NatM f a b -> g a i -> f (g b i)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Applicative f) =>
NatM f a b -> NatM f (t a) (t b)
htraverse NatM f a b
f g a i
e
    hmapM :: NatM m a b -> NatM m ((:+:) f g a) ((:+:) f g b)
hmapM NatM m a b
f (Inl f a i
e) = f b i -> (:+:) f g b i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
f h e -> (:+:) f g h e
Inl (f b i -> (:+:) f g b i) -> m (f b i) -> m ((:+:) f g b i)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` NatM m a b -> f a i -> m (f b i)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m a b
f f a i
e
    hmapM NatM m a b
f (Inr g a i
e) = g b i -> (:+:) f g b i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
g h e -> (:+:) f g h e
Inr (g b i -> (:+:) f g b i) -> m (g b i) -> m ((:+:) f g b i)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` NatM m a b -> g a i -> m (g b i)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m a b
f g a i
e

-- The subsumption relation.

infixl 5 :<:
infixl 5 :=:

type family Elem (f :: (* -> *) -> * -> *)
                 (g :: (* -> *) -> * -> *) :: Emb where
    Elem f f = Found Here
    Elem (f1 :+: f2) g =  Sum' (Elem f1 g) (Elem f2 g)
    Elem f (g1 :+: g2) = Choose (Elem f g1) (Elem f g2)
    Elem f g = NotFound

class Subsume (e :: Emb) (f :: (* -> *) -> * -> *)
                         (g :: (* -> *) -> * -> *) where
  inj'  :: Proxy e -> f a :-> g a
  prj'  :: Proxy e -> NatM Maybe (g a) (f a)

instance Subsume (Found Here) f f where
    inj' :: Proxy ('Found 'Here) -> f a :-> f a
inj' Proxy ('Found 'Here)
_ = f a i -> f a i
forall a. a -> a
id

    prj' :: Proxy ('Found 'Here) -> NatM Maybe (f a) (f a)
prj' Proxy ('Found 'Here)
_ = f a i -> Maybe (f a i)
forall a. a -> Maybe a
Just

instance Subsume (Found p) f g => Subsume (Found (Le p)) f (g :+: g') where
    inj' :: Proxy ('Found ('Le p)) -> f a :-> (:+:) g g' a
inj' Proxy ('Found ('Le p))
_ = g a i -> (:+:) g g' a i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
f h e -> (:+:) f g h e
Inl (g a i -> (:+:) g g' a i)
-> (f a i -> g a i) -> f a i -> (:+:) g g' a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy ('Found p) -> f a :-> g a
forall (e :: Emb) (f :: (* -> *) -> * -> *)
       (g :: (* -> *) -> * -> *) (a :: * -> *).
Subsume e f g =>
Proxy e -> f a :-> g a
inj' (Proxy ('Found p)
forall k (a :: k). Proxy a
P :: Proxy (Found p))

    prj' :: Proxy ('Found ('Le p)) -> NatM Maybe ((:+:) g g' a) (f a)
prj' Proxy ('Found ('Le p))
_ (Inl g a i
x) = Proxy ('Found p) -> g a i -> Maybe (f a i)
forall (e :: Emb) (f :: (* -> *) -> * -> *)
       (g :: (* -> *) -> * -> *) (a :: * -> *).
Subsume e f g =>
Proxy e -> NatM Maybe (g a) (f a)
prj' (Proxy ('Found p)
forall k (a :: k). Proxy a
P :: Proxy (Found p)) g a i
x
    prj' Proxy ('Found ('Le p))
_ (:+:) g g' a i
_       = Maybe (f a i)
forall a. Maybe a
Nothing

instance Subsume (Found p) f g => Subsume (Found (Ri p)) f (g' :+: g) where
    inj' :: Proxy ('Found ('Ri p)) -> f a :-> (:+:) g' g a
inj' Proxy ('Found ('Ri p))
_ = g a i -> (:+:) g' g a i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
g h e -> (:+:) f g h e
Inr (g a i -> (:+:) g' g a i)
-> (f a i -> g a i) -> f a i -> (:+:) g' g a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy ('Found p) -> f a :-> g a
forall (e :: Emb) (f :: (* -> *) -> * -> *)
       (g :: (* -> *) -> * -> *) (a :: * -> *).
Subsume e f g =>
Proxy e -> f a :-> g a
inj' (Proxy ('Found p)
forall k (a :: k). Proxy a
P :: Proxy (Found p))

    prj' :: Proxy ('Found ('Ri p)) -> NatM Maybe ((:+:) g' g a) (f a)
prj' Proxy ('Found ('Ri p))
_ (Inr g a i
x) = Proxy ('Found p) -> g a i -> Maybe (f a i)
forall (e :: Emb) (f :: (* -> *) -> * -> *)
       (g :: (* -> *) -> * -> *) (a :: * -> *).
Subsume e f g =>
Proxy e -> NatM Maybe (g a) (f a)
prj' (Proxy ('Found p)
forall k (a :: k). Proxy a
P :: Proxy (Found p)) g a i
x
    prj' Proxy ('Found ('Ri p))
_ (:+:) g' g a i
_       = Maybe (f a i)
forall a. Maybe a
Nothing

instance (Subsume (Found p1) f1 g, Subsume (Found p2) f2 g)
    => Subsume (Found (Sum p1 p2)) (f1 :+: f2) g where
    inj' :: Proxy ('Found ('Sum p1 p2)) -> (:+:) f1 f2 a :-> g a
inj' Proxy ('Found ('Sum p1 p2))
_ (Inl f1 a i
x) = Proxy ('Found p1) -> f1 a i -> g a i
forall (e :: Emb) (f :: (* -> *) -> * -> *)
       (g :: (* -> *) -> * -> *) (a :: * -> *).
Subsume e f g =>
Proxy e -> f a :-> g a
inj' (Proxy ('Found p1)
forall k (a :: k). Proxy a
P :: Proxy (Found p1)) f1 a i
x
    inj' Proxy ('Found ('Sum p1 p2))
_ (Inr f2 a i
x) = Proxy ('Found p2) -> f2 a i -> g a i
forall (e :: Emb) (f :: (* -> *) -> * -> *)
       (g :: (* -> *) -> * -> *) (a :: * -> *).
Subsume e f g =>
Proxy e -> f a :-> g a
inj' (Proxy ('Found p2)
forall k (a :: k). Proxy a
P :: Proxy (Found p2)) f2 a i
x

    prj' :: Proxy ('Found ('Sum p1 p2)) -> NatM Maybe (g a) ((:+:) f1 f2 a)
prj' Proxy ('Found ('Sum p1 p2))
_ g a i
x = case Proxy ('Found p1) -> g a i -> Maybe (f1 a i)
forall (e :: Emb) (f :: (* -> *) -> * -> *)
       (g :: (* -> *) -> * -> *) (a :: * -> *).
Subsume e f g =>
Proxy e -> NatM Maybe (g a) (f a)
prj' (Proxy ('Found p1)
forall k (a :: k). Proxy a
P :: Proxy (Found p1)) g a i
x of
                 Just f1 a i
y -> (:+:) f1 f2 a i -> Maybe ((:+:) f1 f2 a i)
forall a. a -> Maybe a
Just (f1 a i -> (:+:) f1 f2 a i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
f h e -> (:+:) f g h e
Inl f1 a i
y)
                 Maybe (f1 a i)
_      -> case Proxy ('Found p2) -> g a i -> Maybe (f2 a i)
forall (e :: Emb) (f :: (* -> *) -> * -> *)
       (g :: (* -> *) -> * -> *) (a :: * -> *).
Subsume e f g =>
Proxy e -> NatM Maybe (g a) (f a)
prj' (Proxy ('Found p2)
forall k (a :: k). Proxy a
P :: Proxy (Found p2)) g a i
x of
                             Just f2 a i
y -> (:+:) f1 f2 a i -> Maybe ((:+:) f1 f2 a i)
forall a. a -> Maybe a
Just (f2 a i -> (:+:) f1 f2 a i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
g h e -> (:+:) f g h e
Inr f2 a i
y)
                             Maybe (f2 a i)
_      -> Maybe ((:+:) f1 f2 a i)
forall a. Maybe a
Nothing



-- | A constraint @f :<: g@ expresses that the signature @f@ is
-- subsumed by @g@, i.e. @f@ can be used to construct elements in @g@.
type f :<: g = (Subsume (ComprEmb (Elem f g)) f g)


inj :: forall f g a . (f :<: g) => f a :-> g a
inj :: f a :-> g a
inj = Proxy (ComprEmb (Elem f g)) -> f a :-> g a
forall (e :: Emb) (f :: (* -> *) -> * -> *)
       (g :: (* -> *) -> * -> *) (a :: * -> *).
Subsume e f g =>
Proxy e -> f a :-> g a
inj' (Proxy (ComprEmb (Elem f g))
forall k (a :: k). Proxy a
P :: Proxy (ComprEmb (Elem f g)))

proj :: forall f g a . (f :<: g) => NatM Maybe (g a) (f a)
proj :: NatM Maybe (g a) (f a)
proj = Proxy (ComprEmb (Elem f g)) -> NatM Maybe (g a) (f a)
forall (e :: Emb) (f :: (* -> *) -> * -> *)
       (g :: (* -> *) -> * -> *) (a :: * -> *).
Subsume e f g =>
Proxy e -> NatM Maybe (g a) (f a)
prj' (Proxy (ComprEmb (Elem f g))
forall k (a :: k). Proxy a
P :: Proxy (ComprEmb (Elem f g)))

type f :=: g = (f :<: g, g :<: f)



spl :: (f :=: f1 :+: f2) => (f1 a :-> b) -> (f2 a :-> b) -> f a :-> b
spl :: (f1 a :-> b) -> (f2 a :-> b) -> f a :-> b
spl f1 a :-> b
f1 f2 a :-> b
f2 f a i
x = case f a i -> (:+:) f1 f2 a i
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
f a :-> g a
inj f a i
x of
            Inl f1 a i
y -> f1 a i -> b i
f1 a :-> b
f1 f1 a i
y
            Inr f2 a i
y -> f2 a i -> b i
f2 a :-> b
f2 f2 a i
y

-- Constant Products

infixr 7 :&:

-- | This data type adds a constant product to a
-- signature. Alternatively, this could have also been defined as
--
-- @
-- data (f :&: a) (g ::  * -> *) e = f g e :&: a e
-- @
--
-- This is too general, however, for example for 'productHHom'.

data (f :&: a) (g ::  * -> *) e = f g e :&: a


instance (HFunctor f) => HFunctor (f :&: a) where
    hfmap :: (f :-> g) -> (:&:) f a f :-> (:&:) f a g
hfmap f :-> g
f (f f i
v :&: a
c) = (f :-> g) -> f f i -> f g i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap f :-> g
f f f i
v f g i -> a -> (:&:) f a g i
forall k (f :: (* -> *) -> k -> *) a (g :: * -> *) (e :: k).
f g e -> a -> (:&:) f a g e
:&: a
c

instance (HFoldable f) => HFoldable (f :&: a) where
    hfold :: (:&:) f a (K m) :=> m
hfold (f (K m) i
v :&: a
_) = f (K m) i -> m
forall (h :: (* -> *) -> * -> *) m.
(HFoldable h, Monoid m) =>
h (K m) :=> m
hfold f (K m) i
v
    hfoldMap :: (a :=> m) -> (:&:) f a a :=> m
hfoldMap a :=> m
f (f a i
v :&: a
_) = (a :=> m) -> f a i -> m
forall (h :: (* -> *) -> * -> *) m (a :: * -> *).
(HFoldable h, Monoid m) =>
(a :=> m) -> h a :=> m
hfoldMap a :=> m
f f a i
v
    hfoldr :: (a :=> (b -> b)) -> b -> (:&:) f a a :=> b
hfoldr a :=> (b -> b)
f b
e (f a i
v :&: a
_) = (a :=> (b -> b)) -> b -> f a i -> b
forall (h :: (* -> *) -> * -> *) (a :: * -> *) b.
HFoldable h =>
(a :=> (b -> b)) -> b -> h a :=> b
hfoldr a :=> (b -> b)
f b
e f a i
v
    hfoldl :: (b -> a :=> b) -> b -> (:&:) f a a :=> b
hfoldl b -> a :=> b
f b
e (f a i
v :&: a
_) = (b -> a :=> b) -> b -> f a i -> b
forall (h :: (* -> *) -> * -> *) b (a :: * -> *).
HFoldable h =>
(b -> a :=> b) -> b -> h a :=> b
hfoldl b -> a :=> b
f b
e f a i
v
    hfoldr1 :: (a -> a -> a) -> (:&:) f a (K a) :=> a
hfoldr1 a -> a -> a
f (f (K a) i
v :&: a
_) = (a -> a -> a) -> f (K a) i -> a
forall (h :: (* -> *) -> * -> *) a.
HFoldable h =>
(a -> a -> a) -> h (K a) :=> a
hfoldr1 a -> a -> a
f f (K a) i
v
    hfoldl1 :: (a -> a -> a) -> (:&:) f a (K a) :=> a
hfoldl1 a -> a -> a
f (f (K a) i
v :&: a
_) = (a -> a -> a) -> f (K a) i -> a
forall (h :: (* -> *) -> * -> *) a.
HFoldable h =>
(a -> a -> a) -> h (K a) :=> a
hfoldl1 a -> a -> a
f f (K a) i
v


instance (HTraversable f) => HTraversable (f :&: a) where
    htraverse :: NatM f a b -> NatM f ((:&:) f a a) ((:&:) f a b)
htraverse NatM f a b
f (f a i
v :&: a
c) =  (f b i -> a -> (:&:) f a b i
forall k (f :: (* -> *) -> k -> *) a (g :: * -> *) (e :: k).
f g e -> a -> (:&:) f a g e
:&: a
c) (f b i -> (:&:) f a b i) -> f (f b i) -> f ((:&:) f a b i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NatM f a b -> f a i -> f (f b i)
forall (t :: (* -> *) -> * -> *) (f :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Applicative f) =>
NatM f a b -> NatM f (t a) (t b)
htraverse NatM f a b
f f a i
v)
    hmapM :: NatM m a b -> NatM m ((:&:) f a a) ((:&:) f a b)
hmapM NatM m a b
f (f a i
v :&: a
c) = (f b i -> (:&:) f a b i) -> m (f b i) -> m ((:&:) f a b i)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (f b i -> a -> (:&:) f a b i
forall k (f :: (* -> *) -> k -> *) a (g :: * -> *) (e :: k).
f g e -> a -> (:&:) f a g e
:&: a
c) (NatM m a b -> f a i -> m (f b i)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *)
       (b :: * -> *).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM NatM m a b
f f a i
v)

-- | This class defines how to distribute an annotation over a sum of
-- signatures.
class DistAnn (s :: (* -> *) -> * -> *) p s' | s' -> s, s' -> p where
    -- | This function injects an annotation over a signature.
    injectA :: p -> s a :-> s' a
    projectA :: s' a :-> (s a O.:&: p)


class RemA (s :: (* -> *) -> * -> *) s' | s -> s'  where
    remA :: s a :-> s' a


instance (RemA s s') => RemA (f :&: p :+: s) (f :+: s') where
    remA :: (:+:) (f :&: p) s a i -> (:+:) f s' a i
remA (Inl (f a i
v :&: p
_)) = f a i -> (:+:) f s' a i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
f h e -> (:+:) f g h e
Inl f a i
v
    remA (Inr s a i
v) = s' a i -> (:+:) f s' a i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
g h e -> (:+:) f g h e
Inr (s' a i -> (:+:) f s' a i) -> s' a i -> (:+:) f s' a i
forall a b. (a -> b) -> a -> b
$ s a i -> s' a i
forall (s :: (* -> *) -> * -> *) (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
RemA s s' =>
s a :-> s' a
remA s a i
v


instance RemA (f :&: p) f where
    remA :: (:&:) f p a i -> f a i
remA (f a i
v :&: p
_) = f a i
v


instance DistAnn f p (f :&: p) where

    injectA :: p -> f a :-> (:&:) f p a
injectA p
p f a i
v = f a i
v f a i -> p -> (:&:) f p a i
forall k (f :: (* -> *) -> k -> *) a (g :: * -> *) (e :: k).
f g e -> a -> (:&:) f a g e
:&: p
p

    projectA :: (:&:) f p a i -> (:&:) (f a) p i
projectA (f a i
v :&: p
p) = f a i
v f a i -> p -> (:&:) (f a) p i
forall k (f :: k -> *) a (e :: k). f e -> a -> (:&:) f a e
O.:&: p
p


instance (DistAnn s p s') => DistAnn (f :+: s) p ((f :&: p) :+: s') where
    injectA :: p -> (:+:) f s a :-> (:+:) (f :&: p) s' a
injectA p
p (Inl f a i
v) = (:&:) f p a i -> (:+:) (f :&: p) s' a i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
f h e -> (:+:) f g h e
Inl (f a i
v f a i -> p -> (:&:) f p a i
forall k (f :: (* -> *) -> k -> *) a (g :: * -> *) (e :: k).
f g e -> a -> (:&:) f a g e
:&: p
p)
    injectA p
p (Inr s a i
v) = s' a i -> (:+:) (f :&: p) s' a i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
g h e -> (:+:) f g h e
Inr (s' a i -> (:+:) (f :&: p) s' a i)
-> s' a i -> (:+:) (f :&: p) s' a i
forall a b. (a -> b) -> a -> b
$ p -> s a i -> s' a i
forall (s :: (* -> *) -> * -> *) p (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
DistAnn s p s' =>
p -> s a :-> s' a
injectA p
p s a i
v

    projectA :: (:+:) (f :&: p) s' a i -> (:&:) ((:+:) f s a) p i
projectA (Inl (f a i
v :&: p
p)) = (f a i -> (:+:) f s a i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
f h e -> (:+:) f g h e
Inl f a i
v (:+:) f s a i -> p -> (:&:) ((:+:) f s a) p i
forall k (f :: k -> *) a (e :: k). f e -> a -> (:&:) f a e
O.:&: p
p)
    projectA (Inr s' a i
v) = let (s a i
v' O.:&: p
p) = s' a i -> (:&:) (s a) p i
forall (s :: (* -> *) -> * -> *) p (s' :: (* -> *) -> * -> *)
       (a :: * -> *).
DistAnn s p s' =>
s' a :-> (s a :&: p)
projectA s' a i
v
                        in  (s a i -> (:+:) f s a i
forall k (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
g h e -> (:+:) f g h e
Inr s a i
v' (:+:) f s a i -> p -> (:&:) ((:+:) f s a) p i
forall k (f :: k -> *) a (e :: k). f e -> a -> (:&:) f a e
O.:&: p
p)