Skip to content

Functor and Applicative laws for core library types - #3850

Closed
joelberkeley wants to merge 2 commits into
idris-lang:mainfrom
joelberkeley:laws
Closed

joelberkeley wants to merge 2 commits into
idris-lang:mainfrom
joelberkeley:laws

Conversation

@joelberkeley

@joelberkeley joelberkeley commented Aug 26, 2026

Copy link
Copy Markdown
Contributor

Description

The functor and applicative laws for common library types. I am missing some applicative laws for list/snoclist, cos they're non-trivial. I could also add monad laws. I don't know if I'll get round to them (let's assume not). Laws from here https://en.wikibooks.org/wiki/Haskell/Applicative_functors. PLEASE CORRECT ME IF I'VE INTERPRETED THEM WRONG.

This is a draft to get opinions before I invest effort needlessly.

It's quite unclear what types make sense to implement these for. I originally asked about Prelude types, which doesn't include Vect. Unfussed if we include that or not. It's quite hard to know where the line is (what about List1, State etc.).

Could do just the functor laws for now - they're always easy.

Self-check

  • This is my first time contributing, I've carefully read CONTRIBUTING.md
    and I've updated CONTRIBUTORS with my name.
  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG_NEXT.md
  • I confirm that this contribution did not involve GenerativeAI nor Large Language Models.

@joelberkeley
joelberkeley deleted the laws branch August 27, 2026 11:15
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.

1 participant