Sum -package:math-functions

Sums, lifted to functors.

Lifted sum of functors.

Examples

>>> fmap (+1) (InL (Just 1))  :: Sum Maybe [] Int
InL (Just 2)

>>> fmap (+1) (InR [1, 2, 3]) :: Sum Maybe [] Int
InR [2,3,4]

Monoid under addition.

Sum a <> Sum b = Sum (a + b)

Examples

>>> Sum 1 <> Sum 2 <> mempty
Sum {getSum = 3}

>>> mconcat [ Sum n | n <- [3 .. 9]]
Sum {getSum = 42}

Sum (Left q) = 2*q
Sum (Right q) = 2*q+1

Last two are the locations of the '|' before and after the payload

Monoid under addition.

>>> getSum (Sum 1 <> Sum 2 <> mempty)
3

Monoid under group addition. Alternative to the Sum in Data.Monoid, which uses Num instead of AdditiveGroup.

Lifted sum of functors.

Magic sum operations using Generics These classes need not be instantiated manually, as GHC can automatically prove valid instances via Generics. Only the Generic class needs to be derived (see examples).

Monoid under addition.

>>> getSum (Sum 1 <> Sum 2 <> mempty)
3

TextShow instance for Sum. Since: 3

Abstraction of normed vector spaces

Sum a Nat-list.

Example

>>> :kind! Eval (Sum '[1,2,3])
Eval (Sum '[1,2,3]) :: Natural
= 6

Monoid under addition.

>>> getSum (Sum 1 <> Sum 2 <> mempty)
3

Operations on sums, combining effects into a signature.

A wrapper for an Additive which distinguishes the additive structure

Example inductive proof to show partial correctness of the traditional for-loop sum algorithm:

s = 0
i = 0
while i <= n:
s += i
i++

We prove the loop invariant and establish partial correctness that s is the sum of all numbers up to and including n upon termination.