Last active
December 2, 2020 04:01
-
-
Save siraben/6b1f57ff1a3fbb76432eb79f0f91f507 to your computer and use it in GitHub Desktop.
maximum mountain and derivation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE BangPatterns #-} | |
-- nix-shell --pure -i ghci -p "haskellPackages.ghcWithPackages (h: [ h.QuickCheck ])" | |
import Data.List | |
import Control.Monad | |
-- https://leetcode.com/problems/longest-mountain-in-array/ | |
data Dir = Up | Down | Flat deriving (Show) | |
ex1, ex2, ex3, ex4 :: [Int] | |
ex1 = [2, 1, 4, 7, 3, 2, 5] | |
ex2 = [2, 1, 4, 7, 3, 2, 5, 6, 7, 8, 3, 2, 1] | |
ex3 = [1, 2, 3, 4, 5, 6, 6, 6] | |
ex4 = [1, 3, 1, 4, 5, 6, 7, 8, 9, 8, 7, 6, 5] | |
-- Lists less than 3 cannot have a mountain | |
-- (aRun, dRun, prev, record, state) | |
-- Running time: O(n) (always recursing on smaller list | |
-- Space use: O(1) hopefully with strictness annotations | |
solve :: [Int] -> Int | |
solve (a : l@(_ : _ : _)) = go l (0, 0, a, 0, Flat) | |
where | |
go :: [Int] -> (Int, Int, Int, Int, Dir) -> Int | |
-- Update solution only when in Down state, as we're coming down | |
-- from a mountain that could be the largest one yet. | |
go [] (!aRun, !dRun, _, !r, Down) = max (aRun + dRun) r | |
go [] (_, _, _, !r, _) = r | |
go (curr : xs) (!aRun, !dRun, !prev, !r, Up) = go xs s' | |
where | |
s' = | |
case compare prev curr of | |
-- Up -> Up | |
LT -> (aRun + 1, dRun, curr, r, Up) | |
-- Up -> Down | |
GT -> (aRun, dRun + 1, curr, r, Down) | |
-- Up -> Flat | |
EQ -> (0, 0, curr, r, Flat) | |
go (curr : xs) (!aRun, !dRun, !prev, !r, Down) = go xs s' | |
where | |
r' = max (aRun + dRun) r | |
-- Always update solution | |
s' = | |
case compare prev curr of | |
-- Down -> Down | |
GT -> (aRun, dRun + 1, curr, r', Down) | |
-- Down -> Up | |
LT -> (2, 0, curr, r', Up) | |
-- Down -> Flat | |
EQ -> (0, 0, curr, r', Flat) | |
go (curr : xs) (_, _, !prev, !r, Flat) = go xs s' | |
where | |
s' = | |
case compare prev curr of | |
-- Flat -> Flat | |
GT -> (0, 0, curr, r, Flat) | |
-- Flat -> Up | |
LT -> (2, 0, curr, r, Up) | |
-- Flat -> Flat | |
EQ -> (0, 0, curr, r, Flat) | |
solve _ = 0 | |
-- Spec is return the length of the longest subarray which is a mountain | |
naiveSolve l | |
| length l < 3 = 0 | |
| otherwise = maximum (0:parts) | |
where | |
parts = do | |
-- For every subarray arr in l, check if mountain and return | |
-- length. | |
arr <- (tail . inits) =<< tails l | |
guard (isMountain arr) | |
pure (length arr) | |
isMountain arr = not (null $ do | |
-- arr is a mountain if length arr >= 3 | |
guard (length arr >= 3) | |
-- and there exists some i, 0 < i < length arr - 1 | |
-- (equivalent to 1 <= 1 <= length arr - 2) | |
i <- [1 .. length arr - 2] | |
let l = (arr !!) <$> [0 .. i] | |
let r = (arr !!) <$> [i .. length arr - 1] | |
-- such that arr[0..i] is ascending and arr[i..length arr - 1] | |
-- is descending | |
guard (isAscending l && isDescending r) | |
pure (length arr)) | |
isAscending l = and ((zipWith (<) <*> tail) l) | |
isDescending l = and ((zipWith (>) <*> tail) l) | |
-- Point free naive solution | |
naiveSolvePf l@(_:_:_:_) = maximum . (0:) . map length . filter isMountain . segs $ l | |
where | |
segs = concatMap tails . inits | |
isMountain l@(_:_:_:_) = any (\(l, r) -> isAscending l && isDescending r) | |
. (\l -> (\i -> (take (i + 1) l, drop i l)) <$> [1..length l - 2]) | |
$ l | |
isMountain _ = False | |
isAscending l = and ((zipWith (<) <*> tail) l) | |
isDescending l = and ((zipWith (>) <*> tail) l) | |
naiveSolvePf _ = 0 | |
{- | |
Explain that each step was QuickChecked, then when writing blog post justify later | |
define | |
bmax = max | |
let max l = foldr bmax 0 l in ... | |
max . map length . filter isMountain . segs | |
= max . map length . concat . map (filter isMountain) . map tails . inits | |
= max . map length . concat . map (filter isMountain . tails) . inits | |
= max . concat . map (map length) . map (filter isMountain . tails) . inits | |
= max . concat . map (map length . filter isMountain . tails) . inits | |
= max . map max . map (map length . filter isMountain . tails) . inits | |
= max . map (max . map length . filter isMountain . tails) . inits | |
e = max . (map length . filter isMountain . tails) | |
Now, can we use Horner's rule for e? Use foldr definition of filter and length | |
filter' p = foldr (\a b -> if p a then a:b else b) [] | |
length' = foldr (\_ b -> b + 1) (0 :: Int) | |
So | |
e | |
= max . map length . filter' isMountain . tails | |
= foldr bmax 0 . map length . filter' isMountain . tails | |
= foldr (bmax . length) 0 . filter' isMountain . tails | |
But now recall, naiveSolvePf' = max . map e . inits | |
So we can use foldr/map fusion again | |
naiveSolvePf' | |
= max' . map (foldr (bmax . length) 0 . filter isMountain . tails) . inits | |
= foldr bmax 0 . map (foldr (bmax . length) 0 . filter isMountain . tails) . inits | |
= foldr (bmax . (foldr (bmax . length) 0 . filter isMountain . tails)) 0 . inits | |
= foldr (bmax . (foldr (bmax . length) 0 . foldr (\a b -> if isMountain a then a:b else b) [] . tails)) 0 . inits $ l | |
= foldr (bmax . foo) 0 . inits $ l | |
Let foo = foldr (bmax . length) 0 . foldr (\a b -> if isMountain a then a:b else b) [] . tails | |
To combine this into one catamorphism, apply fusion law | |
h w = v and h (g x y) = f x (h y) | |
----------------------------------- | |
h . foldr g w = foldr f v | |
foldr (bmax . length) 0 . foldr (\a b -> if isMountain a then a:b else b) [] . tails | |
<= | |
foldr (bmax . length) 0 [] = 0 = v | |
and | |
foldr (bmax . length) 0 ((\a b -> if isMountain a then a:b else b) x y) = f x (foldr (bmax . length) 0 y) | |
= foldr (bmax . length) 0 (if isMountain x then x:y else y) = f x (foldr (bmax . length) 0 y) | |
= if isMountain x then bmax (length x) (foldr (bmax . length) 0 y) else foldr (bmax . length) 0 y = f x (foldr (bmax . length) 0 y) | |
<= { generalize (foldr (bmax . length) 0 y) to ys } | |
= if isMountain x then bmax (length x) ys else ys = f x ys | |
Now we have definition of f. | |
= foldr (\x ys -> if isMountain x then bmax (length x) ys else ys) 0 | |
Larger context: | |
scan lemmas: | |
map (foldl f a) . inits = scanl f a | |
map (foldr f a) . tails = scanr f a | |
foldr (bmax . foo) 0 . inits | |
= foldr bmax 0 . map foo . inits | |
= foldr bmax 0 . map (foldr (\x ys -> if isMountain x then bmax (length x) ys else ys) 0 . tails) . inits | |
= max . map (foldr (\x ys -> if isMountain x then bmax (length x) ys else ys) 0 . tails) . inits | |
mountainSum x = if isMountain x then length x else 0 | |
naiveSolvePf' | |
= max . map (max . map mountainSum . tails) . inits | |
emptyState = (0, 0, head l, 0, Flat) | |
bar = maximum . map process . map (\l -> if null l then emptyState else foldl go (0, 0, head l, 0, Flat) (tail l)) . inits | |
process (!aRun, !dRun, _, !r, Down) = max (aRun + dRun) r | |
process (_, _, _, !r, _) = r | |
-} | |
-- Reasoning | |
tls :: [a] -> [[a]] | |
-- original: foldr (\ a (x:xs) -> (a:x):x:xs) [[]] | |
tls = flip (foldl (\g b x -> g ((\(x:xs) -> (b:x):x:xs) x)) id) [[]] | |
{- | |
bar l | |
= foldr (\a b -> max (process a) b) 0 (scanl go (0, 0, head l, 0, Flat) (tail l)) | |
= foldl (\b a -> max (process a) b) 0 (scanl go (0, 0, head l, 0, Flat) (tail l)) | |
Ok, fold-scan fusion law says that | |
foldl f a . scanl g b = fst . foldl h (f a b, b) | |
where | |
w = g v x | |
h (u,v) x = (f u w, w) | |
= fst . foldl h (f a b, b) $ tail l | |
where | |
a = 0 | |
f = flip (max . process) | |
b = (0, 0, head l, 0, Flat) | |
g = go | |
h (u,v) x = (f u w, w) | |
where | |
w = g v x | |
Now change foldl to foldl' since lists are assumed to be finite | |
-} | |
-- Efficient solution derived from naive, pointfree one | |
naiveSolvePf' :: [Int] -> Int | |
naiveSolvePf' l@(_:_:_:_) = bar l | |
where | |
bar l = fst . foldl' h (f a b, b) $ tail l | |
where | |
a = 0 | |
f = flip (max . process) | |
b = (0, 0, head l, 0, Flat) | |
g = go | |
h (u,v) x = let w = g v x in (f u w, w) | |
process (!aRun, !dRun, _, !r, Down) = max (aRun + dRun) r | |
process (_, _, _, !r, _) = r | |
-- Update solution only when in Down state, as we're coming down | |
-- from a mountain that could be the largest one yet. | |
go :: (Int, Int, Int, Int, Dir) -> Int -> (Int, Int, Int, Int, Dir) | |
go (!aRun, !dRun, !prev, !r, Up) curr = s' | |
where | |
s' = | |
case compare prev curr of | |
-- Up -> Up | |
LT -> (aRun + 1, dRun, curr, r, Up) | |
-- Up -> Down | |
GT -> (aRun, dRun + 1, curr, r, Down) | |
-- Up -> Flat | |
EQ -> (0, 0, curr, r, Flat) | |
go (!aRun, !dRun, !prev, !r, Down) curr = s' | |
where | |
r' = max (aRun + dRun) r | |
-- Always update solution | |
s' = | |
case compare prev curr of | |
-- Down -> Down | |
GT -> (aRun, dRun + 1, curr, r', Down) | |
-- Down -> Up | |
LT -> (2, 0, curr, r', Up) | |
-- Down -> Flat | |
EQ -> (0, 0, curr, r', Flat) | |
go (_, _, !prev, !r, Flat) curr = s' | |
where | |
s' = | |
case compare prev curr of | |
-- Flat -> Flat | |
GT -> (0, 0, curr, r, Flat) | |
-- Flat -> Up | |
LT -> (2, 0, curr, r, Up) | |
-- Flat -> Flat | |
EQ -> (0, 0, curr, r, Flat) | |
naiveSolvePf' _ = 0 | |
checkSol a b l = a l' == b l' | |
where | |
l' = abs <$> l | |
-- Check if efficient sol is correct wrt naive sol | |
solCorrect :: [Int] -> Bool | |
solCorrect = checkSol solve naiveSolve | |
-- Check if efficient sol is correct wrt pointfree naive sol | |
solCorrect' :: [Int] -> Bool | |
solCorrect' = checkSol solve naiveSolvePf | |
-- Horner's Rule (for lists) | |
tri :: (a -> a) -> [a] -> [a] | |
tri f = foldr (\a b -> a : map f b) [] | |
{- | |
The claim, for bifunctor F | |
f . g = g . F (f, f) | |
--------------------------------------- | |
cata g . tri f = cata (g . F (id,f)) | |
-} | |
{- | |
Specializing to lists we have | |
f c = c and f (g (a,b)) = g (f a, f b) | |
--------------------------------------------------------- | |
foldr g c . tri f = foldr (\a b -> g (a, f b)) c | |
For instance, let c = 0, f = id, g (a, b) = a + b then | |
Prove provisos: | |
1. f c = id 0 = 0 = c | |
2. f (g (a,b)) = id (a + b) = a + b = (id a) + (id b) = g (f a, f b) | |
Then conclude | |
foldr (+) 0 . tri id = foldr (\a b -> a + b) 0 | |
-} | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment