Parallelism Equivalence of Morphisms

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

chunk :: Int -> L a -> L (L a) mconcat :: L (L a) -> L a pmap :: (a -> b) -> L a -> L b pmap f xs = withStrategy parStrategy (map f xs) {-@ assume withStrategy :: Strategy a -> x:a -> {v:a | v = x} @-}

For parallelism we use Control.Parallel.Strategies.withStrategy encoded in the logic as an identity.

What about the rest of the recursive functions?














Lifting Haskell functions in the logic

Example: reflecting take.

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














Warming up proof

Our first recursive proof using combinators from Language.Haskell.Liquid.ProofCombinators.

{-@ takeDropProp :: i:Nat -> xs:{L a | i <= length xs } -> {xs == take i xs <> drop i xs } @-} takeDropProp i xs | i == 0 = error "Define me!" 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! Please automate it!

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














Parallelism Equivalence: Setup

Let's define type aliases for morphism

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

and a proof for append right identity.

{-@ rightIdProp :: xs:L a -> { xs <> N == xs } @-}














Parallelism Equivalence

The proof is simply a recursive Haskell function!

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








































List Definition

We start with the classic 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.

STAY

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 } @-} {-@ chunk :: i:Pos -> xs:L a -> L (L a) / [length xs] @-} {-@ reflect chunk @-} 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.

{-@ 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.

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 @-}

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 N = N mconcat (C x xs) = x <> mconcat xs





































Hidden Haskell types :)
parallelismEq :: (L a -> L b) -> Morphism a b ->L a -> Int -> Proof type RightId a = a -> Proof type Morphism a b = L a -> L a -> Proof takeDropProp :: Int -> L a -> Proof drop :: Int -> L a -> L a take :: Int -> L a -> L a length :: L a -> Int rightIdProp :: L a -> Proof rightIdProp _ = undefined