Goal 0.2: parallel fold

[rrnewton]

After 0.1 is finished, we will be mapping over a concurrent set. We can then extend that to perform a parallel reduction with the contents of the output set.

Parallel fold will need to take a proof of associativity.

[rrnewton]

Vikraman has been working on this recently, getting VerifiedSemigroup and VerifiedMonoid working.

The way this is implemented brings back up issues of performance. I think we need to RUN our benchmarks, not just report how many lines of code were added for verification.

[rrnewton]

In @vikraman's work, he has been aiming to get products of monoids working, to demonstrate composability. This is not critical, but it is nice.

[vikraman]

There is one extra level of indirection that could possibly be eliminated. Since type families are not injective, it's data Verified Eq a instead of type Verified Eq a. @RyanGlScott thinks ghc 8.0 can get you injective type families using TypeFamilyDependencies.

[RyanGlScott]

As it turns out, we can "fake" TypeFamilyDependencies using newtype instances, so at least that indirection won't be a problem.