# Parallelism Equivalence of Morphisms

Lets prove that f x == mconcat (pmap f (chunk i x)) in Haskell!

module Parallelism where {-@ LIQUID "--exactdc" @-} {-@ LIQUID "--higherorder" @-} import Prelude hiding (length, (<>), drop, take, chunk, map, mconcat) import Language.Haskell.Liquid.ProofCombinators import Control.Parallel.Strategies

## List Definition

refined with a length termination annotation.

data L a = N | C {hd :: a, tl :: L a} {-@ data L [length] a = N | C {hd :: a, tl :: L a} @-} {-@ measure length @-} {-@ length :: L a -> Nat @-} length N = 0 length (C x xs) = 1 + length xs

## List chunking

List chunking uses the standard take and drop functions.

{-@ reflect take @-} {-@ take :: i:Nat -> xs:{L a | i <= length xs} -> L a @-} take i xs | i == 0 = N take i (C x xs) = C x (take (i-1) xs)

Note: We need to make take total!

## List dropping

Similarly we define a total drop function.

{-@ reflect drop @-} {-@ drop :: i:Nat -> xs:{L a | i <= length xs} -> {v:L a | length v == length xs - i} @-} drop i xs | i == 0 = xs drop i (C x xs) = drop (i-1) xs

## List chunking

We use take and drop to define chunk.

{-@ type Pos = {v:Int | 0 < v } @-} {-@ reflect chunk @-} {-@ chunk :: i:Pos -> xs:L a -> L (L a) / [length xs] @-} chunk i xs | length xs <= i = C xs N | otherwise = take i xs C chunk i (drop i xs)

## Getting ready for our first theorem!

Appending take and drop exactly reconstuct the list.

{-@ infixr <> @-} {-@ reflect <> @-} (<>) :: L a -> L a -> L a N <> ys = ys (C x xs) <> ys = C x (xs <> ys)

## Proving take and drop reconstruction

Define an inductive proof term, ... following the structure of take and drop.

{-@ takeDropProp :: i:Nat -> xs:{L a | i <= length xs } -> {xs == take i xs <> drop i xs } @-} takeDropProp i xs | i == 0 = take i xs <> drop i xs ==. N <> xs ==. xs *** QED takeDropProp i (C x xs) = take i (C x xs) <> drop i (C x xs) ==. C x (take (i-1) xs) <> drop (i-1) xs ==. C x xs ? takeDropProp (i-1) xs *** QED

This proof is boring!

{-@ LIQUID "--automatic-instances=liquidinstances" @-}

## Step 2: Parallel mapping

GOAL: f x == mconcat (pmap f (chunk i x))

First, we define list mapping.

{-@ reflect map @-} map :: (a -> b) -> L a -> L b map _ N = N map f (C x xs) = f x C map f xs

## Parallelizing mapping

We parallelize mapping using Control.Parallel.Strategies

{-@ reflect pmap @-} pmap :: (a -> b) -> L a -> L b pmap f xs = withStrategy parStrategy (map f xs)

Where withStrategy is assumed to be identity.

{-@ assume withStrategy :: Strategy a -> x:a -> {v:a | v = x} @-}

## Runtime parallelism

Runtime parallelization does not affect the proof and is the classic haskell code.

parStrategy :: Strategy (L a) parStrategy = parTraversable rseq instance Functor L where fmap f N = N fmap f (C x xs) = f x C fmap f xs instance Foldable L where instance Traversable L where traverse f N = pure N traverse f (C x xs) = C <\$> f x <*> traverse f xs

## Step 3: Concatenating the result

GOAL: f x == mconcat (pmap f (chunk i x))

Finally, lets concatenate the result!

{-@ reflect mconcat @-} mconcat :: L (L a) -> L a mconcat N = N mconcat (C x xs) = x <> mconcat xs

## Parallelism Equivalence

Let's define type aliases for morphism and right identity.

{-@ type Morphism a b F = x:(L a) -> y:(L a) -> {F N = N && F (x <> y) = F x <> F y} @-} {-@ type RightId a = xs:a -> { xs <> N == xs } @-}

## Parallelism Equivalence

The proof is simply a recursive Haskell function!

{-@ parallelismEq :: RightId (L b) -> f:(L a -> L b) -> Morphism a b f -> x:L a -> i:Pos -> {f x == mconcat (pmap f (chunk i x))} @-} parallelismEq rightIdProp f morphismProp x i | length x <= i = rightIdProp (f x) parallelismEq rightIdProp f morphismProp x i = parallelismEq rightIdProp f morphismProp (drop i x) i &&& morphismProp (take i x) (drop i x) &&& takeDropProp i x