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

--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Ops
-- Copyright   :  (c) 2010-2011 Patrick Bahr, Tom Hvitved
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module provides operators on functors.
--
--------------------------------------------------------------------------------

module Data.Comp.Ops where

import Data.Foldable
import Data.Traversable

import Control.Applicative
import Control.Monad hiding (mapM, sequence)
import Data.Comp.SubsumeCommon


import Prelude hiding (foldl, foldl1, foldr, foldr1, mapM, sequence)


-- Sums

infixr 6 :+:


-- |Formal sum of signatures (functors).
data (f :+: g) e = Inl (f e)
                 | Inr (g e)

fromInl :: (f :+: g) e -> Maybe (f e)
fromInl :: (:+:) f g e -> Maybe (f e)
fromInl = (f e -> Maybe (f e))
-> (g e -> Maybe (f e)) -> (:+:) f g e -> Maybe (f e)
forall k (f :: k -> *) (a :: k) b (g :: k -> *).
(f a -> b) -> (g a -> b) -> (:+:) f g a -> b
caseF f e -> Maybe (f e)
forall a. a -> Maybe a
Just (Maybe (f e) -> g e -> Maybe (f e)
forall a b. a -> b -> a
const Maybe (f e)
forall a. Maybe a
Nothing)

fromInr :: (f :+: g) e -> Maybe (g e)
fromInr :: (:+:) f g e -> Maybe (g e)
fromInr = (f e -> Maybe (g e))
-> (g e -> Maybe (g e)) -> (:+:) f g e -> Maybe (g e)
forall k (f :: k -> *) (a :: k) b (g :: k -> *).
(f a -> b) -> (g a -> b) -> (:+:) f g a -> b
caseF (Maybe (g e) -> f e -> Maybe (g e)
forall a b. a -> b -> a
const Maybe (g e)
forall a. Maybe a
Nothing) g e -> Maybe (g e)
forall a. a -> Maybe a
Just

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

instance (Functor f, Functor g) => Functor (f :+: g) where
    fmap :: (a -> b) -> (:+:) f g a -> (:+:) f g b
fmap a -> b
f (Inl f a
e) = f b -> (:+:) f g b
forall k (f :: k -> *) (g :: k -> *) (e :: k). f e -> (:+:) f g e
Inl ((a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f f a
e)
    fmap a -> b
f (Inr g a
e) = g b -> (:+:) f g b
forall k (f :: k -> *) (g :: k -> *) (e :: k). g e -> (:+:) f g e
Inr ((a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f g a
e)

instance (Foldable f, Foldable g) => Foldable (f :+: g) where
    fold :: (:+:) f g m -> m
fold (Inl f m
e) = f m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold f m
e
    fold (Inr g m
e) = g m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold g m
e
    foldMap :: (a -> m) -> (:+:) f g a -> m
foldMap a -> m
f (Inl f a
e) = (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f f a
e
    foldMap a -> m
f (Inr g a
e) = (a -> m) -> g a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f g a
e
    foldr :: (a -> b -> b) -> b -> (:+:) f g a -> b
foldr a -> b -> b
f b
b (Inl f a
e) = (a -> b -> b) -> b -> f a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f b
b f a
e
    foldr a -> b -> b
f b
b (Inr g a
e) = (a -> b -> b) -> b -> g a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f b
b g a
e
    foldl :: (b -> a -> b) -> b -> (:+:) f g a -> b
foldl b -> a -> b
f b
b (Inl f a
e) = (b -> a -> b) -> b -> f a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> a -> b
f b
b f a
e
    foldl b -> a -> b
f b
b (Inr g a
e) = (b -> a -> b) -> b -> g a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> a -> b
f b
b g a
e
    foldr1 :: (a -> a -> a) -> (:+:) f g a -> a
foldr1 a -> a -> a
f (Inl f a
e) = (a -> a -> a) -> f a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 a -> a -> a
f f a
e
    foldr1 a -> a -> a
f (Inr g a
e) = (a -> a -> a) -> g a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 a -> a -> a
f g a
e
    foldl1 :: (a -> a -> a) -> (:+:) f g a -> a
foldl1 a -> a -> a
f (Inl f a
e) = (a -> a -> a) -> f a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 a -> a -> a
f f a
e
    foldl1 a -> a -> a
f (Inr g a
e) = (a -> a -> a) -> g a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 a -> a -> a
f g a
e

instance (Traversable f, Traversable g) => Traversable (f :+: g) where
    traverse :: (a -> f b) -> (:+:) f g a -> f ((:+:) f g b)
traverse a -> f b
f (Inl f a
e) = f b -> (:+:) f g b
forall k (f :: k -> *) (g :: k -> *) (e :: k). f e -> (:+:) f g e
Inl (f b -> (:+:) f g b) -> f (f b) -> f ((:+:) f g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> f a -> f (f b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f f a
e
    traverse a -> f b
f (Inr g a
e) = g b -> (:+:) f g b
forall k (f :: k -> *) (g :: k -> *) (e :: k). g e -> (:+:) f g e
Inr (g b -> (:+:) f g b) -> f (g b) -> f ((:+:) f g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> g a -> f (g b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f g a
e
    sequenceA :: (:+:) f g (f a) -> f ((:+:) f g a)
sequenceA (Inl f (f a)
e) = f a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (e :: k). f e -> (:+:) f g e
Inl (f a -> (:+:) f g a) -> f (f a) -> f ((:+:) f g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (f a) -> f (f a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA f (f a)
e
    sequenceA (Inr g (f a)
e) = g a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (e :: k). g e -> (:+:) f g e
Inr (g a -> (:+:) f g a) -> f (g a) -> f ((:+:) f g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g (f a) -> f (g a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA g (f a)
e
    mapM :: (a -> m b) -> (:+:) f g a -> m ((:+:) f g b)
mapM a -> m b
f (Inl f a
e) = f b -> (:+:) f g b
forall k (f :: k -> *) (g :: k -> *) (e :: k). f e -> (:+:) f g e
Inl (f b -> (:+:) f g b) -> m (f b) -> m ((:+:) f g b)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` (a -> m b) -> f a -> m (f b)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m b
f f a
e
    mapM a -> m b
f (Inr g a
e) = g b -> (:+:) f g b
forall k (f :: k -> *) (g :: k -> *) (e :: k). g e -> (:+:) f g e
Inr (g b -> (:+:) f g b) -> m (g b) -> m ((:+:) f g b)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` (a -> m b) -> g a -> m (g b)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m b
f g a
e
    sequence :: (:+:) f g (m a) -> m ((:+:) f g a)
sequence (Inl f (m a)
e) = f a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (e :: k). f e -> (:+:) f g e
Inl (f a -> (:+:) f g a) -> m (f a) -> m ((:+:) f g a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` f (m a) -> m (f a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence f (m a)
e
    sequence (Inr g (m a)
e) = g a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (e :: k). g e -> (:+:) f g e
Inr (g a -> (:+:) f g a) -> m (g a) -> m ((:+:) f g a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` g (m a) -> m (g a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence g (m a)
e

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 -> g a -> Maybe (f a)

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

    prj' :: Proxy ('Found 'Here) -> f a -> Maybe (f a)
prj' Proxy ('Found 'Here)
_ = f a -> Maybe (f a)
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 -> (:+:) g g' a
forall k (f :: k -> *) (g :: k -> *) (e :: k). f e -> (:+:) f g e
Inl (g a -> (:+:) g g' a) -> (f a -> g a) -> f a -> (:+:) g g' a
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)) -> (:+:) g g' a -> Maybe (f a)
prj' Proxy ('Found ('Le p))
_ (Inl g a
x) = Proxy ('Found p) -> g a -> Maybe (f a)
forall (e :: Emb) (f :: * -> *) (g :: * -> *) a.
Subsume e f g =>
Proxy e -> g a -> Maybe (f a)
prj' (Proxy ('Found p)
forall k (a :: k). Proxy a
P :: Proxy (Found p)) g a
x
    prj' Proxy ('Found ('Le p))
_ (:+:) g g' a
_       = Maybe (f a)
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 -> (:+:) g' g a
forall k (f :: k -> *) (g :: k -> *) (e :: k). g e -> (:+:) f g e
Inr (g a -> (:+:) g' g a) -> (f a -> g a) -> f a -> (:+:) g' g a
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)) -> (:+:) g' g a -> Maybe (f a)
prj' Proxy ('Found ('Ri p))
_ (Inr g a
x) = Proxy ('Found p) -> g a -> Maybe (f a)
forall (e :: Emb) (f :: * -> *) (g :: * -> *) a.
Subsume e f g =>
Proxy e -> g a -> Maybe (f a)
prj' (Proxy ('Found p)
forall k (a :: k). Proxy a
P :: Proxy (Found p)) g a
x
    prj' Proxy ('Found ('Ri p))
_ (:+:) g' g a
_       = Maybe (f a)
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
x) = Proxy ('Found p1) -> f1 a -> g a
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
x
    inj' Proxy ('Found ('Sum p1 p2))
_ (Inr f2 a
x) = Proxy ('Found p2) -> f2 a -> g a
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
x

    prj' :: Proxy ('Found ('Sum p1 p2)) -> g a -> Maybe ((:+:) f1 f2 a)
prj' Proxy ('Found ('Sum p1 p2))
_ g a
x = case Proxy ('Found p1) -> g a -> Maybe (f1 a)
forall (e :: Emb) (f :: * -> *) (g :: * -> *) a.
Subsume e f g =>
Proxy e -> g a -> Maybe (f a)
prj' (Proxy ('Found p1)
forall k (a :: k). Proxy a
P :: Proxy (Found p1)) g a
x of
                 Just f1 a
y -> (:+:) f1 f2 a -> Maybe ((:+:) f1 f2 a)
forall a. a -> Maybe a
Just (f1 a -> (:+:) f1 f2 a
forall k (f :: k -> *) (g :: k -> *) (e :: k). f e -> (:+:) f g e
Inl f1 a
y)
                 Maybe (f1 a)
_      -> case Proxy ('Found p2) -> g a -> Maybe (f2 a)
forall (e :: Emb) (f :: * -> *) (g :: * -> *) a.
Subsume e f g =>
Proxy e -> g a -> Maybe (f a)
prj' (Proxy ('Found p2)
forall k (a :: k). Proxy a
P :: Proxy (Found p2)) g a
x of
                             Just f2 a
y -> (:+:) f1 f2 a -> Maybe ((:+:) f1 f2 a)
forall a. a -> Maybe a
Just (f2 a -> (:+:) f1 f2 a
forall k (f :: k -> *) (g :: k -> *) (e :: k). g e -> (:+:) f g e
Inr f2 a
y)
                             Maybe (f2 a)
_      -> Maybe ((:+:) f1 f2 a)
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) => g a -> Maybe (f a)
proj :: g a -> Maybe (f a)
proj = Proxy (ComprEmb (Elem f g)) -> g a -> Maybe (f a)
forall (e :: Emb) (f :: * -> *) (g :: * -> *) a.
Subsume e f g =>
Proxy e -> g a -> Maybe (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
x = case f a -> (:+:) f1 f2 a
forall (f :: * -> *) (g :: * -> *) a. (f :<: g) => f a -> g a
inj f a
x of
            Inl f1 a
y -> f1 a -> b
f1 f1 a
y
            Inr f2 a
y -> f2 a -> b
f2 f2 a
y



-- Products

infixr 8 :*:

-- |Formal product of signatures (functors).
data (f :*: g) a = f a :*: g a


ffst :: (f :*: g) a -> f a
ffst :: (:*:) f g a -> f a
ffst (f a
x :*: g a
_) = f a
x

fsnd :: (f :*: g) a -> g a
fsnd :: (:*:) f g a -> g a
fsnd (f a
_ :*: g a
x) = g a
x

instance (Functor f, Functor g) => Functor (f :*: g) where
    fmap :: (a -> b) -> (:*:) f g a -> (:*:) f g b
fmap a -> b
h (f a
f :*: g a
g) = ((a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
h f a
f f b -> g b -> (:*:) f g b
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
:*: (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
h g a
g)


instance (Foldable f, Foldable g) => Foldable (f :*: g) where
    foldr :: (a -> b -> b) -> b -> (:*:) f g a -> b
foldr a -> b -> b
f b
e (f a
x :*: g a
y) = (a -> b -> b) -> b -> f a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f ((a -> b -> b) -> b -> g a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f b
e g a
y) f a
x
    foldl :: (b -> a -> b) -> b -> (:*:) f g a -> b
foldl b -> a -> b
f b
e (f a
x :*: g a
y) = (b -> a -> b) -> b -> g a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> a -> b
f ((b -> a -> b) -> b -> f a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> a -> b
f b
e f a
x) g a
y


instance (Traversable f, Traversable g) => Traversable (f :*: g) where
    traverse :: (a -> f b) -> (:*:) f g a -> f ((:*:) f g b)
traverse a -> f b
f (f a
x :*: g a
y) = (f b -> g b -> (:*:) f g b)
-> f (f b) -> f (g b) -> f ((:*:) f g b)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 f b -> g b -> (:*:) f g b
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
(:*:) ((a -> f b) -> f a -> f (f b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f f a
x) ((a -> f b) -> g a -> f (g b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f g a
y)
    sequenceA :: (:*:) f g (f a) -> f ((:*:) f g a)
sequenceA (f (f a)
x :*: g (f a)
y) = (f a -> g a -> (:*:) f g a)
-> f (f a) -> f (g a) -> f ((:*:) f g a)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
(:*:)(f (f a) -> f (f a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA f (f a)
x) (g (f a) -> f (g a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA g (f a)
y)
    mapM :: (a -> m b) -> (:*:) f g a -> m ((:*:) f g b)
mapM a -> m b
f (f a
x :*: g a
y) = (f b -> g b -> (:*:) f g b)
-> m (f b) -> m (g b) -> m ((:*:) f g b)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 f b -> g b -> (:*:) f g b
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
(:*:) ((a -> m b) -> f a -> m (f b)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m b
f f a
x) ((a -> m b) -> g a -> m (g b)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m b
f g a
y)
    sequence :: (:*:) f g (m a) -> m ((:*:) f g a)
sequence (f (m a)
x :*: g (m a)
y) = (f a -> g a -> (:*:) f g a)
-> m (f a) -> m (g a) -> m ((:*:) f g a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
(:*:) (f (m a) -> m (f a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence f (m a)
x) (g (m a) -> m (g a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence g (m a)
y)

-- Constant Products

infixr 7 :&:

{-| This data type adds a constant product (annotation) to a signature. -}
data (f :&: a) e = f e :&: a


instance (Functor f) => Functor (f :&: a) where
    fmap :: (a -> b) -> (:&:) f a a -> (:&:) f a b
fmap a -> b
f (f a
v :&: a
c) = (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f f a
v f b -> a -> (:&:) f a b
forall k (f :: k -> *) a (e :: k). f e -> a -> (:&:) f a e
:&: a
c

instance (Foldable f) => Foldable (f :&: a) where
    fold :: (:&:) f a m -> m
fold (f m
v :&: a
_) = f m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold f m
v
    foldMap :: (a -> m) -> (:&:) f a a -> m
foldMap a -> m
f (f a
v :&: a
_) = (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f f a
v
    foldr :: (a -> b -> b) -> b -> (:&:) f a a -> b
foldr a -> b -> b
f b
e (f a
v :&: a
_) = (a -> b -> b) -> b -> f a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f b
e f a
v
    foldl :: (b -> a -> b) -> b -> (:&:) f a a -> b
foldl b -> a -> b
f b
e (f a
v :&: a
_) = (b -> a -> b) -> b -> f a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> a -> b
f b
e f a
v
    foldr1 :: (a -> a -> a) -> (:&:) f a a -> a
foldr1 a -> a -> a
f (f a
v :&: a
_) = (a -> a -> a) -> f a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 a -> a -> a
f f a
v
    foldl1 :: (a -> a -> a) -> (:&:) f a a -> a
foldl1 a -> a -> a
f (f a
v :&: a
_) = (a -> a -> a) -> f a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 a -> a -> a
f f a
v

instance (Traversable f) => Traversable (f :&: a) where
    traverse :: (a -> f b) -> (:&:) f a a -> f ((:&:) f a b)
traverse a -> f b
f (f a
v :&: a
c) = (f b -> (:&:) f a b) -> f (f b) -> f ((:&:) f a b)
forall (f :: * -> *) a b. Applicative f => (a -> b) -> f a -> f b
liftA (f b -> a -> (:&:) f a b
forall k (f :: k -> *) a (e :: k). f e -> a -> (:&:) f a e
:&: a
c) ((a -> f b) -> f a -> f (f b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f f a
v)
    sequenceA :: (:&:) f a (f a) -> f ((:&:) f a a)
sequenceA (f (f a)
v :&: a
c) = (f a -> (:&:) f a a) -> f (f a) -> f ((:&:) f a a)
forall (f :: * -> *) a b. Applicative f => (a -> b) -> f a -> f b
liftA (f a -> a -> (:&:) f a a
forall k (f :: k -> *) a (e :: k). f e -> a -> (:&:) f a e
:&: a
c)(f (f a) -> f (f a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA f (f a)
v)
    mapM :: (a -> m b) -> (:&:) f a a -> m ((:&:) f a b)
mapM a -> m b
f (f a
v :&: a
c) = (f b -> (:&:) f a b) -> m (f b) -> m ((:&:) f a b)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (f b -> a -> (:&:) f a b
forall k (f :: k -> *) a (e :: k). f e -> a -> (:&:) f a e
:&: a
c) ((a -> m b) -> f a -> m (f b)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m b
f f a
v)
    sequence :: (:&:) f a (m a) -> m ((:&:) f a a)
sequence (f (m a)
v :&: a
c) = (f a -> (:&:) f a a) -> m (f a) -> m ((:&:) f a a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (f a -> a -> (:&:) f a a
forall k (f :: k -> *) a (e :: k). f e -> a -> (:&:) f a e
:&: a
c) (f (m a) -> m (f a)
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence f (m a)
v)

{-| This class defines how to distribute an annotation over a sum of
signatures. -}
class DistAnn s p s' | s' -> s, s' -> p where
    {-| Inject an annotation over a signature. -}
    injectA :: p -> s a -> s' a
    {-| Project an annotation from a signature. -}
    projectA :: s' a -> (s a, p)


class RemA s s' | s -> s'  where
    {-| Remove annotations from a signature. -}
    remA :: s a -> s' a

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


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


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

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

    projectA :: (:&:) f p a -> (f a, p)
projectA (f a
v :&: p
p) = (f a
v,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
c (Inl f a
v) = (:&:) f p a -> (:+:) (f :&: p) s' a
forall k (f :: k -> *) (g :: k -> *) (e :: k). f e -> (:+:) f g e
Inl (f a
v f a -> p -> (:&:) f p a
forall k (f :: k -> *) a (e :: k). f e -> a -> (:&:) f a e
:&: p
c)
    injectA p
c (Inr s a
v) = s' a -> (:+:) (f :&: p) s' a
forall k (f :: k -> *) (g :: k -> *) (e :: k). g e -> (:+:) f g e
Inr (s' a -> (:+:) (f :&: p) s' a) -> s' a -> (:+:) (f :&: p) s' a
forall a b. (a -> b) -> a -> b
$ p -> s a -> s' a
forall k (s :: k -> *) p (s' :: k -> *) (a :: k).
DistAnn s p s' =>
p -> s a -> s' a
injectA p
c s a
v

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