From 3b6390f8ca20dd720e80ffeb279328e8f4c18eee Mon Sep 17 00:00:00 2001 From: oleja Date: Mon, 10 Aug 2026 15:36:01 +0300 Subject: [PATCH 1/9] [ docs ] add documentation for `Applicative` interface --- libs/prelude/Prelude/Interfaces.idr | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr index f4c2ab78803..843cd9f23d9 100644 --- a/libs/prelude/Prelude/Interfaces.idr +++ b/libs/prelude/Prelude/Interfaces.idr @@ -169,16 +169,29 @@ namespace Bifunctor mapFst = map . mapFst mapSnd = map . mapSnd +||| A functor with application, providing operations to embed +||| pure expressions ('pure') and sequence computations (`<*>`). +||| Abstracts the notion of function application. +||| @ f a parameterised type public export interface Functor f => Applicative f where constructor MkApplicative + ||| Lift a value into the structure. + ||| @ f the parameterised type pure : a -> f a + + ||| Sequential application. + ||| @ f the parameterised type (<*>) : f (a -> b) -> f a -> f b +||| Sequence actions, discarding the value of the second argument. +||| @ f the parameterised type public export %tcinline (<*) : Applicative f => f a -> f b -> f a a <* b = map const a <*> b +||| Sequence actions, discarding the value of the first argument. +||| @ f the parameterised type public export %tcinline (*>) : Applicative f => f a -> f b -> f b a *> b = map (const id) a <*> b From 91db2ea33e992861440ef0f5b3125483b23b6aad Mon Sep 17 00:00:00 2001 From: oleja Date: Tue, 11 Aug 2026 14:32:49 +0300 Subject: [PATCH 2/9] [ docs ] add documentation for `mapHom` --- libs/prelude/Prelude/Interfaces.idr | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr index 843cd9f23d9..3245f07852a 100644 --- a/libs/prelude/Prelude/Interfaces.idr +++ b/libs/prelude/Prelude/Interfaces.idr @@ -156,9 +156,16 @@ interface Bifunctor f where mapSnd : (b -> d) -> f a b -> f a d mapSnd = bimap id +||| The action of the `Bifunctor` on morphisms pertaining to both objects. +||| Applies the same morphism to the first and second objects. +||| +||| ```idris example +||| mapHom (\x => x + 1) (5, 10) == (6, 11) +||| ``` +||| @ func the morphism to apply public export %tcinline -mapHom : Bifunctor f => (a -> b) -> f a a -> f b b -mapHom f = bimap f f +mapHom : Bifunctor f => (func : a -> b) -> f a a -> f b b +mapHom func = bimap func func namespace Bifunctor From b67e9f1712968b1a259aaa2cb33bd213ce7a5c73 Mon Sep 17 00:00:00 2001 From: oleja Date: Tue, 11 Aug 2026 16:55:01 +0300 Subject: [PATCH 3/9] [ docs ] add code examples for `Applicative` documentation --- libs/prelude/Prelude/Interfaces.idr | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr index 3245f07852a..ec6e0aff7b7 100644 --- a/libs/prelude/Prelude/Interfaces.idr +++ b/libs/prelude/Prelude/Interfaces.idr @@ -183,21 +183,37 @@ namespace Bifunctor public export interface Functor f => Applicative f where constructor MkApplicative - ||| Lift a value into the structure. + ||| Lifts a value into the structure. ||| @ f the parameterised type pure : a -> f a - ||| Sequential application. + ||| Sequential application. Applies an `Applicative` of functions to + ||| a second `Applicative`. + ||| + ||| ```idris example + ||| ((Just \x => x + 1) <*> Just 5) == Just 6 + ||| ``` ||| @ f the parameterised type (<*>) : f (a -> b) -> f a -> f b ||| Sequence actions, discarding the value of the second argument. +||| +||| ```idris example +||| (Just 5 <* Just 10) == Just 5 +||| ``` ||| @ f the parameterised type public export %tcinline (<*) : Applicative f => f a -> f b -> f a a <* b = map const a <*> b ||| Sequence actions, discarding the value of the first argument. +||| +||| ```idris example +||| (Just 5 *> Just 10) == Just 10 +||| ``` +||| ```idris example +||| (Nothing *> Just 2) == Nothing +||| ``` ||| @ f the parameterised type public export %tcinline (*>) : Applicative f => f a -> f b -> f b From 855615780dac5adbe65326a30bd53e3a58f240f1 Mon Sep 17 00:00:00 2001 From: oleja Date: Tue, 11 Aug 2026 17:38:52 +0300 Subject: [PATCH 4/9] [ docs ] added documentation for `Bifoldable` interface --- libs/prelude/Prelude/Interfaces.idr | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr index ec6e0aff7b7..53d3e1d25ca 100644 --- a/libs/prelude/Prelude/Interfaces.idr +++ b/libs/prelude/Prelude/Interfaces.idr @@ -547,11 +547,25 @@ namespace Foldable public export interface Bifoldable p where constructor MkBifoldable - bifoldr : (a -> acc -> acc) -> (b -> acc -> acc) -> acc -> p a b -> acc + ||| Successively combine elements of two different types in a parameterised type using the + ||| provided functions, starting with the element that is in the final position, + ||| i.e. the right-most position. + ||| @ f The function used to fold elements of the first type into the accumulated result + ||| @ g The function used to fold elements of the second type into the accumulated result + ||| @ init The starting value the results are being combined into + ||| @ input The parameterised type + bifoldr : (f : a -> acc -> acc) -> (g : b -> acc -> acc) -> (init : acc) -> (input : p a b) -> acc - bifoldl : (acc -> a -> acc) -> (acc -> b -> acc) -> acc -> p a b -> acc + ||| The same as `bifoldr` but begins folding from the element at the initial + ||| position in the data structure parameterised by two types, i.e. the left-most position. + ||| @ f The function used to fold elements of the first type into the accumulated result + ||| @ g The function used to fold elements of the second type into the accumulated result + ||| @ init The starting value the results are being combined into + ||| @ input The parameterised type + bifoldl : (f : acc -> a -> acc) -> (g : acc -> b -> acc) -> (init : acc) -> (input : p a b) -> acc bifoldl f g z t = bifoldr (flip (.) . flip f) (flip (.) . flip g) id t z + ||| Test whether the structure parameterised by two types is empty. binull : p a b -> Bool binull t = bifoldr {acc = Lazy Bool} (\ _,_ => False) (\ _,_ => False) True t From 011d2f4daaf3a31afe7dc0aefc7028d4fa86dfaf Mon Sep 17 00:00:00 2001 From: oleja Date: Tue, 11 Aug 2026 18:32:12 +0300 Subject: [PATCH 5/9] [ docs ] add documentation for some named interface implementations --- libs/prelude/Prelude/Interfaces.idr | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr index 53d3e1d25ca..5739d16c1ed 100644 --- a/libs/prelude/Prelude/Interfaces.idr +++ b/libs/prelude/Prelude/Interfaces.idr @@ -358,19 +358,25 @@ concatMap = foldMap namespace Bool.Lazy namespace Semigroup + ||| `Lazy Bool` is a semigroup with logical disjunction as an operation. public export [Any] Semigroup (Lazy Bool) where x <+> y = force x || y + ||| `Lazy Bool` is a semigroup with logical conjunction as an operation. public export [All] Semigroup (Lazy Bool) where x <+> y = force x && y namespace Monoid + ||| `Lazy Bool` is a monoid with logical disjunction as an operation and + ||| a delayed `False` as the neutral element. public export [Any] Monoid (Lazy Bool) using Semigroup.Any where neutral = delay False + ||| `Lazy Bool` is a monoid with logical conjunction as an operation and + ||| a delayed `True` as the neutral element. public export [All] Monoid (Lazy Bool) using Semigroup.All where neutral = delay True @@ -391,19 +397,23 @@ or = force . concat @{Any} namespace Bool namespace Semigroup + ||| `Bool` is a semigroup with `||` as an operation. public export [Any] Semigroup Bool where x <+> y = x || delay y + ||| `Bool` is a semigroup with `&&` as an operation. public export [All] Semigroup Bool where x <+> y = x && delay y namespace Monoid + ||| `Bool` is a monoid with `||` as an operation and `False` as the neutral element. public export [Any] Monoid Bool using Bool.Semigroup.Any where neutral = False + ||| `Bool` is a monoid with `&&` as an operation and `True` as the neutral element. public export [All] Monoid Bool using Bool.Semigroup.All where neutral = True @@ -422,19 +432,23 @@ all = foldMap @{%search} @{All} namespace Num namespace Semigroup + ||| `Num` types form a semigroup with addition as an operation. public export [Additive] Num a => Semigroup a where (<+>) = (+) + ||| `Num` types form a semigroup with multiplication as an operation. public export [Multiplicative] Num a => Semigroup a where (<+>) = (*) namespace Monoid + ||| `Num` types form a monoid with addition as an operation and `0` as the neutral element. public export [Additive] Num a => Monoid a using Semigroup.Additive where neutral = 0 + ||| `Num` types form a monoid with multiplication as an operation and `1` as the neutral element. public export [Multiplicative] Num a => Monoid a using Semigroup.Multiplicative where neutral = 1 From aea5102b5f8b45411395959c70ac5e5ab3b5e408 Mon Sep 17 00:00:00 2001 From: oleja Date: Tue, 11 Aug 2026 18:44:12 +0300 Subject: [PATCH 6/9] [ docs ] add documentation for `Traversable` and `Bitraversable` interfaces --- libs/prelude/Prelude/Interfaces.idr | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr index 5739d16c1ed..153e2b26b41 100644 --- a/libs/prelude/Prelude/Interfaces.idr +++ b/libs/prelude/Prelude/Interfaces.idr @@ -602,6 +602,9 @@ namespace Bifoldable bifoldl = foldl .: bifoldl binull fp = null fp || all binull fp +||| Functors representing data structures that can be transformed to +||| structures of the same shape by applying an `Applicative` +||| action on each element from left to right. public export interface (Functor t, Foldable t) => Traversable t where constructor MkTraversable @@ -619,6 +622,9 @@ sequence = traverse id for : Applicative f => Traversable t => t a -> (a -> f b) -> f (t b) for = flip traverse +||| Bifunctors representing data structures that can be transformed to +||| structures of the same shape by applying `Applicative` actions +||| on each element from left to right. public export interface (Bifunctor p, Bifoldable p) => Bitraversable p where constructor MkBitraversable From da91b0f89fbe90c124c1358d763c534ad06b6636 Mon Sep 17 00:00:00 2001 From: oleja Date: Tue, 11 Aug 2026 19:03:21 +0300 Subject: [PATCH 7/9] [ docs ] add documentation for named interface implementations --- libs/prelude/Prelude/Interfaces.idr | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr index 153e2b26b41..40e0120ee84 100644 --- a/libs/prelude/Prelude/Interfaces.idr +++ b/libs/prelude/Prelude/Interfaces.idr @@ -491,27 +491,40 @@ public export %tcinline for_ : Applicative f => Foldable t => t a -> (a -> f b) -> f () for_ = flip traverse_ +||| `Applicative` structures over a `Semigroup` type form a semigroup +||| by lifting the semigroup operation through the `Applicative` structure. public export [SemigroupApplicative] Applicative f => Semigroup a => Semigroup (f a) where x <+> y = [| x <+> y |] +||| `Applicative` structures over a `Monoid` type form a monoid +||| by lifting the monoid operation and the neutral element +||| through the `Applicative` structure. public export [MonoidApplicative] Applicative f => Monoid a => Monoid (f a) using SemigroupApplicative where neutral = pure neutral namespace Lazy + ||| Lazy `Alternative` structures over an arbitrary type form a semigroup + ||| with `<|>` as an operation. public export [SemigroupAlternative] Alternative f => Semigroup (Lazy (f a)) where x <+> y = force x <|> y + ||| Lazy `Alternative` structures over an arbitrary type form a monoid + ||| with `<|>` as an operation and `empty` as the neutral element. public export [MonoidAlternative] Alternative f => Monoid (Lazy (f a)) using Lazy.SemigroupAlternative where neutral = delay empty +||| `Alternative` structures over an arbitrary type form a semigroup +||| with `<|>` as an operation. public export [SemigroupAlternative] Alternative f => Semigroup (f a) where x <+> y = x <|> delay y +||| `Alternative` structures over an arbitrary type form a monoid +||| with `<|>` as an operation and `empty` as the neutral element. public export [MonoidAlternative] Alternative f => Monoid (f a) using Interfaces.SemigroupAlternative where neutral = empty From 504a58921fe1c13a924a984388fd918abb98af0f Mon Sep 17 00:00:00 2001 From: oleja Date: Wed, 12 Aug 2026 01:55:41 +0300 Subject: [PATCH 8/9] [ docs ] fix verb form and quoting in `Applicative` docstrings --- libs/prelude/Prelude/Interfaces.idr | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr index 40e0120ee84..7da1931424a 100644 --- a/libs/prelude/Prelude/Interfaces.idr +++ b/libs/prelude/Prelude/Interfaces.idr @@ -177,17 +177,17 @@ namespace Bifunctor mapSnd = map . mapSnd ||| A functor with application, providing operations to embed -||| pure expressions ('pure') and sequence computations (`<*>`). +||| pure expressions (`pure`) and sequence computations (`<*>`). ||| Abstracts the notion of function application. ||| @ f a parameterised type public export interface Functor f => Applicative f where constructor MkApplicative - ||| Lifts a value into the structure. + ||| Lift a value into the structure. ||| @ f the parameterised type pure : a -> f a - ||| Sequential application. Applies an `Applicative` of functions to + ||| Sequential application. Apply an `Applicative` of functions to ||| a second `Applicative`. ||| ||| ```idris example From 2358deb9055aa8f5b65455ef4671e60d4a198601 Mon Sep 17 00:00:00 2001 From: oleja Date: Fri, 14 Aug 2026 14:53:24 +0300 Subject: [PATCH 9/9] [ docs ] add second example for `<*` Add second example for `<*`, analogous to the `*>` example with `Nothing` to convey that the second effect is used --- libs/prelude/Prelude/Interfaces.idr | 3 +++ 1 file changed, 3 insertions(+) diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr index 7da1931424a..9fd9e47d032 100644 --- a/libs/prelude/Prelude/Interfaces.idr +++ b/libs/prelude/Prelude/Interfaces.idr @@ -201,6 +201,9 @@ interface Functor f => Applicative f where ||| ```idris example ||| (Just 5 <* Just 10) == Just 5 ||| ``` +||| ```idris example +||| (Just 2 <* Nothing) == Nothing +||| ``` ||| @ f the parameterised type public export %tcinline (<*) : Applicative f => f a -> f b -> f a