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