{-# LANGUAGE TupleSections #-}
{-@ LIQUID "--no-warnings" @-}
{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--diff" @-}
{-@ LIQUID "--higherorder" @-}
{-@ LIQUID "--exactdc" @-}
{-@ LIQUID "--automatic-instances=liquidinstanceslocal" @-}
module MapReduce where
import Prelude hiding (mconcat, map, split, take, drop, sum, (++))
import Language.Haskell.Liquid.ProofCombinators
map :: (a -> b) -> List a -> List b
sumEq :: Int -> List Int -> Proof
appendAssoc, appendAssocAuto :: List a -> List a -> List a -> Proof
plusRightId :: List Int -> Proof
sumDistr :: List Int -> List Int -> Proof
mRTheorem :: Int -> (List a -> b) -> (b -> b -> b)
-> (List a -> Proof)
-> (List a -> List a -> Proof)
-> List a -> Proof
appendTakeDrop :: Int -> List a -> Proof
llen :: List a -> Int
{-@ infix ++ @-}
(++) :: List a -> List a -> List a
drop :: Int -> List a -> List a
take :: Int -> List a -> List a

{-@ reflect mapReduce @-}
mapReduce :: Int -> (List a -> b) -> (b -> b -> b) -> List a -> b
mapReduce n f op is = reduce op (f N) (map f (chunk n is))
{-@ reflect reduce @-}
reduce :: (a -> a -> a) -> a -> List a -> a
reduce op b N = b
reduce op b (C x xs) = op x (reduce op b xs)
{-@ reflect map @-}
{-@ map :: (a -> b) -> xs:List a -> {v:List b | llen v == llen xs } @-}
map _ N = N
map f (C x xs) = f x `C` map f xs
{-@ reflect chunk @-}
chunk :: Int -> List a -> List (List a)

{-@ reflect sum @-}
sum :: List Int -> Int
sum N = 0
sum (C x xs) = x `plus` sum xs
{-@ reflect plus @-}
plus :: Int -> Int -> Int
plus x y = x + y
{-@ reflect psum @-}
psum :: Int -> List Int -> Int
psum n is = mapReduce n sum plus is

**Question:** Is `psum`

equivalent to `sum`

?

{-@ automatic-instances sumEq @-}
{-@ sumEq :: n:Int -> is:List Int -> { sum is == psum n is } @-}
sumEq n is = mRTheorem n -- chunk size
sum -- function to map-reduce
plus -- reduction operator
plusRightId -- plus has "right-identity"
sumDistr -- sum is "distributive"
is -- input list

`plus`

```
{-@ sumDistr :: xs:List Int -> ys:List Int ->
{sum (xs ++ ys) == plus (sum xs) (sum ys)} @-}
{-@ plusRightId :: xs:List Int ->
{plus (sum xs) (sum N) == sum xs} @-}
```

If f is right-id and op distributes ...

... then it is OK to map-reduce.

{-@ mRTheorem :: n:Int -> f:(List a -> b) -> op:(b -> b -> b)
-> rightId:(xs:List a -> {op (f xs) (f N) == f xs } )
-> distrib:(xs:List a -> ys:List a
-> {f (xs ++ ys) == op (f xs) (f ys)} )
-> is:List a
-> { mapReduce n f op is == f is }
/ [llen is]
@-}

Lets prove Right Identity

{-@ plusRightId :: xs:List Int ->
{plus (sum xs) (sum N) == sum xs} @-}
plusRightId xs
= undefined

- Lets prove Associativity of append

{-@ appendAssoc :: xs:List a -> ys:List a -> zs:List a
-> { xs ++ (ys ++ zs) == (xs ++ ys) ++ zs } @-}
appendAssoc xs ys zs = undefined

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

{-@ automatic-instances appendAssocAuto @-}
{-@ appendAssocAuto :: xs:List a -> ys:List a -> zs:List a
-> { xs ++ (ys ++ zs) == (xs ++ ys) ++ zs } @-}
appendAssocAuto N _ _ = trivial
appendAssocAuto (C _ xs) ys zs = appendAssocAuto xs ys zs

- Lets prove distribution

{-@ automatic-instances sumDistr @-}
{-@ sumDistr :: xs:List Int -> ys:List Int -> {sum (xs ++ ys) == plus (sum xs) (sum ys)} @-}
sumDistr xs ys = undefined

**Refinement Reflection:**Allow Haskell functions in Logic**Case Study:**Prove Program Equivalence

Prove crucial properties **for** Haskell **in** Haskell!

where Haskell = a general purspose programming language.

**Refinements:**Types + Predicates**Automation:**SMT Implication**Measures:**Specify Properties of Data**Termination:**Semantic Termination Checking**Reflection:**Allow Haskell functions in Logic!**Case Study:**Prove Program Equivalence

`cabal install liquidhaskell`

https://github.com/ucsd-progsys/liquidhaskell

`http://www.refinement-types.org`

online demo @ http://goto.ucsd.edu/liquidhaskell

mRTheorem n f op rightId _ N
= mapReduce n f op N
==. reduce op (f N) (map f (chunk n N))
==. reduce op (f N) (map f (C N N))
==. reduce op (f N) (f N `C` map f N )
==. reduce op (f N) (f N `C` N)
==. op (f N) (reduce op (f N) N)
==. op (f N) (f N)
? rightId N
==. f N
*** QED
mRTheorem n f op rightId _ is@(C _ _)
| n <= 1 || llen is <= n
= mapReduce n f op is
==. reduce op (f N) (map f (chunk n is))
==. reduce op (f N) (map f (C is N))
==. reduce op (f N) (f is `C` map f N)
==. reduce op (f N) (f is `C` N)
==. op (f is) (reduce op (f N) N)
==. op (f is) (f N)
==. f is
? rightId is
*** QED
mRTheorem n f op rightId distrib is
= mapReduce n f op is
==. reduce op (f N) (map f (chunk n is))
==. reduce op (f N) (map f (C (take n is) (chunk n (drop n is))))
==. reduce op (f N) (C (f (take n is)) (map f (chunk n (drop n is))))
==. op (f (take n is)) (reduce op (f N) (map f (chunk n (drop n is))))
==. op (f (take n is)) (mapReduce n f op (drop n is))
==. op (f (take n is)) (f (drop n is))
? mRTheorem n f op rightId distrib (drop n is)
==. f ((take n is) ++ (drop n is))
? distrib (take n is) (drop n is)
==. f is
? appendTakeDrop n is
*** QED

{-@ appendTakeDrop :: i:Nat -> xs:{List a | i <= llen xs} ->
{xs == (take i xs) ++ (drop i xs) } @-}
appendTakeDrop i N
= (take i N) ++ (drop i N)
==. N ++ N
==. N
*** QED
appendTakeDrop i (C x xs)
| i == 0
= (take 0 (C x xs)) ++ (drop 0 (C x xs))
==. N ++ (C x xs)
==. C x xs
*** QED
| otherwise
= (take i (C x xs)) ++ (drop i (C x xs))
==. (C x (take (i-1) xs)) ++ (drop (i-1) xs)
==. C x ( (take (i-1) xs) ++ (drop (i-1) xs))
==. C x xs ? appendTakeDrop (i-1) xs
*** QED

Built-in Lists are not supported for now.

(So does imports...)

{-@ data List [llen] a = N | C {lhead :: a, ltail :: List a} @-}
data List a = N | C a (List a)
{-@ measure llen @-}
{-@ llen :: List a -> Nat @-}
llen N = 0
llen (C _ xs) = 1 + llen xs

{-@ chunk :: i:Int -> xs:List a
-> {v:List (List a) | if (i <= 1 || llen xs <= i) then (llen v == 1) else (llen v < llen xs) }
/ [llen xs] @-}
chunk i xs
| i <= 1
= C xs N
| llen xs <= i
= C xs N
| otherwise
= C (take i xs) (chunk i (drop i xs))
{-@ reflect drop @-}
{-@ drop :: i:Nat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == llen xs - i } @-}
drop i N = N
drop i (C x xs)
| i == 0
= C x xs
| otherwise
= drop (i-1) xs
{-@ reflect take @-}
{-@ take :: i:Nat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == i} @-}
take i N = N
take i (C x xs)
| i == 0
= N
| otherwise
= C x (take (i-1) xs)
{-@ reflect ++ @-}
N ++ ys = ys
(C x xs) ++ ys = x `C` (xs ++ ys)