Include laws for Functor, Applicative, Monad

[alex-mckenna]

Currently, the modules for Functor, Applicative and Monad include records for the Raw types similar to the algebraic structures, but do not have corresponding types including the laws. I think this could be a nice issue for someone like myself who knows the laws, and wants to take a gentle first step into contributing to the standard library.

From what I can tell this would involve:

• Creating a Category.Structures module for definitions of IsFunctor, IsApplicative and IsMonad
• Creating the extended records which include proof the laws hold

[alex-mckenna]

@gallais Any comments / gotchas I should know about with this?

[gallais]

Any comments / gotchas I should know about with this?

The right notion of equality to use in these is a hard question. E.g. you'll probably need
functional extensionality to prove the laws for State if you pick PropositionalEquality
as your notion of equality.

[HuStmpHrrr]

i think this is a good issue. I was wondering the same thing too.

[jespercockx]

It would be great if someone could take a look at this! It is kind of embarrassing to claim one of the big advantages of Agda over Haskell is the ability to specify lawful typeclasses, but then the standard library does not actually do this.

[JacquesCarette]

I was hoping to start migrating the basic parts of agda-categories to agda-stdlib, so that Category, Functor and friends could be 'right'. I think that things in agda-categories have settled, so that once stdlib-1.3 ships, that could start.

[jamesmckinna]

... fast-forward to v2.x and the year 2024... UPDATED: and suggest removing the low-hanging-fruit label!

[JacquesCarette]

Right, this serves as a nice reminder for me to start a design discussion on just that.