search

iu-parfunc / verified-instances

Verified instances for parallel programming.
BSD 3-Clause "New" or "Revised" License
8 stars 5 forks source link

Goal 0.2: parallel fold #2

Open rrnewton opened 8 years ago

rrnewton commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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