Many faces of isOrderedTree – code to the talk (actually extended version)

Tree.hs

{-# 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)
-}