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
{-@ 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
Hidden Haskell types :)
parallelismEq :: RightId (L b) -> (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
chunk :: Int -> L a -> L (L a)
drop :: Int -> L a -> L a
take :: Int -> L a -> L a
length :: L a -> Int