Sum is:module
Sums, lifted to 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).
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.
Operations on sums, combining effects into a signature.
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.
Proof of correctness of an imperative summation algorithm, using
weakest preconditions. We investigate a few different invariants and
see how different versions lead to proofs and failures.
The
SumType data type that represents a sum type consisting of
types specified in a type-level list.
traverse over generic sum types.
Disambiguates constructors by prepending sum tags.
Note that the sum tag approach has efficiency limitations. You may
design a constructor disambiguation schema which permits
"incrementally" parsing, rather than parsing some whole thing then
comparing to each option, which will be faster. If you wish to perform
such sum tag handling yourself, but still want the free generics,
Generic.Data.FOnCstr can do this for you.
Proves sum (reverse xs) == sum xs.