{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Extensible.Sum (
(:|)(..)
, hoist
, embed
, strike
, strikeAt
, (<:|)
, exhaust
, embedAssoc
) where
import Data.Extensible.Class
import Data.Profunctor
import Data.Proxy
import Data.Type.Equality
import Type.Membership
data (h :: k -> *) :| (s :: [k]) where
EmbedAt :: !(Membership xs x) -> h x -> h :| xs
instance Enum (Proxy :| xs) where
fromEnum (EmbedAt m _) = fromIntegral $ getMemberId m
toEnum i = reifyMembership (fromIntegral i) $ \m -> EmbedAt m Proxy
instance (Last xs ∈ xs) => Bounded (Proxy :| xs) where
minBound = reifyMembership 0 $ \m -> EmbedAt m Proxy
maxBound = EmbedAt (membership :: Membership xs (Last xs)) Proxy
hoist :: (forall x. g x -> h x) -> g :| xs -> h :| xs
hoist f (EmbedAt p h) = EmbedAt p (f h)
{-# INLINE hoist #-}
embed :: (x ∈ xs) => h x -> h :| xs
embed = EmbedAt membership
{-# INLINE embed #-}
strike :: forall h x xs. (x ∈ xs) => h :| xs -> Maybe (h x)
strike = strikeAt membership
{-# INLINE strike #-}
strikeAt :: forall h x xs. Membership xs x -> h :| xs -> Maybe (h x)
strikeAt q (EmbedAt p h) = case compareMembership p q of
Right Refl -> Just h
_ -> Nothing
{-# INLINE strikeAt #-}
(<:|) :: (h x -> r)
-> (h :| xs -> r)
-> h :| (x ': xs)
-> r
(<:|) r c = \(EmbedAt i h) -> testMembership i
(\Refl -> r h)
(\j -> c (EmbedAt j h))
infixr 1 <:|
{-# INLINE (<:|) #-}
exhaust :: h :| '[] -> r
exhaust _ = error "Impossible"
embedAssoc :: Lookup xs k a => h (k ':> a) -> h :| xs
embedAssoc = EmbedAt association
{-# INLINE embedAssoc #-}
instance (Applicative f, Choice p) => Extensible f p (:|) where
pieceAt m = dimap (\t@(EmbedAt i h) -> case compareMembership i m of
Right Refl -> Right h
Left _ -> Left t) (either pure (fmap (EmbedAt m))) . right'
{-# INLINABLE pieceAt #-}