generics-mrsop-2.3.0: Generic Programming with Mutually Recursive Sums of Products.

Generics.MRSOP.Base.NS

Contents

Description

Standard representation of n-ary sums.

Synopsis
• data NS (a :: k -> Type) (b :: [k]) :: forall k. (k -> Type) -> [k] -> Type
• pattern Here :: forall k (a :: k -> *) (b :: [k]). () => forall (x :: k) (xs :: [k]). b ~ (x ': xs) => a x -> NS a b
• pattern There :: forall k (a :: k -> *) (b :: [k]). () => forall (xs :: [k]) (x :: k). b ~ (x ': xs) => NS a xs -> NS a b
• mapNS :: (f :-> g) -> NS f ks -> NS g ks
• mapNSM :: Monad m => (forall x. f x -> m (g x)) -> NS f ks -> m (NS g ks)
• elimNS :: (forall x. f x -> a) -> NS f ks -> a
• zipNS :: MonadPlus m => NS ki xs -> NS kj xs -> m (NS (ki :*: kj) xs)
• cataNS :: (forall x xs. f x -> r (x ': xs)) -> (forall x xs. r xs -> r (x ': xs)) -> NS f xs -> r xs
• eqNS :: (forall x. p x -> p x -> Bool) -> NS p xs -> NS p xs -> Bool

# 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) Instance detailsDefined in Data.SOP.NS Methodshtrans :: 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) Instance detailsDefined in Data.SOP.NS Methodshap :: Prod NS (f -.-> g) xs -> NS f xs -> NS g xs # HCollapse (NS :: (k -> Type) -> [k] -> Type) Instance detailsDefined in Data.SOP.NS Methodshcollapse :: SListIN NS xs => NS (K a) xs -> CollapseTo NS a # HTraverse_ (NS :: (k -> Type) -> [k] -> Type) Instance detailsDefined in Data.SOP.NS Methodshctraverse_ :: (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) Instance detailsDefined in Data.SOP.NS Methodshsequence' :: (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) Instance detailsDefined in Data.SOP.NS Methodshindex :: NS f xs -> Int # HApInjs (NS :: (k -> Type) -> [k] -> Type) Instance detailsDefined in Data.SOP.NS MethodshapInjs :: SListIN NS xs => Prod NS f xs -> [NS f xs] # HExpand (NS :: (k -> Type) -> [k] -> Type) Instance detailsDefined in Data.SOP.NS Methodshexpand :: 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 # ShowHO f => ShowHO (NS f :: [k] -> Type) Source # Since: 2.3.0 Instance detailsDefined in Generics.MRSOP.Base.NS MethodsshowHO :: NS f k0 -> String Source #showsPrecHO :: Int -> NS f k0 -> ShowS Source # EqHO f => EqHO (NS f :: [k] -> Type) Source # Since: 2.3.0 Instance detailsDefined in Generics.MRSOP.Base.NS MethodseqHO :: NS f k0 -> NS f k0 -> Bool Source # All (Compose Eq f) xs => Eq (NS f xs) Instance detailsDefined 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) Instance detailsDefined in Data.SOP.NS Methodscompare :: 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) Instance detailsDefined in Data.SOP.NS MethodsshowsPrec :: 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 Instance detailsDefined in Data.SOP.NS Methodsrnf :: NS f xs -> () # type Same (NS :: (k1 -> Type) -> [k1] -> Type) Instance detailsDefined in Data.SOP.NS type Same (NS :: (k1 -> Type) -> [k1] -> Type) = (NS :: (k2 -> Type) -> [k2] -> Type) type Prod (NS :: (k -> Type) -> [k] -> Type) Instance detailsDefined in Data.SOP.NS type Prod (NS :: (k -> Type) -> [k] -> Type) = (NP :: (k -> Type) -> [k] -> Type) type CollapseTo (NS :: (k -> Type) -> [k] -> Type) a Instance detailsDefined in Data.SOP.NS type CollapseTo (NS :: (k -> Type) -> [k] -> Type) a = a type SListIN (NS :: (k -> Type) -> [k] -> Type) Instance detailsDefined in Data.SOP.NS type SListIN (NS :: (k -> Type) -> [k] -> Type) = (SListI :: [k] -> Constraint) type AllN (NS :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint) Instance detailsDefined 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 Source #

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 Source #

Pattern synonym to S

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

Maps over a sum

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

Maps a monadic function over a sum

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

Eliminates a sum

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

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 Source #

Consumes a value of type NS

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

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

# Orphan instances

 ShowHO f => ShowHO (NS f :: [k] -> Type) Source # Since: 2.3.0 Instance details MethodsshowHO :: NS f k0 -> String Source #showsPrecHO :: Int -> NS f k0 -> ShowS Source # EqHO f => EqHO (NS f :: [k] -> Type) Source # Since: 2.3.0 Instance details MethodseqHO :: NS f k0 -> NS f k0 -> Bool Source #