ClassLaws

Laws for the type classes in par-classes and par-collections

Par-collections

• TBD

Par-classes

Mandatory laws for ParFuture

This refers to a new version (2015.07) of ParFuture where spawn/read/Future are completely separate from new/put/get/IVar.

• spawn reordering

(do x <- spawn f; y <- spawn g; m) == 
(do y <- spawn g; x <- spawn f; m)

(This law also holds for IVars + fork.)

• spawn/read identity

(spawn m >>= read)  == m

Optional laws for ParFuture monads

• Speculative-only futures, which reveal divergence/exceptions only when reading the futures.

-- Here are values whose WHNF is not bottom, but create bottom when run:
loop = return () >> loop
err = return () >> undefined

(spawn loop >> m) == m
(spawn err >> m) == m

My proposal is that this is modeled by a ForgettableFutures class, and conversely an UnforgettableFutures. A given monad can only be a member of at most one. The first implies the law above, and the latter implies that:

(spawn loop >> m) == loop || OtherError
(spawn err >> m) == err || OtherError

• Idempotence for all actions in the monad. This can be modeled in general by IdempotentMonad or IdempotentParMonad. (which?)

(m >> m) == m

Mandatory laws for ParIVar

• Non-speculative fork - the "speculative spawn" optional law above specifically does not hold for IVars + fork.

(fork err >> m)  == err  || OtherError
(fork loop >> m) == loop || OtherError

This is absolutely required so that multiple put exceptions are flushed out deterministically. Premature exiting of a computation based on the "main thread" completing is tantamount to nondeterministic cancelation of everything left running.

• Idempotence - in this case, the class that marks idempotence can also carry extra methods which include the Eq-requiring variant of put. That is, IdempotentParIVar could be a subclass of both ParIVar and IdempotentParMonad, which both notes the property and adds the extra method(s).

Optional laws for ParIVar monads

• Fully parallel - side effecting computations can be run in parallel to the same effect.

 (m1 >> m2) == (fork m1 >> m2)

This is modeled by the ParThreadSafe class already. Notably, the ParST transformer requires ParThreadSafe of its underlying monad, but itself does not exhibit this property.