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

--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Ops
-- Copyright   :  Original (c) 2011 Patrick Bahr; modifications (c) 2020 James Koppel
-- License     :  BSD3
--
-- This module provides operators on higher-order functors. All definitions are
-- generalised versions of those in "Data.Comp.Ops".
--
--------------------------------------------------------------------------------

module Data.Comp.Multi.Ops
    ( Sum (..)
    , caseH
    , (:<:)
    , (:-<:)
    , inj
    , proj
    , (:=:)
    , spl
    , (:&:)(..)
    , RemA(..)
    , (O.:*:)(..)
    , O.ffst
    , O.fsnd
    , unsafeMapSum
    , unsafeElem
    , caseCxt
    , caseSumF
    , caseSum
    , Alts
    , Alt
    , alt
    , (<|)
    , cons
    , nil
    , Elem
    , pattern Elem
    , Mem
    , at
    , witness
    , extend
    , contract
    ) where

import Control.Monad
import Data.Default
import Data.Functor
import Data.Functor.Identity
import Data.Type.Equality
import Data.Comp.Multi.Alt
import Data.Comp.Multi.HFoldable
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.HTraversable
import Data.Comp.Multi.Kinds
import qualified Data.Comp.Ops as O
import Data.Comp.Elem
import Data.Comp.Dict

-------------------------------------------------------------

-- | Data type defining a sum of signatures.
--
--   It is inspired by modular reifiable matching, as described in
--
--   * Oliveira, Bruno C. D. S., Shin-Cheng Mu, and Shu-Hung You.
--     \"Modular reifiable matching: a list-of-functors approach to two-level types.\"
--     In Haskell Symposium, 2015.
--
--   except that this definition uses value-level integers (in the `Elem` datatype) in place
--   of type-level naturals. It hence uses `unsafeCoerce` under the hood, but is type-safe if used
--   through the public API. The result is that values of this type take constant memory with respect to the number
--   of summands (unlike vanilla datatypes à la carte), and constant time to dereference
--   (unlike modular reifiable matching). The representation is the bare minimum: an int representing the alternative,
--   and pointer to the value.
data Sum (fs :: Signature) h e where
  Sum :: Elem f fs -> f h e -> Sum fs h e

at :: Elem f fs -> Sum fs a e -> Maybe (f a e)
at :: forall (f :: Fragment) (fs :: [Fragment]) (a :: Family)
       (e :: Sort).
Elem f fs -> Sum fs a e -> Maybe (f a e)
at Elem f fs
e (Sum Elem f fs
wit f a e
a) =
  case Elem f fs -> Elem f fs -> Maybe (f :~: f)
forall {k :: Sort} (f :: k) (g :: k) (fs :: [k]).
Elem f fs -> Elem g fs -> Maybe (f :~: g)
elemEq Elem f fs
e Elem f fs
wit of
    Just f :~: f
Refl -> f a e -> Maybe (f a e)
forall (a :: Sort). a -> Maybe a
Just f a e
f a e
a
    Maybe (f :~: f)
Nothing   -> Maybe (f a e)
forall (a :: Sort). Maybe a
Nothing

{-| Utility function to case on a higher-order functor sum, without exposing the
  internal representation of sums. -}
{-# INLINE caseH #-}
caseH :: Alts fs a e b -> Sum fs a e -> b
caseH :: forall (fs :: [Fragment]) (a :: Family) (e :: Sort) (b :: Sort).
Alts fs a e b -> Sum fs a e -> b
caseH Alts fs a e b
alts (Sum Elem f fs
wit f a e
v) = Elem f fs -> Alts fs a e b -> f a e -> b
forall (f :: Fragment) (fs :: [Fragment]) (a :: Family) (e :: Sort)
       (b :: Sort).
Elem f fs -> Alts fs a e b -> f a e -> b
extractAt Elem f fs
wit Alts fs a e b
alts f a e
v

{-# INLINE caseCxt #-}
caseCxt :: forall cxt fs a e b. (All cxt fs) => (forall f. (cxt f) => f a e -> b) -> Sum fs a e -> b
caseCxt :: forall (cxt :: Fragment -> Constraint) (fs :: [Fragment])
       (a :: Family) (e :: Sort) (b :: Sort).
All cxt fs =>
(forall (f :: Fragment). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt forall (f :: Fragment). cxt f => f a e -> b
f (Sum Elem f fs
wit f a e
v) = f a e -> b
forall (f :: Fragment). cxt f => f a e -> b
f f a e
v (cxt f => b) -> Dict cxt f -> b
forall {k :: Sort} (c :: k -> Constraint) (a :: k) (r :: Sort).
(c a => r) -> Dict c a -> r
\\ forall {k :: Sort} (c :: k -> Constraint) (f :: k) (fs :: [k]).
All c fs =>
Elem f fs -> Dict c f
forall (c :: Fragment -> Constraint) (f :: Fragment)
       (fs :: [Fragment]).
All c fs =>
Elem f fs -> Dict c f
dictFor @cxt Elem f fs
wit

{-# INLINE caseSumF #-}
caseSumF :: forall cxt f fs a e b. (All cxt fs, Functor f) => (forall g. (cxt g) => g a e -> f (g b e)) -> Sum fs a e -> f (Sum fs b e)
caseSumF :: forall (cxt :: Fragment -> Constraint) (f :: Family)
       (fs :: [Fragment]) (a :: Family) (e :: Sort) (b :: Family).
(All cxt fs, Functor f) =>
(forall (g :: Fragment). cxt g => g a e -> f (g b e))
-> Sum fs a e -> f (Sum fs b e)
caseSumF forall (g :: Fragment). cxt g => g a e -> f (g b e)
f (Sum Elem f fs
wit f a e
v) = Elem f fs -> f b e -> Sum fs b e
forall (f :: Fragment) (fs :: [Fragment]) (h :: Family)
       (e :: Sort).
Elem f fs -> f h e -> Sum fs h e
Sum Elem f fs
wit (f b e -> Sum fs b e) -> f (f b e) -> f (Sum fs b e)
forall (f :: Family) (a :: Sort) (b :: Sort).
Functor f =>
(a -> b) -> f a -> f b
<$> f a e -> f (f b e)
forall (g :: Fragment). cxt g => g a e -> f (g b e)
f f a e
v (cxt f => f (Sum fs b e)) -> Dict cxt f -> f (Sum fs b e)
forall {k :: Sort} (c :: k -> Constraint) (a :: k) (r :: Sort).
(c a => r) -> Dict c a -> r
\\ forall {k :: Sort} (c :: k -> Constraint) (f :: k) (fs :: [k]).
All c fs =>
Elem f fs -> Dict c f
forall (c :: Fragment -> Constraint) (f :: Fragment)
       (fs :: [Fragment]).
All c fs =>
Elem f fs -> Dict c f
dictFor @cxt Elem f fs
wit

{-# INLINE caseSum #-}
caseSum :: forall cxt fs a e b. (All cxt fs) => (forall g. (cxt g) => g a e -> g b e) -> Sum fs a e -> Sum fs b e
caseSum :: forall (cxt :: Fragment -> Constraint) (fs :: [Fragment])
       (a :: Family) (e :: Sort) (b :: Family).
All cxt fs =>
(forall (g :: Fragment). cxt g => g a e -> g b e)
-> Sum fs a e -> Sum fs b e
caseSum forall (g :: Fragment). cxt g => g a e -> g b e
f = Identity (Sum fs b e) -> Sum fs b e
forall (a :: Sort). Identity a -> a
runIdentity (Identity (Sum fs b e) -> Sum fs b e)
-> (Sum fs a e -> Identity (Sum fs b e))
-> Sum fs a e
-> Sum fs b e
forall (b :: Sort) (c :: Sort) (a :: Sort).
(b -> c) -> (a -> b) -> a -> c
. forall (cxt :: Fragment -> Constraint) (f :: Family)
       (fs :: [Fragment]) (a :: Family) (e :: Sort) (b :: Family).
(All cxt fs, Functor f) =>
(forall (g :: Fragment). cxt g => g a e -> f (g b e))
-> Sum fs a e -> f (Sum fs b e)
caseSumF @cxt (g b e -> Identity (g b e)
forall (a :: Sort). a -> Identity a
Identity (g b e -> Identity (g b e))
-> (g a e -> g b e) -> g a e -> Identity (g b e)
forall (b :: Sort) (c :: Sort) (a :: Sort).
(b -> c) -> (a -> b) -> a -> c
. g a e -> g b e
forall (g :: Fragment). cxt g => g a e -> g b e
f) 

instance (All HFunctor fs) => HFunctor (Sum fs) where
    hfmap :: forall (f :: Family) (g :: Family).
(f :-> g) -> Sum fs f :-> Sum fs g
hfmap f :-> g
f = forall (cxt :: Fragment -> Constraint) (fs :: [Fragment])
       (a :: Family) (e :: Sort) (b :: Family).
All cxt fs =>
(forall (g :: Fragment). cxt g => g a e -> g b e)
-> Sum fs a e -> Sum fs b e
caseSum @HFunctor ((f :-> g) -> g f :-> g g
forall (f :: Family) (g :: Family). (f :-> g) -> g f :-> g g
forall (h :: Fragment) (f :: Family) (g :: Family).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap f i -> g i
f :-> g
f)
      
instance ( All HFoldable fs
         , All HFunctor fs
         ) => HFoldable (Sum fs) where
    hfold :: forall (m :: Sort). Monoid m => Sum fs (K m) :=> m
hfold      = forall (cxt :: Fragment -> Constraint) (fs :: [Fragment])
       (a :: Family) (e :: Sort) (b :: Sort).
All cxt fs =>
(forall (f :: Fragment). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @HFoldable f (K m) i -> m
f (K m) :=> m
forall (m :: Sort). Monoid m => f (K m) :=> m
forall (f :: Fragment). HFoldable f => f (K m) i -> m
forall (h :: Fragment) (m :: Sort).
(HFoldable h, Monoid m) =>
h (K m) :=> m
hfold
    hfoldMap :: forall (m :: Sort) (a :: Family).
Monoid m =>
(a :=> m) -> Sum fs a :=> m
hfoldMap a :=> m
f = forall (cxt :: Fragment -> Constraint) (fs :: [Fragment])
       (a :: Family) (e :: Sort) (b :: Sort).
All cxt fs =>
(forall (f :: Fragment). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @HFoldable ((a :=> m) -> f a :=> m
forall (m :: Sort) (a :: Family).
Monoid m =>
(a :=> m) -> f a :=> m
forall (h :: Fragment) (m :: Sort) (a :: Family).
(HFoldable h, Monoid m) =>
(a :=> m) -> h a :=> m
hfoldMap a i -> m
a :=> m
f)
    hfoldr :: forall (a :: Family) (b :: Sort).
(a :=> (b -> b)) -> b -> Sum fs a :=> b
hfoldr a :=> (b -> b)
f b
b = forall (cxt :: Fragment -> Constraint) (fs :: [Fragment])
       (a :: Family) (e :: Sort) (b :: Sort).
All cxt fs =>
(forall (f :: Fragment). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @HFoldable ((a :=> (b -> b)) -> b -> f a :=> b
forall (a :: Family) (b :: Sort).
(a :=> (b -> b)) -> b -> f a :=> b
forall (h :: Fragment) (a :: Family) (b :: Sort).
HFoldable h =>
(a :=> (b -> b)) -> b -> h a :=> b
hfoldr a i -> b -> b
a :=> (b -> b)
f b
b)
    hfoldl :: forall (b :: Sort) (a :: Family).
(b -> a :=> b) -> b -> Sum fs a :=> b
hfoldl b -> a :=> b
f b
b = forall (cxt :: Fragment -> Constraint) (fs :: [Fragment])
       (a :: Family) (e :: Sort) (b :: Sort).
All cxt fs =>
(forall (f :: Fragment). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @HFoldable ((b -> a :=> b) -> b -> f a :=> b
forall (b :: Sort) (a :: Family). (b -> a :=> b) -> b -> f a :=> b
forall (h :: Fragment) (b :: Sort) (a :: Family).
HFoldable h =>
(b -> a :=> b) -> b -> h a :=> b
hfoldl b -> a i -> b
b -> a :=> b
f b
b)
    hfoldr1 :: forall (a :: Sort). (a -> a -> a) -> Sum fs (K a) :=> a
hfoldr1 a -> a -> a
f  = forall (cxt :: Fragment -> Constraint) (fs :: [Fragment])
       (a :: Family) (e :: Sort) (b :: Sort).
All cxt fs =>
(forall (f :: Fragment). cxt f => f a e -> b) -> Sum fs a e -> b
caseCxt @HFoldable ((a -> a -> a) -> f (K a) :=> a
forall (a :: Sort). (a -> a -> a) -> f (K a) :=> a
forall (h :: Fragment) (a :: Sort).
HFoldable h =>
(a -> a -> a) -> h (K a) :=> a
hfoldr1 a -> a -> a
f)

instance ( All HTraversable fs
         , All HFoldable fs
         , All HFunctor fs
         ) => HTraversable (Sum fs) where
    htraverse :: forall (f :: Family) (a :: Family) (b :: Family).
Applicative f =>
NatM f a b -> NatM f (Sum fs a) (Sum fs b)
htraverse NatM f a b
f = forall (cxt :: Fragment -> Constraint) (f :: Family)
       (fs :: [Fragment]) (a :: Family) (e :: Sort) (b :: Family).
(All cxt fs, Functor f) =>
(forall (g :: Fragment). cxt g => g a e -> f (g b e))
-> Sum fs a e -> f (Sum fs b e)
caseSumF @HTraversable (NatM f a b -> NatM f (g a) (g b)
forall (f :: Family) (a :: Family) (b :: Family).
Applicative f =>
NatM f a b -> NatM f (g a) (g b)
forall (t :: Fragment) (f :: Family) (a :: Family) (b :: Family).
(HTraversable t, Applicative f) =>
NatM f a b -> NatM f (t a) (t b)
htraverse a i -> f (b i)
NatM f a b
f)
    hmapM :: forall (m :: Family) (a :: Family) (b :: Family).
Monad m =>
NatM m a b -> NatM m (Sum fs a) (Sum fs b)
hmapM NatM m a b
f     = forall (cxt :: Fragment -> Constraint) (f :: Family)
       (fs :: [Fragment]) (a :: Family) (e :: Sort) (b :: Family).
(All cxt fs, Functor f) =>
(forall (g :: Fragment). cxt g => g a e -> f (g b e))
-> Sum fs a e -> f (Sum fs b e)
caseSumF @HTraversable (NatM m a b -> NatM m (g a) (g b)
forall (m :: Family) (a :: Family) (b :: Family).
Monad m =>
NatM m a b -> NatM m (g a) (g b)
forall (t :: Fragment) (m :: Family) (a :: Family) (b :: Family).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM a i -> m (b i)
NatM m a b
f)

-- The subsumption relation.

infixl 5 :<:
infixl 5 :=:

class (f :: Fragment) :<: (g :: Fragment) where
  inj :: f a :-> g a
  proj :: NatM Maybe (g a) (f a)

instance ( Mem f fs
         ) => f :<: (Sum fs) where
  inj :: forall (a :: Family). f a :-> Sum fs a
inj = Elem f fs -> f a i -> Sum fs a i
forall (f :: Fragment) (fs :: [Fragment]) (h :: Family)
       (e :: Sort).
Elem f fs -> f h e -> Sum fs h e
Sum Elem f fs
forall {k :: Sort} (f :: k) (fs :: [k]). Mem f fs => Elem f fs
witness
  proj :: forall (a :: Family). NatM Maybe (Sum fs a) (f a)
proj = Elem f fs -> Sum fs a i -> Maybe (f a i)
forall (f :: Fragment) (fs :: [Fragment]) (a :: Family)
       (e :: Sort).
Elem f fs -> Sum fs a e -> Maybe (f a e)
at Elem f fs
forall {k :: Sort} (f :: k) (fs :: [k]). Mem f fs => Elem f fs
witness

instance {-# OVERLAPPABLE #-}
         ( f :<: (Sum fs)
         , Default a
         ) => f :<: (Sum fs :&: a) where
  inj :: forall (a :: Family). f a :-> (:&:) (Sum fs) a a
inj f a i
x = f a i -> Sum fs a i
forall (a :: Family). f a :-> Sum fs a
forall (f :: Fragment) (g :: Fragment) (a :: Family).
(f :<: g) =>
f a :-> g a
inj f a i
x Sum fs a i -> a -> (:&:) (Sum fs) a a i
forall (f :: Fragment) (a :: Sort) (g :: Family) (e :: Sort).
f g e -> a -> (:&:) f a g e
:&: a
forall (a :: Sort). Default a => a
def
  proj :: forall (a :: Family). NatM Maybe ((:&:) (Sum fs) a a) (f a)
proj (Sum fs a i
x :&: a
_) = Sum fs a i -> Maybe (f a i)
forall (a :: Family). NatM Maybe (Sum fs a) (f a)
forall (f :: Fragment) (g :: Fragment) (a :: Family).
(f :<: g) =>
NatM Maybe (g a) (f a)
proj Sum fs a i
x

instance {-# OVERLAPS #-}
         (f :<: Sum fs
         ) => (f :&: a) :<: (Sum fs :&: a) where
  inj :: forall (a :: Family). (:&:) f a a :-> (:&:) (Sum fs) a a
inj  (f a i
x :&: a
a) = f a i -> Sum fs a i
forall (a :: Family). f a :-> Sum fs a
forall (f :: Fragment) (g :: Fragment) (a :: Family).
(f :<: g) =>
f a :-> g a
inj f a i
x Sum fs a i -> a -> (:&:) (Sum fs) a a i
forall (f :: Fragment) (a :: Sort) (g :: Family) (e :: Sort).
f g e -> a -> (:&:) f a g e
:&: a
a
  proj :: forall (a :: Family). NatM Maybe ((:&:) (Sum fs) a a) ((:&:) f a a)
proj (Sum fs a i
x :&: a
a) = Sum fs a i -> Maybe (f a i)
forall (a :: Family). NatM Maybe (Sum fs a) (f a)
forall (f :: Fragment) (g :: Fragment) (a :: Family).
(f :<: g) =>
NatM Maybe (g a) (f a)
proj Sum fs a i
x Maybe (f a i) -> (f a i -> (:&:) f a a i) -> Maybe ((:&:) f a a i)
forall (f :: Family) (a :: Sort) (b :: Sort).
Functor f =>
f a -> (a -> b) -> f b
<&> (f a i -> a -> (:&:) f a a i
forall (f :: Fragment) (a :: Sort) (g :: Family) (e :: Sort).
f g e -> a -> (:&:) f a g e
:&: a
a)

instance {-# INCOHERENT #-} f :<: f where
  inj :: forall (a :: Family). f a :-> f a
inj = f a i -> f a i
forall (a :: Sort). a -> a
id
  proj :: forall (a :: Family). NatM Maybe (f a) (f a)
proj = f a i -> Maybe (f a i)
forall (a :: Sort). a -> Maybe a
Just

-- 2023.11.13: Reviewing the GHC docs on instance resolution in manual section 6.8.8.5, this
--             seems to be
--instance {-# INCOHERENT #-} (Sum fs :&: a) :<: (Sum fs :&: a) where
--  inj = id
--  proj = Just

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

spl :: ( f :=: Sum fs
      ) => (forall e l. Alts fs a e (b l)) -> f a :-> b
spl :: forall (f :: Fragment) (fs :: [Fragment]) (a :: Family)
       (b :: Family).
(f :=: Sum fs) =>
(forall (e :: Sort) (l :: Sort). Alts fs a e (b l)) -> f a :-> b
spl forall (e :: Sort) (l :: Sort). Alts fs a e (b l)
alts = Alts fs a i (b i) -> Sum fs a i -> b i
forall (fs :: [Fragment]) (a :: Family) (e :: Sort) (b :: Sort).
Alts fs a e b -> Sum fs a e -> b
caseH Alts fs a i (b i)
forall (e :: Sort) (l :: Sort). Alts fs a e (b l)
alts (Sum fs a i -> b i) -> (f a i -> Sum fs a i) -> f a i -> b i
forall (b :: Sort) (c :: Sort) (a :: Sort).
(b -> c) -> (a -> b) -> a -> c
. f a i -> Sum fs a i
forall (a :: Family). f a :-> Sum fs a
forall (f :: Fragment) (g :: Fragment) (a :: Family).
(f :<: g) =>
f a :-> g a
inj

-- Constant Products

infixr 7 :&:

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

data ((f :: Node) :&: a) g e = f g e :&: a

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

instance (HFoldable f) => HFoldable (f :&: a) where
    hfold :: forall (m :: Sort). Monoid m => (:&:) f a (K m) :=> m
hfold (f (K m) i
v :&: a
_) = f (K m) i -> m
f (K m) :=> m
forall (m :: Sort). Monoid m => f (K m) :=> m
forall (h :: Fragment) (m :: Sort).
(HFoldable h, Monoid m) =>
h (K m) :=> m
hfold f (K m) i
v
    hfoldMap :: forall (m :: Sort) (a :: Family).
Monoid m =>
(a :=> m) -> (:&:) f a a :=> m
hfoldMap a :=> m
f (f a i
v :&: a
_) = (a :=> m) -> f a :=> m
forall (m :: Sort) (a :: Family).
Monoid m =>
(a :=> m) -> f a :=> m
forall (h :: Fragment) (m :: Sort) (a :: Family).
(HFoldable h, Monoid m) =>
(a :=> m) -> h a :=> m
hfoldMap a i -> m
a :=> m
f f a i
v
    hfoldr :: forall (a :: Family) (b :: Sort).
(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 :=> b
forall (a :: Family) (b :: Sort).
(a :=> (b -> b)) -> b -> f a :=> b
forall (h :: Fragment) (a :: Family) (b :: Sort).
HFoldable h =>
(a :=> (b -> b)) -> b -> h a :=> b
hfoldr a i -> b -> b
a :=> (b -> b)
f b
e f a i
v
    hfoldl :: forall (b :: Sort) (a :: Family).
(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 :=> b
forall (b :: Sort) (a :: Family). (b -> a :=> b) -> b -> f a :=> b
forall (h :: Fragment) (b :: Sort) (a :: Family).
HFoldable h =>
(b -> a :=> b) -> b -> h a :=> b
hfoldl b -> a i -> b
b -> a :=> b
f b
e f a i
v
    hfoldr1 :: forall (a :: Sort). (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) :=> a
forall (a :: Sort). (a -> a -> a) -> f (K a) :=> a
forall (h :: Fragment) (a :: Sort).
HFoldable h =>
(a -> a -> a) -> h (K a) :=> a
hfoldr1 a -> a -> a
f f (K a) i
v
    hfoldl1 :: forall (a :: Sort). (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) :=> a
forall (a :: Sort). (a -> a -> a) -> f (K a) :=> a
forall (h :: Fragment) (a :: Sort).
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 :: forall (f :: Family) (a :: Family) (b :: Family).
Applicative f =>
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 (f :: Fragment) (a :: Sort) (g :: Family) (e :: Sort).
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 :: Family) (a :: Sort) (b :: Sort).
Functor f =>
(a -> b) -> f a -> f b
<$> (NatM f a b -> NatM f (f a) (f b)
forall (f :: Family) (a :: Family) (b :: Family).
Applicative f =>
NatM f a b -> NatM f (f a) (f b)
forall (t :: Fragment) (f :: Family) (a :: Family) (b :: Family).
(HTraversable t, Applicative f) =>
NatM f a b -> NatM f (t a) (t b)
htraverse a i -> f (b i)
NatM f a b
f f a i
v)
    hmapM :: forall (m :: Family) (a :: Family) (b :: Family).
Monad m =>
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 :: Family) (a1 :: Sort) (r :: Sort).
Monad m =>
(a1 -> r) -> m a1 -> m r
liftM (f b i -> a -> (:&:) f a b i
forall (f :: Fragment) (a :: Sort) (g :: Family) (e :: Sort).
f g e -> a -> (:&:) f a g e
:&: a
c) (NatM m a b -> NatM m (f a) (f b)
forall (m :: Family) (a :: Family) (b :: Family).
Monad m =>
NatM m a b -> NatM m (f a) (f b)
forall (t :: Fragment) (m :: Family) (a :: Family) (b :: Family).
(HTraversable t, Monad m) =>
NatM m a b -> NatM m (t a) (t b)
hmapM a i -> m (b i)
NatM m a b
f f a i
v)

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

-- TODO: This is linear
--       Is there a way to make this constant time?
instance ( RemA f g
         , RemA (Sum fs) (Sum gs)
         ) => RemA (Sum (f ': fs)) (Sum (g ': gs)) where
  remA :: forall (a :: Family). Sum (f : fs) a :-> Sum (g : gs) a
remA (Sum Elem f (f : fs)
w f a i
a) = case Elem f (f : fs) -> Either (f :~: f) (Elem f fs)
forall {k :: Sort} (f :: k) (g :: k) (fs :: [k]).
Elem f (g : fs) -> Either (f :~: g) (Elem f fs)
contract Elem f (f : fs)
w of
    Left f :~: f
Refl -> Elem g (g : gs) -> g a i -> Sum (g : gs) a i
forall (f :: Fragment) (fs :: [Fragment]) (h :: Family)
       (e :: Sort).
Elem f fs -> f h e -> Sum fs h e
Sum Elem g (g : gs)
forall {k :: Sort} (f :: k) (fs :: [k]). Mem f fs => Elem f fs
witness (f a i -> g a i
forall (a :: Family). f a :-> g a
forall (s :: Fragment) (s' :: Fragment) (a :: Family).
RemA s s' =>
s a :-> s' a
remA f a i
a)
    Right Elem f fs
w0  -> case Sum fs a i -> Sum gs a i
Sum fs a :-> Sum gs a
forall (a :: Family).
RemA (Sum fs) (Sum gs) =>
Sum fs a :-> Sum gs a
go (Elem f fs -> f a i -> Sum fs a i
forall (f :: Fragment) (fs :: [Fragment]) (h :: Family)
       (e :: Sort).
Elem f fs -> f h e -> Sum fs h e
Sum Elem f fs
w0 f a i
a) of
      Sum Elem f gs
w1 f a i
a -> Elem f (g : gs) -> f a i -> Sum (g : gs) a i
forall (f :: Fragment) (fs :: [Fragment]) (h :: Family)
       (e :: Sort).
Elem f fs -> f h e -> Sum fs h e
Sum (Elem f gs -> Elem f (g : gs)
forall {a :: Sort} (f :: a) (fs :: [a]) (g :: a).
Elem f fs -> Elem f (g : fs)
extend Elem f gs
w1) f a i
a

    where go :: (RemA (Sum fs) (Sum gs)) => Sum fs a :-> Sum gs a
          go :: forall (a :: Family).
RemA (Sum fs) (Sum gs) =>
Sum fs a :-> Sum gs a
go = Sum fs a i -> Sum gs a i
forall (a :: Family). Sum fs a :-> Sum gs a
forall (s :: Fragment) (s' :: Fragment) (a :: Family).
RemA s s' =>
s a :-> s' a
remA

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

-- NOTE: Invariant => Length fs == Length gs
-- TODO: write gs as a function of fs.    
unsafeMapSum :: Elem f fs -> f a e -> (f a :-> g a) -> Sum gs a e
unsafeMapSum :: forall (f :: Fragment) (fs :: [Fragment]) (a :: Family) (e :: Sort)
       (g :: Fragment) (gs :: [Fragment]).
Elem f fs -> f a e -> (f a :-> g a) -> Sum gs a e
unsafeMapSum Elem f fs
wit f a e
v f a :-> g a
f = Elem g gs -> g a e -> Sum gs a e
forall (f :: Fragment) (fs :: [Fragment]) (h :: Family)
       (e :: Sort).
Elem f fs -> f h e -> Sum fs h e
Sum (Elem f fs -> Elem g gs
forall {k1 :: Sort} {k2 :: Sort} (f :: k1) (fs :: [k1]) (g :: k2)
       (gs :: [k2]).
Elem f fs -> Elem g gs
unsafeElem Elem f fs
wit) (f a e -> g a e
f a :-> g a
f f a e
v)

class (f :<: Sum fs) => f :-<: fs
instance (f :<: Sum fs) => f :-<: fs