Agda.Utils.List

Utility functions for lists.

Variants of list case, cons, head, tail, init, last

snoc :: [a] -> a -> [a]

Append a single element at the end. Time: O(length); use only on small lists.

caseList :: [a] -> b -> (a -> [a] -> b) -> b

Case distinction for lists, with list first. O(1).

Cf. ifNull.

caseListM :: Monad m => m [a] -> m b -> (a -> [a] -> m b) -> m b

Case distinction for lists, with list first. O(1).

Cf. ifNull.

listCase :: b -> (a -> [a] -> b) -> [a] -> b

Case distinction for lists, with list last. O(1).

headWithDefault :: a -> [a] -> a

Head function (safe). Returns a default value on empty lists. O(1).

headWithDefault 42 []      = 42
headWithDefault 42 [1,2,3] = 1

tailMaybe :: [a] -> Maybe [a]

Tail function (safe). O(1).

tailWithDefault :: [a] -> [a] -> [a]

Tail function (safe). Returns a default list on empty lists. O(1).

lastMaybe :: [a] -> Maybe a

Last element (safe). O(n).

last2 :: [a] -> Maybe (a, a)

Last two elements (safe). O(n).

uncons :: [a] -> Maybe (a, [a])

Opposite of cons (:), safe. O(1).

mcons :: Maybe a -> [a] -> [a]

Maybe cons. O(1). mcons ma as = maybeToList ma ++ as

initLast :: [a] -> Maybe ([a], a)

init and last in one go, safe. O(n).

initMaybe :: [a] -> Maybe [a]

init, safe. O(n).

Lookup and indexing

(!!!) :: [a] -> Int -> Maybe a

Lookup function (partially safe). O(min n index).

indexWithDefault :: a -> [a] -> Int -> a

Lookup function with default value for index out of range. O(min n index).

The name is chosen akin to genericIndex.

findWithIndex :: (a -> Bool) -> [a] -> Maybe (a, Int)

Find an element satisfying a predicate and return it with its index. O(n) in the worst case, e.g. findWithIndex f xs = Nothing.

TODO: more efficient implementation!?

genericElemIndex :: (Eq a, Integral i) => a -> [a] -> Maybe i

A generalised variant of elemIndex. O(n).

downFrom :: Integral a => a -> [a]

downFrom n = [n-1,..1,0]. O(n).

Update

updateHead :: (a -> a) -> [a] -> [a]

Update the first element of a list, if it exists. O(1).

updateLast :: (a -> a) -> [a] -> [a]

Update the last element of a list, if it exists. O(n).

updateAt :: Int -> (a -> a) -> [a] -> [a]

Update nth element of a list, if it exists. O(min index n).

Precondition: the index is >= 0.

Sublist extraction and partitioning

type Prefix a

Arguments

 = [a]

The list before the split point.

type Suffix a

Arguments

 = [a]

The list after the split point.

splitExactlyAt :: Integral n => n -> [a] -> Maybe (Prefix a, Suffix a)

splitExactlyAt n xs = Just (ys, zs) iff xs = ys ++ zs and genericLength ys = n.

dropEnd :: forall a. Int -> [a] -> Prefix a

Drop from the end of a list. O(length).

dropEnd n = reverse . drop n . reverse

Forces the whole list even for n==0.

spanEnd :: forall a. (a -> Bool) -> [a] -> (Prefix a, Suffix a)

Split off the largest suffix whose elements satisfy a predicate. O(n).

spanEnd p xs = (ys, zs) where xs = ys ++ zs and all p zs and maybe True (not . p) (lastMaybe yz).

takeWhileJust :: (a -> Maybe b) -> [a] -> Prefix b

A generalized version of takeWhile. (Cf. mapMaybe vs. filter). @O(length . takeWhileJust f).

takeWhileJust f = fst . spanJust f.

spanJust :: (a -> Maybe b) -> [a] -> (Prefix b, Suffix a)

A generalized version of span. O(length . fst . spanJust f).

partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])

Partition a list into Nothings and Justs. O(n).

partitionMaybe f = partitionEithers . map ( a -> maybe (Left a) Right (f a))

Note: mapMaybe f = snd . partitionMaybe f.

filterAndRest :: (a -> Bool) -> [a] -> ([a], Suffix a)

Like filter, but additionally return the last partition of the list where the predicate is False everywhere. O(n).

mapMaybeAndRest :: (a -> Maybe b) -> [a] -> ([b], Suffix a)

Like mapMaybe, but additionally return the last partition of the list where the function always returns Nothing. O(n).

isSublistOf :: Eq a => [a] -> [a] -> Bool

Sublist relation.

holes :: [a] -> [(a, [a])]

All ways of removing one element from a list. O(n²).

Prefix and suffix

Prefix

commonPrefix :: Eq a => [a] -> [a] -> Prefix a

Compute the common prefix of two lists. O(min n m).

dropCommon :: [a] -> [b] -> (Suffix a, Suffix b)

Drops from both lists simultaneously until one list is empty. O(min n m).

stripPrefixBy :: (a -> a -> Bool) -> Prefix a -> [a] -> Maybe (Suffix a)

Check if a list has a given prefix. If so, return the list minus the prefix. O(length prefix).

Suffix

commonSuffix :: Eq a => [a] -> [a] -> Suffix a

Compute the common suffix of two lists. O(n + m).

stripSuffix :: Eq a => Suffix a -> [a] -> Maybe (Prefix a)

stripSuffix suf xs = Just pre iff xs = pre ++ suf. O(n).

type ReversedSuffix a = [a]

stripReversedSuffix :: forall a. Eq a => ReversedSuffix a -> [a] -> Maybe (Prefix a)

stripReversedSuffix rsuf xs = Just pre iff xs = pre ++ reverse suf. O(n).

data StrSufSt a

Internal state for stripping suffix.

Constructors

SSSMismatch

Error.

SSSStrip (ReversedSuffix a)

"Negative string" to remove from end. List may be empty.

SSSResult [a]

"Positive string" (result). Non-empty list.

Groups and chunks

groupOn :: Ord b => (a -> b) -> [a] -> [[a]]

groupOn f = groupBy ((==) `on` f) . sortBy (compare `on` f). O(n log n).

groupBy' :: (a -> a -> Bool) -> [a] -> [[a]]

A variant of groupBy which applies the predicate to consecutive pairs. O(n).

wordsBy :: (a -> Bool) -> [a] -> [[a]]

Split a list into sublists. Generalisation of the prelude function words. O(n).

words xs == wordsBy isSpace xs

chop :: Int -> [a] -> [[a]]

Chop up a list in chunks of a given length. O(n).

chopWhen :: (a -> Bool) -> [a] -> [[a]]

Chop a list at the positions when the predicate holds. Contrary to wordsBy, consecutive separator elements will result in an empty segment in the result. O(n).

intercalate [x] (chopWhen (== x) xs) == xs

List as sets

hasElem :: Ord a => [a] -> a -> Bool

Check membership for the same list often. Use partially applied to create membership predicate hasElem xs :: a -> Bool.

• First time: O(n log n) in the worst case.
• Subsequently: O(log n).

Specification: hasElem xs == (elem xs).

sorted :: Ord a => [a] -> Bool

Check whether a list is sorted. O(n).

Assumes that the Ord instance implements a partial order.

distinct :: Eq a => [a] -> Bool

Check whether all elements in a list are distinct from each other. Assumes that the Eq instance stands for an equivalence relation.

O(n²) in the worst case distinct xs == True.

fastDistinct :: Ord a => [a] -> Bool

An optimised version of distinct. O(n log n).

Precondition: The list's length must fit in an Int.

duplicates :: Ord a => [a] -> [a]

Returns an (arbitrary) representative for each list element that occurs more than once. O(n log n).

allDuplicates :: Ord a => [a] -> [a]

Remove the first representative for each list element. Thus, returns all duplicate copies. O(n log n).

allDuplicates xs == sort $ xs \ nub xs.

nubOn :: Ord b => (a -> b) -> [a] -> [a]

Efficient variant of nubBy for lists, using a set to store already seen elements. O(n log n)

Specification:

nubOn f xs == 'nubBy' ((==) `'on'` f) xs.

uniqOn :: Ord b => (a -> b) -> [a] -> [a]

Efficient variant of nubBy for finite lists. O(n log n).

Specification: For each list xs there is a list ys which is a permutation of xs such that

uniqOn f xs == 'nubBy' ((==) `'on'` f) ys.

Furthermore:

List.sortBy (compare `on` f) (uniqOn f xs) == uniqOn f xs
uniqOn id == Set.toAscList . Set.fromList

allEqual :: Eq a => [a] -> Bool

Checks if all the elements in the list are equal. Assumes that the Eq instance stands for an equivalence relation. O(n).

Zipping

zipWith' :: (a -> b -> c) -> [a] -> [b] -> Maybe [c]

Requires both lists to have the same length. O(n).

Otherwise, Nothing is returned.

zipWithKeepRest :: (a -> b -> b) -> [a] -> [b] -> [b]

Like zipWith but keep the rest of the second list as-is (in case the second list is longer). O(n).

  zipWithKeepRest f as bs == zipWith f as bs ++ drop (length as) bs

Unzipping

unzipWith :: (a -> (b, c)) -> [a] -> ([b], [c])

Edit distance

editDistanceSpec :: Eq a => [a] -> [a] -> Int

Implemented using tree recursion, don't run me at home! O(3^(min n m)).

editDistance :: forall a. Eq a => [a] -> [a] -> Int

Implemented using dynamic programming and Data.Array. O(n*m).