Skip to content

Instantly share code, notes, and snippets.

@nomeata
Created August 6, 2020 11:43
Show Gist options
  • Save nomeata/3f61dc16cfed360c3df51eab1892e0a5 to your computer and use it in GitHub Desktop.
Save nomeata/3f61dc16cfed360c3df51eab1892e0a5 to your computer and use it in GitHub Desktop.
Many faces of isOrderedTree – code to the talk (actually extended version)
{-# LANGUAGE GADTSyntax #-}
{-# LANGUAGE DeriveFoldable #-}
module Tree where
import Control.Monad
import Data.Maybe
import Data.Foldable
data T a = L | N (T a) a (T a) deriving (Show, Foldable)
isOrdered0 :: Ord a => T a -> Bool
isOrdered0 L = True
isOrdered0 (N l x r) =
isOrdered0 l &&
isOrdered0 r &&
(case l of L -> True; N _ y _ -> y <= x) &&
(case r of L -> True; N _ y _ -> x <= y)
isOrdered1 :: Ord a => T a -> Bool
isOrdered1 = everynode (\l x r -> all (<= x) (elems l) && all (>= x) (elems r))
everynode :: (T a -> a -> T a -> Bool) -> T a -> Bool
everynode p L = True
everynode p (N l x r) = p l x r && everynode p l && everynode p r
elems :: T a -> [a]
elems L = []
elems (N l x r) = elems l ++ [x] ++ elems r
isOrdered2 :: Ord a => T a -> Bool
isOrdered2 L = True
isOrdered2 (N l x r) =
all (<= x) (elems l) &&
all (>= x) (elems r) &&
isOrdered2 l &&
isOrdered2 r
-- allElems p t = all p (elems t)
allElems :: (a -> Bool) -> T a -> Bool
allElems p L = True
allElems p (N l x r) = allElems p l && p x && allElems p r
-- replace all p elems with allElems p
-- (maybe forget updating recursive call)
isOrdered3 :: Ord a => T a -> Bool
isOrdered3 L = True
isOrdered3 (N l x r) =
allElems (<= x) l &&
allElems (>= x) r &&
isOrdered3 l &&
isOrdered3 r
-- local go
isOrdered4 :: Ord a => T a -> Bool
isOrdered4 = go
where
go L = True
go (N l x r) =
allElems (<= x) l &&
allElems (>= x) r &&
go l &&
go r
-- Fuse allElems and go into a single traversal
isOrdered5 :: Ord a => T a -> Bool
isOrdered5 = go' (const True)
where
-- go' p t = allElems p t && go t
go' p L = True
go' p (N l x r) =
p x &&
go' (\y -> p y && y <= x) l &&
go' (\y -> p y && y >= x) r
isOrdered6 :: Ord a => T a -> Bool
isOrdered6 = go' constTrue
where
constTrue :: (a -> Bool)
constTrue = const True
andLe, andGe :: Ord a => (a -> Bool) -> a -> (a -> Bool)
andLe p x = \y -> p y && y <= x
andGe p x = \y -> p y && y >= x
go' p L = True
go' p (N l x r) = p x && go' (andLe p x) l && go' (andGe p x) r
-- Defunctionalization
-- data Pred a = ConstTrue | AndLe (Pred a) a | AndGe (Pred a) a
data Pred a where
ConstTrue :: Pred a
AndLe :: Pred a -> a -> Pred a
AndGe :: Pred a -> a -> Pred a
eval :: Ord a => Pred a -> (a -> Bool)
eval ConstTrue = const True
eval (AndLe p x) = \y -> eval p y && y <= x
eval (AndGe p x) = \y -> eval p y && y >= x
isOrdered7 :: Ord a => T a -> Bool
isOrdered7 = go' ConstTrue
where
go' p L = True
go' p (N l x r) = eval p x && go' (AndLe p x) l && go' (AndGe p x) r
-- A more precise type for intervals
type Interval a = (Maybe a, Maybe a)
full :: Interval a
andLe, andGe :: Ord a => Interval a -> a -> Interval a
full = (Nothing, Nothing)
andLe i@(_, Just ub) x | ub < x = i
andLe (lb, _) x = (lb, Just x)
andGe i@(Just lb, _) x | x < lb = i
andGe (_, ub) x = (Just x, ub)
inInterval :: Ord a => Interval a -> a -> Bool
inInterval (lb, ub) x = maybe True (<= x) lb && maybe True (>= x) ub
isOrdered8 :: Ord a => T a -> Bool
isOrdered8 = go full
where
go p L = True
go p (N l x r) = inInterval p x && go (andLe p x) l && go (andGe p x) r
-- Inline the type, and notice that we don’t need to do the checks
isOrdered9 :: Ord a => T a -> Bool
isOrdered9 = go (Nothing, Nothing)
where
go _ L = True
go (lb, ub) (N l x r) =
maybe True (<= x) lb && maybe True (>= x) ub &&
go (lb, Just x) l && go (Just x, ub) r
-- Unbox the option
isOrdered10 :: Ord a => T a -> Bool
isOrdered10 = goNN
where
goNN :: Ord a => T a -> Bool
goNN L = True
goNN (N l x r) = goNJ x l && goJN x r
goNJ :: Ord a => a -> T a -> Bool
goNJ _ L = True
goNJ ub (N l x r) = ub >= x && goNJ x l && goJJ x ub r
goJN :: Ord a => a -> T a -> Bool
goJN _ L = True
goJN lb (N l x r) = lb <= x && goJJ lb x l && goJN x r
goJJ :: Ord a => a -> a -> T a -> Bool
goJJ _ _ L = True
goJJ lb ub (N l x r) = lb <= x && ub >= x && goJJ lb x l && goJJ x ub r
-- starting from isOrdered2
isOrdered11 :: Ord a => T a -> Bool
isOrdered11 t = fst (go' t)
where
-- go' t = (go t, elems t)
go' :: Ord a => T a -> (Bool, [a])
go' L = (True, [])
go' (N l x r) =
let (ok_l, elems_l) = go' l in
let (ok_r, elems_r) = go' r in
( all (<= x) elems_l &&
all (>= x) elems_r &&
ok_l && ok_r
, elems_l ++ [x] ++ elems_r
)
isOrdered12 :: Ord a => T a -> Bool
isOrdered12 t = isJust (go' t)
where
-- (True, xs) <-> Just xs
-- (False, xs) <-> Nothing
-- Maybe monad!
go' :: Ord a => T a -> Maybe [a]
go' L = Just []
go' (N l x r) = do
elems_l <- go' l
elems_r <- go' r
guard $ all (<= x) elems_l
guard $ all (>= x) elems_r
return $ elems_l ++ [x] ++ elems_r
isOrdered13 :: Ord a => T a -> Bool
isOrdered13 t = isJust (go' t)
where
-- only check minium/maximum
go' :: Ord a => T a -> Maybe [a]
go' L = Just []
go' (N l x r) = do
elems_l <- go' l
elems_r <- go' r
guard $ null elems_l || maximum elems_l <= x
guard $ null elems_r || minimum elems_r >= x
return $ elems_l ++ [x] ++ elems_r
isOrdered14 :: Ord a => T a -> Bool
isOrdered14 t = isJust (go' t)
where
-- only check first/last element
go' :: Ord a => T a -> Maybe [a]
go' L = Just []
go' (N l x r) = do
elems_l <- go' l
elems_r <- go' r
guard $ null elems_l || last elems_l <= x
guard $ null elems_r || head elems_r >= x
return $ elems_l ++ [x] ++ elems_r
isOrdered15 :: Ord a => T a -> Bool
isOrdered15 t = isJust (go' t)
where
-- only return leftmost/rightmost
-- [] <-> Nothing
-- [x,…,y] <-> Just (x,y)
go' :: Ord a => T a -> Maybe (Maybe (a,a))
go' L = Just Nothing
go' (N l x r) = do
elems_l <- go' l
elems_r <- go' r
guard $ maybe True (\(_,y) -> y <= x) elems_l
guard $ maybe True (\(y,_) -> y >= x) elems_r
return $ elems_l <.> Just (x,x) <.> elems_r
Nothing <.> x = x
x <.> Nothing = x
Just (l,_) <.> Just (_,r) = Just (l,r)
isOrdered16 :: Ord a => T a -> Bool
isOrdered16 = go'
where
go' :: Ord a => T a -> Bool
go' L = True
go' t = isJust (goN t)
goN :: Ord a => T a -> Maybe (a,a)
goN (N L x L) = return (x,x)
goN (N L x r) = do
(rl, ru) <- goN r
guard $ rl >= x
return (x,ru)
goN (N l x L) = do
(ll, lu) <- goN l
guard $ lu <= x
return (ll, x)
goN (N l x r) = do
(ll, lu) <- goN l
(rl, ru) <- goN r
guard $ rl >= x
guard $ lu <= x
return (ll, ru)
-- from isOrdered11
isOrdered17 :: Ord a => T a -> Bool
isOrdered17 t = sortedList (go' t)
where
-- ∀ (b,xs). b = sortedList xs
-- note dropping of Ord constraint
go' :: T a -> [a]
go' L = []
go' (N l x r) = go' l ++ [x] ++ go' r
sortedList :: Ord a => [a] -> Bool
sortedList [] = True
sortedList [x] = True
sortedList (x:y:zs) = x <= y && sortedList (y : zs)
-- difference list
isOrdered18 :: Ord a => T a -> Bool
isOrdered18 t = sortedList (go' t [])
where
go' L = id
go' (N l x r) = go' l . (x:) . go' r
-- now use Foldable
isOrdered19 :: Ord a => T a -> Bool
isOrdered19 = sortedList . toList
-- Now testing with Quickcheck
{-
:load Tree Test ABC
:module Tree Test ABC Test.QuickCheck
quickCheck $ \t -> isOrdered1 t == isOrdered2 t
quickCheck $ \t -> isOrdered1 0 == isOrdered1 t
verboseCheck $ \t -> isOrdered1 t == isOrdered2 t
:set -XTypeApplications
verboseCheck $ \t -> isOrdered1 t == isOrdered2 @Int t
table (allFuns @Int)
:set -fobject-code -O
table (allFuns @Int)
table (allFuns @ABC)
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment