Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
, 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.K
a
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) | |
HAp (NS :: (k -> Type) -> [k] -> Type) | |
HCollapse (NS :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NS | |
HTraverse_ (NS :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NS 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 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 | |
HApInjs (NS :: (k -> Type) -> [k] -> Type) | |
HExpand (NS :: (k -> Type) -> [k] -> Type) | |
ShowHO f => ShowHO (NS f :: [k] -> Type) Source # | Since: 2.3.0 |
EqHO f => EqHO (NS f :: [k] -> Type) Source # | Since: 2.3.0 |
All (Compose Eq f) xs => Eq (NS f xs) | |
(All (Compose Eq f) xs, All (Compose Ord f) xs) => Ord (NS f xs) | |
All (Compose Show f) xs => Show (NS f xs) | |
All (Compose NFData f) xs => NFData (NS f xs) | Since: sop-core-0.2.5.0 |
Defined in Data.SOP.NS | |
type Same (NS :: (k1 -> Type) -> [k1] -> Type) | |
type Prod (NS :: (k -> Type) -> [k] -> Type) | |
type CollapseTo (NS :: (k -> Type) -> [k] -> Type) a | |
Defined in Data.SOP.NS | |
type SListIN (NS :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NS | |
type AllN (NS :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint) | |
Defined in Data.SOP.NS |
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
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
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.