Sum -package:base

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.

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}

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

Functions for summing floating point numbers more accurately than the naive sum function and its counterparts in the vector package and elsewhere. When used with floating point numbers, in the worst case, the sum function accumulates numeric error at a rate proportional to the number of values being summed. The algorithms in this module implement different methods of /compensated summation/, which reduce the accumulation of numeric error so that it either grows much more slowly than the number of inputs (e.g. logarithmically), or remains constant.

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

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

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.