Generics.MRSOP.Base.NS

Standard representation of n-ary sums.

Documentation

data NS (a :: k -> Type) (b :: [k]) :: forall k. (k -> Type) -> [k] -> Type

An n-ary sum.

The sum is parameterized by a type constructor f and indexed by a type-level list xs. The length of the list determines the number of choices in the sum and if the i-th element of the list is of type x, then the i-th choice of the sum is of type f x.

The constructor names are chosen to resemble Peano-style natural numbers, i.e., Z is for "zero", and S is for "successor". Chaining S and Z chooses the corresponding component of the sum.

Examples:

Z         :: f x -> NS f (x ': xs)
S . Z     :: f y -> NS f (x ': y ': xs)
S . S . Z :: f z -> NS f (x ': y ': z ': xs)
...

Note that empty sums (indexed by an empty list) have no non-bottom elements.

Two common instantiations of f are the identity functor I and the constant functor K. For I, the sum becomes a direct generalization of the Either type to arbitrarily many choices. For K a, the result is a homogeneous choice type, where the contents of the type-level list are ignored, but its length specifies the number of options.

In the context of the SOP approach to generic programming, an n-ary sum describes the top-level structure of a datatype, which is a choice between all of its constructors.

Examples:

Z (I 'x')      :: NS I       '[ Char, Bool ]
S (Z (I True)) :: NS I       '[ Char, Bool ]
S (Z (K 1))    :: NS (K Int) '[ Char, Bool ]

Instances

HTrans (NS :: (k1 -> Type) -> [k1] -> Type) (NS :: (k2 -> Type) -> [k2] -> Type)

Defined in Data.SOP.NS

Methods

htrans :: AllZipN (Prod NS) c xs ys => proxy c -> (forall (x :: k10) (y :: k20). c x y => f x -> g y) -> NS f xs -> NS g ys

hcoerce :: (AllZipN (Prod NS) (LiftedCoercible f g) xs ys, HTrans NS NS) => NS f xs -> NS g ys

HAp (NS :: (k -> Type) -> [k] -> Type)

Defined in Data.SOP.NS

Methods

hap :: Prod NS (f -.-> g) xs -> NS f xs -> NS g xs

HCollapse (NS :: (k -> Type) -> [k] -> Type)

Defined in Data.SOP.NS

Methods

hcollapse :: SListIN NS xs => NS (K a) xs -> CollapseTo NS a

HTraverse_ (NS :: (k -> Type) -> [k] -> Type)

Defined in Data.SOP.NS

Methods

hctraverse_ :: (AllN NS c xs, Applicative g) => proxy c -> (forall (a :: k0). c a => f a -> g ()) -> NS f xs -> g ()

htraverse_ :: (SListIN NS xs, Applicative g) => (forall (a :: k0). f a -> g ()) -> NS f xs -> g ()

HSequence (NS :: (k -> Type) -> [k] -> Type)

Defined in Data.SOP.NS

Methods

hsequence' :: (SListIN NS xs, Applicative f) => NS (f :.: g) xs -> f (NS g xs)

hctraverse' :: (AllN NS c xs, Applicative g) => proxy c -> (forall (a :: k0). c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs)

htraverse' :: (SListIN NS xs, Applicative g) => (forall (a :: k0). f a -> g (f' a)) -> NS f xs -> g (NS f' xs)

HIndex (NS :: (k -> Type) -> [k] -> Type)

Defined in Data.SOP.NS

Methods

hindex :: NS f xs -> Int

HApInjs (NS :: (k -> Type) -> [k] -> Type)

Defined in Data.SOP.NS

Methods

hapInjs :: SListIN NS xs => Prod NS f xs -> [NS f xs]

HExpand (NS :: (k -> Type) -> [k] -> Type)

Defined in Data.SOP.NS

Methods

hexpand :: SListIN (Prod NS) xs => (forall (x :: k0). f x) -> NS f xs -> Prod NS f xs

hcexpand :: AllN (Prod NS) c xs => proxy c -> (forall (x :: k0). c x => f x) -> NS f xs -> Prod NS f xs

All (Compose Eq f) xs => Eq (NS f xs)

Defined in Data.SOP.NS

Methods

(==) :: NS f xs -> NS f xs -> Bool

(/=) :: NS f xs -> NS f xs -> Bool

(All (Compose Eq f) xs, All (Compose Ord f) xs) => Ord (NS f xs)

Defined in Data.SOP.NS

Methods

compare :: NS f xs -> NS f xs -> Ordering

(<) :: NS f xs -> NS f xs -> Bool

(<=) :: NS f xs -> NS f xs -> Bool

(>) :: NS f xs -> NS f xs -> Bool

(>=) :: NS f xs -> NS f xs -> Bool

max :: NS f xs -> NS f xs -> NS f xs

min :: NS f xs -> NS f xs -> NS f xs

All (Compose Show f) xs => Show (NS f xs)

Defined in Data.SOP.NS

Methods

showsPrec :: Int -> NS f xs -> ShowS

show :: NS f xs -> String

showList :: [NS f xs] -> ShowS

All (Compose NFData f) xs => NFData (NS f xs)

Since: sop-core-0.2.5.0

Defined in Data.SOP.NS

Methods

rnf :: NS f xs -> ()

type Same (NS :: (k1 -> Type) -> [k1] -> Type)

Defined in Data.SOP.NS

type Same (NS :: (k1 -> Type) -> [k1] -> Type) = (NS :: (k2 -> Type) -> [k2] -> Type)

type Prod (NS :: (k -> Type) -> [k] -> Type)

Defined in Data.SOP.NS

type Prod (NS :: (k -> Type) -> [k] -> Type) = (NP :: (k -> Type) -> [k] -> Type)

type CollapseTo (NS :: (k -> Type) -> [k] -> Type) a

Defined in Data.SOP.NS

type CollapseTo (NS :: (k -> Type) -> [k] -> Type) a = a

type SListIN (NS :: (k -> Type) -> [k] -> Type)

Defined in Data.SOP.NS

type SListIN (NS :: (k -> Type) -> [k] -> Type) = (SListI :: [k] -> Constraint)

type AllN (NS :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint)

Defined in Data.SOP.NS

type AllN (NS :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint) = All c

pattern Here :: forall k (a :: k -> *) (b :: [k]). () => forall (x :: k) (xs :: [k]). b ~ (x ': xs) => a x -> NS a b

Pattern synonym to Z

pattern There :: forall k (a :: k -> *) (b :: [k]). () => forall (xs :: [k]) (x :: k). b ~ (x ': xs) => NS a xs -> NS a b

Pattern synonym to S

mapNS :: (f :-> g) -> NS f ks -> NS g ks

Maps over a sum

mapNSM :: Monad m => (forall x. f x -> m (g x)) -> NS f ks -> m (NS g ks)

Maps a monadic function over a sum

elimNS :: (forall x. f x -> a) -> NS f ks -> a

Eliminates a sum

zipNS :: MonadPlus m => NS ki xs -> NS kj xs -> m (NS (ki :*: kj) xs)

Combines two sums. Note that we have to fail if they are constructed from different injections.

cataNS :: (forall x xs. f x -> r (x ': xs)) -> (forall x xs. r xs -> r (x ': xs)) -> NS f xs -> r xs

Consumes a value of type NS

eqNS :: (forall x. p x -> p x -> Bool) -> NS p xs -> NS p xs -> Bool

Compares two values of type NS using the provided function in case they are made of the same injection.