Skip to content

Instantly share code, notes, and snippets.

@siraben
Last active December 2, 2020 04:01
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save siraben/6b1f57ff1a3fbb76432eb79f0f91f507 to your computer and use it in GitHub Desktop.
Save siraben/6b1f57ff1a3fbb76432eb79f0f91f507 to your computer and use it in GitHub Desktop.
maximum mountain and derivation
{-# 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