Sum -package:bifunctors
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
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
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.