Copyright	(c) 2023 Yamada Ryo
License	MPL-2.0 (see the file LICENSE)
Maintainer	ymdfield@outlook.jp
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	GHC2021

Data.Free.Union

Description

A type class representing a general open union for first-order effects, independent of the internal implementation.

Synopsis

class Union (u :: [Instruction] -> Instruction) where
- type HasMembership u (f :: Instruction) (fs :: [Instruction]) :: Constraint
- inject :: HasMembership u f fs => f ~> u fs
- project :: HasMembership u f fs => u fs a -> Maybe (f a)
- absurdUnion :: u '[] a -> x
- comp :: Either (f a) (u fs a) -> u (f ': fs) a
- decomp :: u (f ': fs) a -> Either (f a) (u fs a)
- (|+|:) :: (f a -> r) -> (u fs a -> r) -> u (f ': fs) a -> r
- inject0 :: f ~> u (f ': fs)
- injectUnder :: f2 ~> u (f1 ': (f2 ': fs))
- injectUnder2 :: f3 ~> u (f1 ': (f2 ': (f3 ': fs)))
- injectUnder3 :: f4 ~> u (f1 ': (f2 ': (f3 ': (f4 ': fs))))
- weaken :: u fs a -> u (f ': fs) a
- weaken2 :: u fs a -> u (f1 ': (f2 ': fs)) a
- weaken3 :: u fs a -> u (f1 ': (f2 ': (f3 ': fs))) a
- weaken4 :: u fs a -> u (f1 ': (f2 ': (f3 ': (f4 ': fs)))) a
- weakenUnder :: u (f1 ': fs) ~> u (f1 ': (f2 ': fs))
- weakenUnder2 :: u (f1 ': (f2 ': fs)) ~> u (f1 ': (f2 ': (f3 ': fs)))
- weakenUnder3 :: u (f1 ': (f2 ': (f3 ': fs))) ~> u (f1 ': (f2 ': (f3 ': (f4 ': fs))))
- weaken2Under :: u (f1 ': fs) ~> u (f1 ': (f2 ': (f3 ': fs)))
- weaken2Under2 :: u (f1 ': (f2 ': fs)) ~> u (f1 ': (f2 ': (f3 ': (f4 ': fs))))
- weaken3Under :: u (f1 ': fs) ~> u (f1 ': (f2 ': (f3 ': (f4 ': fs))))
- flipUnion :: u (f1 ': (f2 ': fs)) ~> u (f2 ': (f1 ': fs))
- flipUnion3 :: u (f1 ': (f2 ': (f3 ': fs))) ~> u (f3 ': (f2 ': (f1 ': fs)))
- flipUnionUnder :: u (f1 ': (f2 ': (f3 ': fs))) ~> u (f1 ': (f3 ': (f2 ': fs)))
- rot3 :: u (f1 ': (f2 ': (f3 ': fs))) ~> u (f2 ': (f3 ': (f1 ': fs)))
- rot3' :: u (f1 ': (f2 ': (f3 ': fs))) ~> u (f3 ': (f1 ': (f2 ': fs)))
- bundleUnion2 :: Union u' => u (f1 ': (f2 ': fs)) ~> u (u' '[f1, f2] ': fs)
- bundleUnion3 :: Union u' => u (f1 ': (f2 ': (f3 ': fs))) ~> u (u' '[f1, f2, f3] ': fs)
- bundleUnion4 :: Union u' => u (f1 ': (f2 ': (f3 ': (f4 ': fs)))) ~> u (u' '[f1, f2, f3, f4] ': fs)
- unbundleUnion2 :: Union u' => u (u' '[f1, f2] ': fs) ~> u (f1 ': (f2 ': fs))
- unbundleUnion3 :: Union u' => u (u' '[f1, f2, f3] ': fs) ~> u (f1 ': (f2 ': (f3 ': fs)))
- unbundleUnion4 :: Union u' => u (u' '[f1, f2, f3, f4] ': fs) ~> u (f1 ': (f2 ': (f3 ': (f4 ': fs))))
type family IsMember (f :: Instruction) fs where ...
type Member u f fs = (HasMembership u f fs, IsMember f fs ~ 'True)

Documentation

class Union (u :: [Instruction] -> Instruction) where Source #

A type class representing a general open union for first-order effects, independent of the internal implementation.

Minimal complete definition

inject, project, absurdUnion, (comp | inject0, weaken, decomp | (|+|:))

Associated Types

type HasMembership u (f :: Instruction) (fs :: [Instruction]) :: Constraint Source #

Methods

inject :: HasMembership u f fs => f ~> u fs Source #

project :: HasMembership u f fs => u fs a -> Maybe (f a) Source #

absurdUnion :: u '[] a -> x Source #

comp :: Either (f a) (u fs a) -> u (f ': fs) a Source #

decomp :: u (f ': fs) a -> Either (f a) (u fs a) Source #

(|+|:) :: (f a -> r) -> (u fs a -> r) -> u (f ': fs) a -> r infixr 5 Source #

inject0 :: f ~> u (f ': fs) Source #

injectUnder :: f2 ~> u (f1 ': (f2 ': fs)) Source #

injectUnder2 :: f3 ~> u (f1 ': (f2 ': (f3 ': fs))) Source #

injectUnder3 :: f4 ~> u (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source #

weaken :: u fs a -> u (f ': fs) a Source #

weaken2 :: u fs a -> u (f1 ': (f2 ': fs)) a Source #

weaken3 :: u fs a -> u (f1 ': (f2 ': (f3 ': fs))) a Source #

weaken4 :: u fs a -> u (f1 ': (f2 ': (f3 ': (f4 ': fs)))) a Source #

weakenUnder :: u (f1 ': fs) ~> u (f1 ': (f2 ': fs)) Source #

weakenUnder2 :: u (f1 ': (f2 ': fs)) ~> u (f1 ': (f2 ': (f3 ': fs))) Source #

weakenUnder3 :: u (f1 ': (f2 ': (f3 ': fs))) ~> u (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source #

weaken2Under :: u (f1 ': fs) ~> u (f1 ': (f2 ': (f3 ': fs))) Source #

weaken2Under2 :: u (f1 ': (f2 ': fs)) ~> u (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source #

weaken3Under :: u (f1 ': fs) ~> u (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source #

flipUnion :: u (f1 ': (f2 ': fs)) ~> u (f2 ': (f1 ': fs)) Source #

flipUnion3 :: u (f1 ': (f2 ': (f3 ': fs))) ~> u (f3 ': (f2 ': (f1 ': fs))) Source #

flipUnionUnder :: u (f1 ': (f2 ': (f3 ': fs))) ~> u (f1 ': (f3 ': (f2 ': fs))) Source #

rot3 :: u (f1 ': (f2 ': (f3 ': fs))) ~> u (f2 ': (f3 ': (f1 ': fs))) Source #

rot3' :: u (f1 ': (f2 ': (f3 ': fs))) ~> u (f3 ': (f1 ': (f2 ': fs))) Source #

bundleUnion2 :: Union u' => u (f1 ': (f2 ': fs)) ~> u (u' '[f1, f2] ': fs) Source #

bundleUnion3 :: Union u' => u (f1 ': (f2 ': (f3 ': fs))) ~> u (u' '[f1, f2, f3] ': fs) Source #

bundleUnion4 :: Union u' => u (f1 ': (f2 ': (f3 ': (f4 ': fs)))) ~> u (u' '[f1, f2, f3, f4] ': fs) Source #

unbundleUnion2 :: Union u' => u (u' '[f1, f2] ': fs) ~> u (f1 ': (f2 ': fs)) Source #

unbundleUnion3 :: Union u' => u (u' '[f1, f2, f3] ': fs) ~> u (f1 ': (f2 ': (f3 ': fs))) Source #

unbundleUnion4 :: Union u' => u (u' '[f1, f2, f3, f4] ': fs) ~> u (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source #

Instances

Instances details

Union ExtensibleUnion Source #
Instance details Defined in Data.Free.Extensible Associated Types type HasMembership ExtensibleUnion f fs Source # Methods inject :: forall (f :: Instruction) (fs :: [Instruction]). HasMembership ExtensibleUnion f fs => f ~> ExtensibleUnion fs Source # project :: forall f (fs :: [Instruction]) a. HasMembership ExtensibleUnion f fs => ExtensibleUnion fs a -> Maybe (f a) Source # absurdUnion :: ExtensibleUnion '[] a -> x Source # comp :: forall f a (fs :: [Instruction]). Either (f a) (ExtensibleUnion fs a) -> ExtensibleUnion (f ': fs) a Source # decomp :: forall f (fs :: [Instruction]) a. ExtensibleUnion (f ': fs) a -> Either (f a) (ExtensibleUnion fs a) Source # (\|+\|:) :: forall f a r (fs :: [Instruction]). (f a -> r) -> (ExtensibleUnion fs a -> r) -> ExtensibleUnion (f ': fs) a -> r Source # inject0 :: forall (f :: Type -> Type) (fs :: [Type -> Type]). f ~> ExtensibleUnion (f ': fs) Source # injectUnder :: forall (f2 :: Type -> Type) (f1 :: Type -> Type) (fs :: [Type -> Type]). f2 ~> ExtensibleUnion (f1 ': (f2 ': fs)) Source # injectUnder2 :: forall (f3 :: Type -> Type) (f1 :: Type -> Type) (f2 :: Type -> Type) (fs :: [Type -> Type]). f3 ~> ExtensibleUnion (f1 ': (f2 ': (f3 ': fs))) Source # injectUnder3 :: forall (f4 :: Type -> Type) (f1 :: Type -> Type) (f2 :: Type -> Type) (f3 :: Type -> Type) (fs :: [Type -> Type]). f4 ~> ExtensibleUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source # weaken :: forall (fs :: [Instruction]) a (f :: Instruction). ExtensibleUnion fs a -> ExtensibleUnion (f ': fs) a Source # weaken2 :: forall (fs :: [Instruction]) a (f1 :: Instruction) (f2 :: Instruction). ExtensibleUnion fs a -> ExtensibleUnion (f1 ': (f2 ': fs)) a Source # weaken3 :: forall (fs :: [Instruction]) a (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction). ExtensibleUnion fs a -> ExtensibleUnion (f1 ': (f2 ': (f3 ': fs))) a Source # weaken4 :: forall (fs :: [Instruction]) a (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (f4 :: Instruction). ExtensibleUnion fs a -> ExtensibleUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) a Source # weakenUnder :: forall (f1 :: Instruction) (fs :: [Instruction]) (f2 :: Instruction). ExtensibleUnion (f1 ': fs) ~> ExtensibleUnion (f1 ': (f2 ': fs)) Source # weakenUnder2 :: forall (f1 :: Instruction) (f2 :: Instruction) (fs :: [Instruction]) (f3 :: Instruction). ExtensibleUnion (f1 ': (f2 ': fs)) ~> ExtensibleUnion (f1 ': (f2 ': (f3 ': fs))) Source # weakenUnder3 :: forall (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]) (f4 :: Instruction). ExtensibleUnion (f1 ': (f2 ': (f3 ': fs))) ~> ExtensibleUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source # weaken2Under :: forall (f1 :: Instruction) (fs :: [Instruction]) (f2 :: Instruction) (f3 :: Instruction). ExtensibleUnion (f1 ': fs) ~> ExtensibleUnion (f1 ': (f2 ': (f3 ': fs))) Source # weaken2Under2 :: forall (f1 :: Instruction) (f2 :: Instruction) (fs :: [Instruction]) (f3 :: Instruction) (f4 :: Instruction). ExtensibleUnion (f1 ': (f2 ': fs)) ~> ExtensibleUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source # weaken3Under :: forall (f1 :: Instruction) (fs :: [Instruction]) (f2 :: Instruction) (f3 :: Instruction) (f4 :: Instruction). ExtensibleUnion (f1 ': fs) ~> ExtensibleUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source # flipUnion :: forall (f1 :: Instruction) (f2 :: Instruction) (fs :: [Instruction]). ExtensibleUnion (f1 ': (f2 ': fs)) ~> ExtensibleUnion (f2 ': (f1 ': fs)) Source # flipUnion3 :: forall (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]). ExtensibleUnion (f1 ': (f2 ': (f3 ': fs))) ~> ExtensibleUnion (f3 ': (f2 ': (f1 ': fs))) Source # flipUnionUnder :: forall (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]). ExtensibleUnion (f1 ': (f2 ': (f3 ': fs))) ~> ExtensibleUnion (f1 ': (f3 ': (f2 ': fs))) Source # rot3 :: forall (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]). ExtensibleUnion (f1 ': (f2 ': (f3 ': fs))) ~> ExtensibleUnion (f2 ': (f3 ': (f1 ': fs))) Source # rot3' :: forall (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]). ExtensibleUnion (f1 ': (f2 ': (f3 ': fs))) ~> ExtensibleUnion (f3 ': (f1 ': (f2 ': fs))) Source # bundleUnion2 :: forall (u' :: [Instruction] -> Instruction) (f1 :: Instruction) (f2 :: Instruction) (fs :: [Instruction]). Union u' => ExtensibleUnion (f1 ': (f2 ': fs)) ~> ExtensibleUnion (u' '[f1, f2] ': fs) Source # bundleUnion3 :: forall (u' :: [Instruction] -> Instruction) (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]). Union u' => ExtensibleUnion (f1 ': (f2 ': (f3 ': fs))) ~> ExtensibleUnion (u' '[f1, f2, f3] ': fs) Source # bundleUnion4 :: forall (u' :: [Instruction] -> Instruction) (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (f4 :: Instruction) (fs :: [Instruction]). Union u' => ExtensibleUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) ~> ExtensibleUnion (u' '[f1, f2, f3, f4] ': fs) Source # unbundleUnion2 :: forall (u' :: [Instruction] -> Instruction) (f1 :: Instruction) (f2 :: Instruction) (fs :: [Instruction]). Union u' => ExtensibleUnion (u' '[f1, f2] ': fs) ~> ExtensibleUnion (f1 ': (f2 ': fs)) Source # unbundleUnion3 :: forall (u' :: [Instruction] -> Instruction) (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (fs :: [Instruction]). Union u' => ExtensibleUnion (u' '[f1, f2, f3] ': fs) ~> ExtensibleUnion (f1 ': (f2 ': (f3 ': fs))) Source # unbundleUnion4 :: forall (u' :: [Instruction] -> Instruction) (f1 :: Instruction) (f2 :: Instruction) (f3 :: Instruction) (f4 :: Instruction) (fs :: [Instruction]). Union u' => ExtensibleUnion (u' '[f1, f2, f3, f4] ': fs) ~> ExtensibleUnion (f1 ': (f2 ': (f3 ': (f4 ': fs)))) Source #
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 #

type family IsMember (f :: Instruction) fs where ... Source #

Equations

IsMember f (f ': fs) = 'True
IsMember f (_ ': fs) = IsMember f fs
IsMember _ '[] = 'False

type Member u f fs = (HasMembership u f fs, IsMember f fs ~ 'True) Source #