module Data.Extensible.Sum (
(:|)(..)
, hoist
, embed
, (<:|)
, exhaust
, picked
) where
import Data.Extensible.Internal
import Control.Applicative
import Data.Typeable
data (h :: k -> *) :| (s :: [k]) where
UnionAt :: !(Membership xs x) -> h x -> h :| xs
deriving instance Typeable (:|)
hoist :: (forall x. g x -> h x) -> g :| xs -> h :| xs
hoist f (UnionAt pos h) = UnionAt pos (f h)
embed :: (x ∈ xs) => h x -> h :| xs
embed = UnionAt membership
(<:|) :: (h x -> r) -> (h :| xs -> r) -> h :| (x ': xs) -> r
(<:|) r c = \(UnionAt pos h) -> runMembership pos
(\Refl -> r h)
(\pos' -> c (UnionAt pos' h))
infixr 1 <:|
exhaust :: h :| '[] -> r
exhaust _ = error "Impossible"
picked :: forall f h x xs. (x ∈ xs, Applicative f) => (h x -> f (h x)) -> h :| xs -> f (h :| xs)
picked f u@(UnionAt pos h) = case compareMembership (membership :: Membership xs x) pos of
Right Refl -> fmap (UnionAt pos) (f h)
_ -> pure u