Add type classes and `.Instance` modules declaring their instances

[jespercockx]

During the Agda meeting, I identified the following list of typeclasses for which it would be nice to have a .Instances module declaring their instances (some of these would also need the typeclass itself being added to the library):

• [ ] Show (turning things into strings)
• [x] Eq (decidable equality)
• [ ] Ord (decidable ordering)
• [ ] Number (types that admit natural number literals)
• [ ] Fractional (types that admit floating point literals)
• [ ] Quotable (types that we know how to turn into reflected syntax)
• [ ] IsMagma (from Algebra.Structures)
• [ ] IsSemigroup (from Algebra.Structures)
• [ ] IsMonoid (from Algebra.Structures)
• [ ] ... (other structures from Algebra.Structures)
• [ ] TraversableA and TraversableM
• [ ] ProofIrrelevant (for types with at most one element)
• [ ] HasHLevel (for types of a finite h-level)

The following monad transformers should also be given instances of the typeclasses they inhabit:

• [ ] StateT
• [ ] ReaderT

I didn't want to spam the issue tracker with new issues, so I have bundled them here into one. But it would be easy to divide this work among multiple people!

[jespercockx]

See also https://github.com/agda/agda-stdlib/issues/559 for the more general discussion on instance arguments in the standard library.

[gallais]

See #569 #431 for discussions on what a Show class would look like.

[WhatisRT]

We agreed yesterday that moving all the names like _+_, map, etc. that would clash with type classes (and that do clash with other modules right now) into a separate module that isn't imported with everything else is probably a good thing, even if we don't have type classes in v2.0.

We were also discussing the question of using 'algebraic' type classes (like Monoid) versus using 'syntactic' type classes (like has_add in Lean) but didn't come to a conclusion. Orestis just pointed out that using the renaming fields of the algebraic classes to something like + might be a better match for Agda than the style that Lean uses.

[MatthewDaggitt]

We agreed yesterday that moving all the names like +, map, etc. that would clash with type classes (and that do clash with other modules right now) into a separate module that isn't imported with everything else is probably a good thing, even if we don't have type classes in v2.0.

Err I'm afraid I'm not quite sure that's what I got. I thought that the conclusion was that we should have a separate module that imported everything you need for using instances + all the non-clashing original content as well. I don't think we need to go so far as to create a new common base module, which is what I think you're proposing?

Orestis just pointed out that using the renaming fields of the algebraic classes to something like + might be a better match for Agda than the style that Lean uses.

I'm afraid I don't quite remember this point? I thought Oreistis was saying that that was the better solution if one didn't want to use type-classes. Personally I'm strongly in favour of the syntactic style, as the latter doesn't involve heavy-weight dependencies on the Properties files.

[WhatisRT]

Err I'm afraid I'm not quite sure that's what I got. I thought that the conclusion was that we should have a separate module that imported everything you need for using instances + all the non-clashing original content as well. I don't think we need to go so far as to create a new common base module, which is what I think you're proposing?

As I see it there are two approaches. Using Data.Nat as an example and making up some names, we could either have two modules Data.Nat and Data.Nat.Instance where they both export the same names but with one of them using instance arguments and the other not, or there could be three modules, Data.Nat, Data.Nat.Instance and Data.Nat.NoInstance, where the first one exports no names that clash with the other two. To me the latter approach seems more natural, but you're saying the former is a better pick? I'm fine either way.

I'm afraid I don't quite remember this point? I thought Oreistis was saying that that was the better solution if one didn't want to use type-classes. Personally I'm strongly in favour of the syntactic style, as the latter doesn't involve heavy-weight dependencies on the Properties files.

Yes, my writing was probably a bit unclear. This is a new point that came up this morning, and I'm actually still unsure about my opinion. I think I found an issue with this idea of renaming - maybe it's time to write an example module that demonstrates this issue.

It might also be worth pointing out that Lean does both, it has syntactic classes like has_add, but also algebraic ones like Ring. There are some annoying aspects to this mixing, but it generally works quite well.

[MatthewDaggitt]

As I see it there are two approaches. Using Data.Nat as an example and making up some names, we could either have two modules Data.Nat and Data.Nat.Instance where they both export the same names but with one of them using instance arguments and the other not, or there could be three modules, Data.Nat, Data.Nat.Instance and Data.Nat.NoInstance, where the first one exports no names that clash with the other two.

I have to confess I struggle to see the concrete benefits of the latter?