HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

Modulesop-core-0.5.0.2Haskell2010

Data.SOP.NS

n-ary sums (and sums of products)

  • 4 types
  • 66 values
  • Packagesop-core-0.5.0.2
  • Exports70
  • LanguageHaskell2010
  • LicenceBSD-3-Clause
  • SourceNS.hs

Datatypes

3 declarations
datadata NS (a :: k -> Type) (b :: [k]) where
#

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 ]

Constructors

  • Z :: a x -> NS a (x ': xs)
  • S :: NS a xs -> NS a (x ': xs)
Instances17HTrans, HAp, HApInjs, HCollapse, HExpand, HIndex, …
  • HTrans NS NSDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HAp NSDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HApInjs NSDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HCollapse NSDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HExpand NSDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HIndex NSDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HSequence NSDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HTraverse_ NSDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • All (Compose Eq f) xs => Eq (NS f xs)Defined in sop-core-0.5.0.2 · Data.SOP.NS
  • (All (Compose Eq f) xs, All (Compose Ord f) xs) => Ord (NS f xs)Defined in sop-core-0.5.0.2 · Data.SOP.NS
  • All (Compose Show f) xs => Show (NS f xs)Defined in sop-core-0.5.0.2 · Data.SOP.NS
  • All (Compose NFData f) xs => NFData (NS f xs)Defined in sop-core-0.5.0.2 · Data.SOP.NS
  • type CollapseTo NS a = aDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • type Prod NS = NPDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • type AllN NS c = All cDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • type Same NS = NSDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • type SListIN NS = SListIDefined in sop-core-0.5.0.2 · Data.SOP.NS
newtypenewtype SOP (f :: k -> Type) (xss :: [[k]])
#

A sum of products.

This is a newtype for an NS of an NP. The elements of the (inner) products are applications of the parameter f. The type SOP is indexed by the list of lists that determines the sizes of both the (outer) sum and all the (inner) products, as well as the types of all the elements of the inner products.

A SOP I reflects the structure of a normal Haskell datatype. The sum structure represents the choice between the different constructors, the product structure represents the arguments of each constructor.

Constructors

Instances17HTrans, HAp, HApInjs, HCollapse, HExpand, HIndex, …
  • HTrans SOP SOPDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HAp SOPDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HApInjs SOPDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HCollapse SOPDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HExpand SOPDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HIndex SOPDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HSequence SOPDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • HTraverse_ SOPDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • Eq (NS (NP f) xss) => Eq (SOP f xss)Defined in sop-core-0.5.0.2 · Data.SOP.NS
  • Ord (NS (NP f) xss) => Ord (SOP f xss)Defined in sop-core-0.5.0.2 · Data.SOP.NS
  • Show (NS (NP f) xss) => Show (SOP f xss)Defined in sop-core-0.5.0.2 · Data.SOP.NS
  • NFData (NS (NP f) xss) => NFData (SOP f xss)Defined in sop-core-0.5.0.2 · Data.SOP.NS
  • type CollapseTo SOP a = [a]Defined in sop-core-0.5.0.2 · Data.SOP.NS
  • type Prod SOP = POPDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • type AllN SOP c = All2 cDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • type Same SOP = SOPDefined in sop-core-0.5.0.2 · Data.SOP.NS
  • type SListIN SOP = SListI2Defined in sop-core-0.5.0.2 · Data.SOP.NS
valueunSOP :: SOP f xss -> NS (NP f) xss
#

Unwrap a sum of products.

Constructing sums

8 declarations
typetype Injection (f :: k -> Type) (xs :: [k]) = f -.-> K (NS f xs)
#

The type of injections into an n-ary sum.

If you expand the type synonyms and newtypes involved, you get

Injection f xs a = (f -.-> K (NS f xs)) a ~= f a -> K (NS f xs) a ~= f a -> NS f xs

If we pick a to be an element of xs, this indeed corresponds to an injection into the sum.

valueinjections :: SListI xs => NP (Injection f xs) xs
#

Compute all injections into an n-ary sum.

Each element of the resulting product contains one of the injections.

valueshift :: Injection f xs a2 -> Injection f (x ': xs) a2
#

Deprecated. Use shiftInjection instead.

Shift an injection.

Given an injection, return an injection into a sum that is one component larger.

valueshiftInjection :: Injection f xs a2 -> Injection f (x ': xs) a2
#

Shift an injection.

Given an injection, return an injection into a sum that is one component larger.

valueapInjs_NP :: SListI xs => NP f xs -> [NS f xs]
#

Apply injections to a product.

Given a product containing all possible choices, produce a list of sums by applying each injection to the appropriate element.

Example:

Example1 expression
apInjs_NP (I 'x' :* I True :* I 2 :* Nil)[Z (I 'x'),S (Z (I True)),S (S (Z (I 2)))]
valueapInjs'_NP :: SListI xs => NP f xs -> NP (K (NS f xs)) xs
#

apInjs_NP without hcollapse.

Example1 expression
apInjs'_NP (I 'x' :* I True :* I 2 :* Nil)K (Z (I 'x')) :* K (S (Z (I True))) :* K (S (S (Z (I 2)))) :* Nil
valueapInjs_POP :: SListI xss => POP f xss -> [SOP f xss]
#

Apply injections to a product of product.

This operates on the outer product only. Given a product containing all possible choices (that are products), produce a list of sums (of products) by applying each injection to the appropriate element.

Example:

Example1 expression
apInjs_POP (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil))[SOP (Z (I 'x' :* Nil)),SOP (S (Z (I True :* I 2 :* Nil)))]
valueapInjs'_POP :: SListI xss => POP f xss -> NP (K (SOP f xss)) xss
#

apInjs_POP without hcollapse.

Example:

Example1 expression
apInjs'_POP (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil))K (SOP (Z (I 'x' :* Nil))) :* K (SOP (S (Z (I True :* I 2 :* Nil)))) :* Nil

Destructing sums

6 declarations
valueunZ :: NS f '[x] -> f x
#

Extract the payload from a unary sum.

For larger sums, this function would be partial, so it is only provided with a rather restrictive type.

Example:

Example1 expression
unZ (Z (I 'x'))I 'x'
valueindex_NS :: NS f xs -> Int
#

Obtain the index from an n-ary sum.

An n-nary sum represents a choice between n different options. This function returns an integer between 0 and n - 1 indicating the option chosen by the given value.

Examples:

Example2 expressions
index_NS (S (S (Z (I False))))2index_NS (Z (K ()))0
valueindex_SOP :: SOP f xs -> Int
#

Obtain the index from an n-ary sum of products.

An n-nary sum represents a choice between n different options. This function returns an integer between 0 and n - 1 indicating the option chosen by the given value.

Specification:

index_SOP = index_NS . unSOP

Example:

Example1 expression
index_SOP (SOP (S (Z (I True :* I 'x' :* Nil))))1
typetype Ejection (f :: k -> Type) (xs :: [k]) = K (NS f xs) -.-> (Maybe :.: f)
#

The type of ejections from an n-ary sum.

An ejection is the pattern matching function for one part of the n-ary sum.

It is the opposite of an Injection.

valueejections :: SListI xs => NP (Ejection f xs) xs
#

Compute all ejections from an n-ary sum.

Each element of the resulting product contains one of the ejections.

Application

2 declarations

Lifting / mapping

12 declarations
valuecliftA_NS
  1. :: All c xs
  2. => proxy c
  3. -> forall (a :: k). c a => f a -> g a
  4. -> NS f xs
  5. -> NS g xs
#

Specialization of hcliftA.

valuecliftA2_NS
  1. :: All c xs
  2. => proxy c
  3. -> forall (a :: k). c a => f a -> g a -> h a
  4. -> NP f xs
  5. -> NS g xs
  6. -> NS h xs
#

Specialization of hcliftA2.

valuemap_NS :: SListI xs => (forall (a :: k). f a -> g a) -> NS f xs -> NS g xs
#

Specialization of hmap, which is equivalent to hliftA.

valuecmap_NS
  1. :: All c xs
  2. => proxy c
  3. -> forall (a :: k). c a => f a -> g a
  4. -> NS f xs
  5. -> NS g xs
#

Specialization of hcmap, which is equivalent to hcliftA.

valuecmap_SOP
  1. :: All2 c xss
  2. => proxy c
  3. -> forall (a :: k). c a => f a -> g a
  4. -> SOP f xss
  5. -> SOP g xss
#

Specialization of hcmap, which is equivalent to hcliftA.

Dealing with All c

1 declaration

Comparison

4 declarations
valuecompare_NS
  1. :: r

    what to do if first is smaller

  2. -> (forall (x :: k). f x -> g x -> r)

    what to do if both are equal

  3. -> r

    what to do if first is larger

  4. -> NS f xs
  5. -> NS g xs
  6. -> r
#

Compare two sums with respect to the choice they are making.

A value that chooses the first option is considered smaller than one that chooses the second option.

If the choices are different, then either the first (if the first is smaller than the second) or the third (if the first is larger than the second) argument are called. If both choices are equal, then the second argument is called, which has access to the elements contained in the sums.

valueccompare_NS
  1. :: All c xs
  2. => proxy c
  3. -> r

    what to do if first is smaller

  4. -> (forall (x :: k). c x => f x -> g x -> r)

    what to do if both are equal

  5. -> r

    what to do if first is larger

  6. -> NS f xs
  7. -> NS g xs
  8. -> r
#

Constrained version of compare_NS.

valuecompare_SOP
  1. :: r

    what to do if first is smaller

  2. -> (forall (xs :: [k]). NP f xs -> NP g xs -> r)

    what to do if both are equal

  3. -> r

    what to do if first is larger

  4. -> SOP f xss
  5. -> SOP g xss
  6. -> r
#

Compare two sums of products with respect to the choice in the sum they are making.

Only the sum structure is used for comparison. This is a small wrapper around ccompare_NS for a common special case.

valueccompare_SOP
  1. :: All2 c xss
  2. => proxy c
  3. -> r

    what to do if first is smaller

  4. -> (forall (xs :: [k]). All c xs => NP f xs -> NP g xs -> r)

    what to do if both are equal

  5. -> r

    what to do if first is larger

  6. -> SOP f xss
  7. -> SOP g xss
  8. -> r
#

Constrained version of compare_SOP.

Collapsing

2 declarations

Folding and sequencing

16 declarations

Catamorphism and anamorphism

4 declarations
valuecata_NS
  1. :: forall (y :: k) (ys :: [k]). f y -> r (y ': ys)
  2. -> forall (y :: k) (ys :: [k]). r ys -> r (y ': ys)
  3. -> NS f xs
  4. -> r xs
#

Catamorphism for NS.

Takes arguments determining what to do for Z and what to do for S. The result type is still indexed over the type-level lit.

valueccata_NS
  1. :: All c xs
  2. => proxy c
  3. -> forall (y :: k) (ys :: [k]). c y => f y -> r (y ': ys)
  4. -> forall (y :: k) (ys :: [k]). c y => r ys -> r (y ': ys)
  5. -> NS f xs
  6. -> r xs
#

Constrained catamorphism for NS.

valueana_NS
  1. :: SListI xs
  2. => forall r. s '[] -> r
  3. -> forall (y :: k) (ys :: [k]). s (y ': ys) -> Either (f y) (s ys)
  4. -> s xs
  5. -> NS f xs
#

Anamorphism for NS.

valuecana_NS
  1. :: All c xs
  2. => proxy c
  3. -> forall r. s '[] -> r
  4. -> forall (y :: k) (ys :: [k]). c y => s (y ': ys) -> Either (f y) (s ys)
  5. -> s xs
  6. -> NS f xs
#

Constrained anamorphism for NS.

Expanding sums to products

4 declarations

Transformation of index lists and coercions

8 declarations
valuetrans_NS
  1. :: AllZip c xs ys
  2. => proxy c
  3. -> forall (x :: k1) (y :: k2). c x y => f x -> g y
  4. -> NS f xs
  5. -> NS g ys
#

Specialization of htrans.

valuetrans_SOP
  1. :: AllZip2 c xss yss
  2. => proxy c
  3. -> forall (x :: k1) (y :: k2). c x y => f x -> g y
  4. -> SOP f xss
  5. -> SOP g yss
#

Specialization of htrans.