FR
PréludeChargé par défaut — aucun import nécessaire.

More list functions

Synopsis 
sum : Additive a => List a -> a

Sum of a list (0 for the empty list).

elem : Eq a => a -> List a -> Bool

Is a value an element of a list?

any : (a -> Bool) -> List a -> Bool

Does any element satisfy the predicate?

all : (a -> Bool) -> List a -> Bool

Do all elements satisfy the predicate?

take : Nat -> List a -> List a

The first n elements (fewer if the list is shorter). n : Nat, the same count type as length.

drop : Nat -> List a -> List a

All but the first n elements.

takeWhile : (a -> Bool) -> List a -> List a

The longest prefix whose elements all satisfy the predicate.

dropWhile : (a -> Bool) -> List a -> List a

The remainder after removing the longest prefix that satisfies the predicate (the companion of takeWhile).

index : Nat -> List a -> Maybe a

The element at position n (0-based): index 0 xs is the head; Nothing when n is out of range. The safe accessor — it returns a Maybe rather than failing, like head. (For container-first subscripting see Core.Index: xs[i] / xs ! i.)

zip : List a -> List b -> List (a, b)

Pair up elements of two lists (truncating to the shorter).

zipWith : (a -> b -> c) -> List a -> List b -> List c

Combine two lists element-wise with a function.

range : Int -> Int -> List Int

A list of integers from lo to hi inclusive (empty if lo > hi). [1 .. n] — the for loop's counted-range idiom — does not overflow the stack for large n.

rangeDown : Int -> Int -> List Int -> List Int
applyTimes : (a -> a) -> Nat -> a -> a

Apply f to x, n times (f (f … (f x))). Backs the DEFAULT stepping below, so a bare Enum (enumFromTo, succ, stepUp, stepDown) supports stepped ranges out of the box.

interface Enum a where
enumFromTo : a -> a -> List a
succ : a -> a            -- ^ the next value; lets `for x in [lo..hi]` count without a list
enumDist : a -> a -> Nat            -- ^ PRE lo ≤ hi : count of unit steps from lo up to hi
succBy : a -> Nat -> a              -- ^ advance UP by n unit steps
-- WHERE THE TYPE STOPS (KB-200, 2026-10-07 : a range with no bound, `[e ..]`
-- DEFAULTS (Thomas, 2026-10-07 : a lab's `Enum` must keep compiling) say
-- exactly what `succ` alone can tell : UP goes as far as `succ` goes — an
-- nothing exists below).  To revisit : bounds as interfaces (minBound,
stepUp : a -> Nat -> Maybe a        -- ^ the value n unit steps UP, if the type has one
stepDown : a -> Nat -> Maybe a      -- ^ the value n unit steps DOWN, if the type has one

Types whose values can be enumerated over a bounded range. Backs the range notation [lo .. hi], which desugars to enumFromTo lo hi.

Instances : Char, Int, Nat
enumFromToExcl : Ord a => Enum a => a -> a -> List a

The HALF-OPEN range [lo, hi[ (or [lo, hi)) : lo, succ lo, … up to but EXCLUDING hi (D7). EMPTY when hi <= lo (Dijkstra's convention: the length is exactly hi - lo, [a .. a[ is empty, [0 .. k[ ++ [k .. n[ == [0 .. n[). The PRIMITIVE half-open enumerator — NOT enumFromTo lo (pred hi): the < hi guard needs no pred/subtraction, so it stays correct at hi <= lo and works for EVERY Enum (Nat, Char…), not only Int. Constant stack for large ranges.

rangeStepZeroMessage : String
enumNoStepDownMessage : String
enumFromThenTo : Ord a => Enum a => a -> a -> a -> List a

The STEPPED range [a, b .. c] (D8), INCLUSIVE of c : a, then each value a step on from the last, the step being b − a MONTRÉ by the two terms. [1,3..11] = 1 3 5 7 9 11. The DIRECTION is read from a vs b (Ord), so descent is native — [10,8..0] = 10 8 6 4 2 0, and on Nat [5,3..1] = 5 3 1 with no signed step (never the d = b − a monus-underflow trap). Step 0 (b == a, an unbounded range) is REFUSED: at COMPILE time when the two first terms are literals, as a clean runtime error otherwise. Constant stack.

enumFromThenToExcl : Ord a => Enum a => a -> a -> a -> List a

The half-open stepped range [a, b .. c[ (or [a, b .. c)) (D8) : as enumFromThenTo but EXCLUDING c — [1,3..11[ = 1 3 5 7 9. Same direction rule, same step-0 refusal, same constant stack.

elemBy : (a -> a -> Bool) -> a -> List a -> Bool

Is an element present, using a supplied equality test? (General form of elem, which uses ==.)

concatMap : (a -> List b) -> List a -> List b

Map a list-valued function over a list and concatenate the results. concatMap f = concat . map f.

insertOrd : Ord a => a -> List a -> List a

Insert into a sorted list, keeping it sorted.

sort : Ord a => List a -> List a

Sort a list into ascending order (insertion sort).

replicate : Nat -> a -> List a

n copies of a value. n : Nat.

lookup : Eq k => k -> List (k, v) -> Maybe v

Look up a key in an association list.

maximum : Ord a => List a -> Maybe a

Largest element, or Nothing if empty (total).

maxFrom : Ord a => a -> List a -> a
minimum : Ord a => List a -> Maybe a

Smallest element, or Nothing if empty (total).

minFrom : Ord a => a -> List a -> a
mapMaybe : (a -> Maybe b) -> List a -> List b

Apply a partial function to every element, keeping the successes. mapMaybe f xs = catMaybes (map f xs), but in a single pass.

last' : List a -> Maybe a

The last element of a list, or Nothing if it is empty (total).

intersperse : a -> List a -> List a

Insert sep between consecutive elements of a list (no leading/trailing). intersperse 0 [1, 2, 3] = [1, 0, 2, 0, 3]

intercalate : Monoid m => m -> List m -> m

Join monoid values, inserting sep between consecutive elements (no trailing separator). intercalate sep = concat . intersperse sep. Generalises Haskell's Data.List.intercalate to any Monoid, so it serves both strings and lists of lists: intercalate ", " ["a", "b", "c"] = "a, b, c" intercalate [0] [[1], [2], [3]] = [1, 0, 2, 0, 3]

joinBy : String -> List String -> String

Join a list of strings with sep between them (no trailing separator) — the string face of intercalate, named as in Idris 2 (Data.String.joinBy): joinBy "\n" ["a", "b"] = "a\nb"

lowercase : String -> String

Lower-case every character of a string.

trim : String -> String

Strip leading and trailing ASCII whitespace from a string.

Searching, splitting, grouping, scanning (Data.List staples)

findIndex : (a -> Bool) -> List a -> Maybe Nat

The 0-based index of the first element satisfying the predicate.

elemIndex : Eq a => a -> List a -> Maybe Nat

The 0-based index of the first occurrence of a value.

partition : (a -> Bool) -> List a -> (List a, List a)

Split into (elements satisfying p, the rest), preserving order.

span : (a -> Bool) -> List a -> (List a, List a)

(longest prefix all satisfying p, the remainder): span p = (takeWhile p, dropWhile p).

break : (a -> Bool) -> List a -> (List a, List a)

break p = span (not . p): the prefix up to the first element satisfying p.

sortBy : (a -> a -> Ordering) -> List a -> List a

Sort by a supplied comparator (stable insertion sort). General form of sort, which uses compare.

sortOn : Ord b => (a -> b) -> List a -> List a

Sort by a key projection (decorate–sort–undecorate): each element is paired with its key, the pairs are sorted by key, then the keys are dropped — so the key function runs once per element, not at every comparison. The projection companion of sortBy (à la Haskell/Idris sortOn, Rust sort_by_key).

nubBy : (a -> a -> Bool) -> List a -> List a

Remove duplicates using a supplied equality, keeping the first occurrence.

nub : Eq a => List a -> List a

Remove duplicates (by ==), keeping the first occurrence.

groupBy : (a -> a -> Bool) -> List a -> List (List a)

Group consecutive elements deemed equal by the predicate.

group : Eq a => List a -> List (List a)

Group consecutive equal elements (by ==): group [1,1,2,3,3] = [[1,1],[2],[3,3]].

scanl : (b -> a -> b) -> b -> List a -> List b

Left scan: the running accumulator after each step, seeded with z. scanl (+) 0 [1,2,3] = [0,1,3,6] (always one longer than the input).

scanr : (a -> b -> b) -> b -> List a -> List b

Right scan: scanr (+) 0 [1,2,3] = [6,5,3,0] (always non-empty).

zipWith3 : (a -> b -> c -> d) -> List a -> List b -> List c -> List d

Zip three lists with a function (truncating to the shortest).

unfoldr : (b -> Maybe (a, b)) -> b -> List a

Build a list from a seed: f returns Just (element, next seed) to emit, or Nothing to stop.

foldl1 : (a -> a -> a) -> List a -> Maybe a

Left fold over a NON-empty list, seeded with its first element; Nothing for the empty list (total).

foldr1 : (a -> a -> a) -> List a -> Maybe a

Right fold over a NON-empty list; Nothing for the empty list (total).

tails : List a -> List (List a)

All suffixes of a list, longest first: tails [1,2] = [[1,2],[2],[]].

isPrefixOf : Eq a => List a -> List a -> Bool

Is the first list a prefix of the second?

isSuffixOf : Eq a => List a -> List a -> Bool

Is the first list a suffix of the second?

isInfixOf : Eq a => List a -> List a -> Bool

Is the first list a contiguous sub-sequence of the second?

String splitting (words / lines / split-on-delimiter)

isSpaceChar : Char -> Bool
words : String -> List String

Split a string into words on runs of whitespace (no empty words). words " a b " = ["a", "b"].

lines : String -> List String

Split a string at newlines. A trailing newline does not add an empty line: lines "a\nb" = ["a", "b"], lines "a\n" = ["a"], lines "a\n\nb" = ["a", "", "b"].

splitOnChar : Char -> String -> List String

Split a string on every occurrence of a delimiter character, keeping empty chunks: splitOnChar ',' "a,,b" = ["a", "", "b"], splitOnChar ',' "" = [""].

Maybe / Either utilities

fromLeft : a -> Either a b -> a

The Left value, or a default for a Right.

fromRight : b -> Either a b -> b

The Right value, or a default for a Left.

partitionEithers : List (Either a b) -> (List a, List b)

Split a list of Eithers into (the Lefts, the Rights), preserving order.