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

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)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX














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 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX



This proof is boring! Please automate it!

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














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

and a proof for append right identity.

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














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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX








































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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX














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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX














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)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX














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)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX














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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX














Parallelizing mapping

We parallelize mapping using Control.Parallel.Strategies

{-@ reflect pmap @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Where withStrategy is assumed to be identity.

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














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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX














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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX





































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 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX