Skip to content

[ docs ] Improved documentation for Prelude.Interfaces - #3831

Open
user470750 wants to merge 9 commits into
idris-lang:mainfrom
user470750:prelude-interfaces-docs
Open

user470750 wants to merge 9 commits into
idris-lang:mainfrom
user470750:prelude-interfaces-docs

Conversation

@user470750

@user470750 user470750 commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

Description

  • Add documentation for the Applicative interface and the pure, <*>, *>, and <* functions, including code examples. Examples use == in accordance with the documentation style in Prelude.Interfaces.
  • Add documentation for mapHom function following the style of the documentation for bimap, mapFst, mapSnd documentation.
  • Add documentation for Traversable and Bitraversable intefaces.
  • Add documentation for named interfaces implementations.
  • Add documentation for Bifoldable interface following the style of the documentation for Foldable.

Self-check

  • I confirm that this contribution did not involve GenerativeAI nor Large Language Models.

||| A functor with application, providing operations to embed
||| pure expressions (`pure`) and sequence computations (`<*>`).
||| Abstracts the notion of function application.
||| @ f a parameterised type

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

IMO the @ fs are unnecessary here, and busy the docs. They're also not reflected by docs for a and b later

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I based my choice of which arguments to document on the existing documentation for Functor.

@joelberkeley joelberkeley Aug 14, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ah, well I guess I disagree with Edwin there. But yeah it makes sense to copy Functor's style.

||| Sequence actions, discarding the value of the second argument.
|||
||| ```idris example
||| (Just 5 <* Just 10) == Just 5

@joelberkeley joelberkeley Aug 14, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note this example doesn't convey that the second effect is used. The converse of the (*>) example might help

Main> Just 2 <* Nothing
Nothing

It's a shame sth like State wouldn't be suitable here.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for pointing this out, I'll add such an example.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added the second example for <*.

public export
interface Functor f => Applicative f where
constructor MkApplicative
||| Lift a value into the structure.

@joelberkeley joelberkeley Aug 14, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is "structure" always appropriate? What about IO or State? You use Applicative further down, though I don't think that's strictly true either. Is the Applicative not the pure and (<*>), rather than e.g. the Maybe? I'm unsure if Maybe "is an applicative functor" (small "a").

I'm aware that genericity of these interfaces will make it difficult to document them accurately, without it becoming impractically abstract.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For example, the word "structure" is used in the tutorial for Functor:

A functor allows a function to be applied across a structure, for
example to apply a function to every element in a ``List``:

As for the wording "Applicative", I'm using it by analogy with the documentation for Biapplicative though I'm not sure how reliable a source the tests are for documentation wording.
It might make sense to use the same wording ("Applicative") for pure as well, for consistency.
In some of the phrasing, I also looked at Haskell for reference (e.g. "functor with application").
Also for example, the documentation for the functions related to Functor (map, <$>, <&>, etc.) uses the wording "a parameterised type".

Do you have any suggestions for alternative wording instead of "structure" and "Applicative"?

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would guess the haskell docs would be the standard to follow. And they call it a structure, so seems sensible.

Add second example for `<*`, analogous to the `*>` example with `Nothing`
to convey that the second effect is used
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants