Copyright	(c) 2023 Yamada Ryo (c) 2023 Casper Bach Poulsen and Cas van der Rest
License	MPL-2.0 (see the file LICENSE)
Maintainer	ymdfield@outlook.jp
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	GHC2021

Data.Free.Sum

Description

An implementation of an open union for first-order effects using recursively nested binary sums.

Synopsis

type (<) f g = SumMember (IsHeadInsOf f g) f g
type family IsHeadInsOf (f :: Instruction) g where ...
class isHead ~ (f `IsHeadInsOf` g) => SumMember isHead (f :: Instruction) g where
- injSum :: f a -> g a
- projSum :: g a -> Maybe (f a)
newtype SumUnion fs a = SumUnion {
- unSumUnion :: Sum fs a
}
type family Sum fs where ...
type (+) = (:+:)
caseF :: (f a -> r) -> (g a -> r) -> (f + g) a -> r
absurdL :: (NopI + f) ~> f
absurdR :: (f + NopI) ~> f
swapSum :: (f + g) a -> (g + f) a
inj :: forall f g. f < g => f ~> g
proj :: forall f g a. f < g => g a -> Maybe (f a)
pattern L1 :: f p -> (:+:) f g p
pattern R1 :: g p -> (:+:) f g p

Documentation

type (<) f g = SumMember (IsHeadInsOf f g) f g Source #

type family IsHeadInsOf (f :: Instruction) g where ... Source #

Equations

IsHeadInsOf f (f + g) = 'True
IsHeadInsOf _ _ = 'False

class isHead ~ (f `IsHeadInsOf` g) => SumMember isHead (f :: Instruction) g where Source #

Methods

injSum :: f a -> g a Source #

projSum :: g a -> Maybe (f a) Source #

Instances

Instances details

(IsHeadInsOf f (g + h) ~ 'False, f < h) => SumMember 'False f (g + h) Source #
Instance details Defined in Data.Free.Sum Methods injSum :: f a -> (g + h) a Source # projSum :: (g + h) a -> Maybe (f a) Source #
SumMember 'True f (f + g) Source #
Instance details Defined in Data.Free.Sum Methods injSum :: f a -> (f + g) a Source # projSum :: (f + g) a -> Maybe (f a) Source #

newtype SumUnion fs a Source #

An implementation of an open union for first-order effects using recursively nested binary sums.

Constructors

SumUnion
Fields unSumUnion :: Sum fs a

Instances

Instances details

Union SumUnion Source #
Instance details Defined in Data.Free.Sum Associated Types type HasMembership SumUnion f fs Source # Methods inject :: forall (f :: Instruction) (fs :: [Instruction]). HasMembership SumUnion f fs => f ~> SumUnion fs Source # project :: forall f (fs :: [Instruction]) a. HasMembership SumUnion f fs => SumUnion fs a -> Maybe (f a) Source # absurdUnion :: SumUnion '[] a -> x Source # comp :: forall f a (fs :: [Instruction]). Either (f a) (SumUnion fs a) -> SumUnion (f ': fs) a Source # decomp :: forall f (fs :: [Instruction]) a. SumUnion (f ': fs) a -> Either (f a) (SumUnion fs a) Source # (\|+\|:) :: forall f a r (fs :: [Instruction]). (f a -> r) -> (SumUnion fs a -> r) -> SumUnion (f ': fs) a -> r Source # inject0 :: forall (f :: Type -> Type) (fs :: [Type -> Type]). f ~> SumUnion (f ': fs) Source # injectUnder :: forall (f2 :: Type -> Type) (f1 :: Type -> Type) (fs :: [Type -> Type]). f2 ~> SumUnion (f1 ': (f2 ': fs)) Source # injectUnder2 :: forall (f3 :: Type -> Type) (f1 :: Type -> Type) (f2 :: Type -> Type) (fs :: [Type -> Type]). f3 ~> SumUnion (f1 ': (f2 ': (f3 ': fs))) Source # injectUnder3 :: forall (f4 :: Type -> Type) (f1 :: Type -> Type) (f2 :: Type -> Type) (f3 :: Type -> Type) (fs :: [Type -> Type]). f4 ~> SumUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source # weaken :: forall (fs :: [Instruction]) a (f :: Instruction). SumUnion fs a -> SumUnion (f ': fs) a Source # weaken2 :: forall (fs :: [Instruction]) a (f1 :: Instruction) (f2 :: Instruction). SumUnion fs a -> SumUnion (f1 ': (f2 ': fs)) a Source # weaken3 :: forall (fs :: [Instruction]) a (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction). SumUnion fs a -> SumUnion (f1 ': (f2 ': (f3 ': fs))) a Source # weaken4 :: forall (fs :: [Instruction]) a (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (f4 :: Instruction). SumUnion fs a -> SumUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) a Source # weakenUnder :: forall (f1 :: Instruction) (fs :: [Instruction]) (f2 :: Instruction). SumUnion (f1 ': fs) ~> SumUnion (f1 ': (f2 ': fs)) Source # weakenUnder2 :: forall (f1 :: Instruction) (f2 :: Instruction) (fs :: [Instruction]) (f3 :: Instruction). SumUnion (f1 ': (f2 ': fs)) ~> SumUnion (f1 ': (f2 ': (f3 ': fs))) Source # weakenUnder3 :: forall (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]) (f4 :: Instruction). SumUnion (f1 ': (f2 ': (f3 ': fs))) ~> SumUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source # weaken2Under :: forall (f1 :: Instruction) (fs :: [Instruction]) (f2 :: Instruction) (f3 :: Instruction). SumUnion (f1 ': fs) ~> SumUnion (f1 ': (f2 ': (f3 ': fs))) Source # weaken2Under2 :: forall (f1 :: Instruction) (f2 :: Instruction) (fs :: [Instruction]) (f3 :: Instruction) (f4 :: Instruction). SumUnion (f1 ': (f2 ': fs)) ~> SumUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source # weaken3Under :: forall (f1 :: Instruction) (fs :: [Instruction]) (f2 :: Instruction) (f3 :: Instruction) (f4 :: Instruction). SumUnion (f1 ': fs) ~> SumUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source # flipUnion :: forall (f1 :: Instruction) (f2 :: Instruction) (fs :: [Instruction]). SumUnion (f1 ': (f2 ': fs)) ~> SumUnion (f2 ': (f1 ': fs)) Source # flipUnion3 :: forall (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]). SumUnion (f1 ': (f2 ': (f3 ': fs))) ~> SumUnion (f3 ': (f2 ': (f1 ': fs))) Source # flipUnionUnder :: forall (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]). SumUnion (f1 ': (f2 ': (f3 ': fs))) ~> SumUnion (f1 ': (f3 ': (f2 ': fs))) Source # rot3 :: forall (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]). SumUnion (f1 ': (f2 ': (f3 ': fs))) ~> SumUnion (f2 ': (f3 ': (f1 ': fs))) Source # rot3' :: forall (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]). SumUnion (f1 ': (f2 ': (f3 ': fs))) ~> SumUnion (f3 ': (f1 ': (f2 ': fs))) Source # bundleUnion2 :: forall (u' :: [Instruction] -> Instruction) (f1 :: Instruction) (f2 :: Instruction) (fs :: [Instruction]). Union u' => SumUnion (f1 ': (f2 ': fs)) ~> SumUnion (u' '[f1, f2] ': fs) Source # bundleUnion3 :: forall (u' :: [Instruction] -> Instruction) (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]). Union u' => SumUnion (f1 ': (f2 ': (f3 ': fs))) ~> SumUnion (u' '[f1, f2, f3] ': fs) Source # bundleUnion4 :: forall (u' :: [Instruction] -> Instruction) (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (f4 :: Instruction) (fs :: [Instruction]). Union u' => SumUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) ~> SumUnion (u' '[f1, f2, f3, f4] ': fs) Source # unbundleUnion2 :: forall (u' :: [Instruction] -> Instruction) (f1 :: Instruction) (f2 :: Instruction) (fs :: [Instruction]). Union u' => SumUnion (u' '[f1, f2] ': fs) ~> SumUnion (f1 ': (f2 ': fs)) Source # unbundleUnion3 :: forall (u' :: [Instruction] -> Instruction) (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]). Union u' => SumUnion (u' '[f1, f2, f3] ': fs) ~> SumUnion (f1 ': (f2 ': (f3 ': fs))) Source # unbundleUnion4 :: forall (u' :: [Instruction] -> Instruction) (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (f4 :: Instruction) (fs :: [Instruction]). Union u' => SumUnion (u' '[f1, f2, f3, f4] ': fs) ~> SumUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source #
(Foldable f, Foldable (Sum fs)) => Foldable (SumUnion (f ': fs)) Source #
Instance details Defined in Data.Free.Sum Methods fold :: Monoid m => SumUnion (f ': fs) m -> m # foldMap :: Monoid m => (a -> m) -> SumUnion (f ': fs) a -> m # foldMap' :: Monoid m => (a -> m) -> SumUnion (f ': fs) a -> m # foldr :: (a -> b -> b) -> b -> SumUnion (f ': fs) a -> b # foldr' :: (a -> b -> b) -> b -> SumUnion (f ': fs) a -> b # foldl :: (b -> a -> b) -> b -> SumUnion (f ': fs) a -> b # foldl' :: (b -> a -> b) -> b -> SumUnion (f ': fs) a -> b # foldr1 :: (a -> a -> a) -> SumUnion (f ': fs) a -> a # foldl1 :: (a -> a -> a) -> SumUnion (f ': fs) a -> a # toList :: SumUnion (f ': fs) a -> [a] # null :: SumUnion (f ': fs) a -> Bool # length :: SumUnion (f ': fs) a -> Int # elem :: Eq a => a -> SumUnion (f ': fs) a -> Bool # maximum :: Ord a => SumUnion (f ': fs) a -> a # minimum :: Ord a => SumUnion (f ': fs) a -> a # sum :: Num a => SumUnion (f ': fs) a -> a # product :: Num a => SumUnion (f ': fs) a -> a #
Foldable (SumUnion ('[] :: [Type -> Type])) Source #
Instance details Defined in Data.Free.Sum Methods fold :: Monoid m => SumUnion '[] m -> m # foldMap :: Monoid m => (a -> m) -> SumUnion '[] a -> m # foldMap' :: Monoid m => (a -> m) -> SumUnion '[] a -> m # foldr :: (a -> b -> b) -> b -> SumUnion '[] a -> b # foldr' :: (a -> b -> b) -> b -> SumUnion '[] a -> b # foldl :: (b -> a -> b) -> b -> SumUnion '[] a -> b # foldl' :: (b -> a -> b) -> b -> SumUnion '[] a -> b # foldr1 :: (a -> a -> a) -> SumUnion '[] a -> a # foldl1 :: (a -> a -> a) -> SumUnion '[] a -> a # toList :: SumUnion '[] a -> [a] # null :: SumUnion '[] a -> Bool # length :: SumUnion '[] a -> Int # elem :: Eq a => a -> SumUnion '[] a -> Bool # maximum :: Ord a => SumUnion '[] a -> a # minimum :: Ord a => SumUnion '[] a -> a # sum :: Num a => SumUnion '[] a -> a # product :: Num a => SumUnion '[] a -> a #
(Traversable f, Traversable (Sum fs)) => Traversable (SumUnion (f ': fs)) Source #
Instance details Defined in Data.Free.Sum Methods traverse :: Applicative f0 => (a -> f0 b) -> SumUnion (f ': fs) a -> f0 (SumUnion (f ': fs) b) # sequenceA :: Applicative f0 => SumUnion (f ': fs) (f0 a) -> f0 (SumUnion (f ': fs) a) # mapM :: Monad m => (a -> m b) -> SumUnion (f ': fs) a -> m (SumUnion (f ': fs) b) # sequence :: Monad m => SumUnion (f ': fs) (m a) -> m (SumUnion (f ': fs) a) #
Traversable (SumUnion ('[] :: [Type -> Type])) Source #
Instance details Defined in Data.Free.Sum Methods traverse :: Applicative f => (a -> f b) -> SumUnion '[] a -> f (SumUnion '[] b) # sequenceA :: Applicative f => SumUnion '[] (f a) -> f (SumUnion '[] a) # mapM :: Monad m => (a -> m b) -> SumUnion '[] a -> m (SumUnion '[] b) # sequence :: Monad m => SumUnion '[] (m a) -> m (SumUnion '[] a) #
(Functor f, Functor (Sum fs)) => Functor (SumUnion (f ': fs)) Source #
Instance details Defined in Data.Free.Sum Methods fmap :: (a -> b) -> SumUnion (f ': fs) a -> SumUnion (f ': fs) b # (<$) :: a -> SumUnion (f ': fs) b -> SumUnion (f ': fs) a #
Functor (SumUnion ('[] :: [Type -> Type])) Source #
Instance details Defined in Data.Free.Sum Methods fmap :: (a -> b) -> SumUnion '[] a -> SumUnion '[] b # (<$) :: a -> SumUnion '[] b -> SumUnion '[] a #
type HasMembership SumUnion f fs Source #
Instance details Defined in Data.Free.Sum type HasMembership SumUnion f fs = f < Sum fs

type family Sum fs where ... Source #

Equations

Sum '[] = NopI
Sum (f ': fs) = f :+: Sum fs

type (+) = (:+:) infixr 6 Source #

A type synonym for disambiguation to the sum on the higher-order side.

caseF :: (f a -> r) -> (g a -> r) -> (f + g) a -> r Source #

absurdL :: (NopI + f) ~> f Source #

absurdR :: (f + NopI) ~> f Source #

swapSum :: (f + g) a -> (g + f) a Source #

inj :: forall f g. f < g => f ~> g Source #

proj :: forall f g a. f < g => g a -> Maybe (f a) Source #

pattern L1 :: f p -> (:+:) f g p #

pattern R1 :: g p -> (:+:) f g p #