Instance argument agda-stdlib policy?

[xekoukou]

I would like if agda-stdlib used instance arguments. One could place them in different files so as not to contaminate the other files, as suggested by @jespercockx (1)

According to @UlfNorell , you could also hide instance arguments during import. (2)

(I have code that I want to contribute that has instance arguments)

1. https://lists.chalmers.se/pipermail/agda/2018/010699.html
2. https://lists.chalmers.se/pipermail/agda/2018/010698.html

[MatthewDaggitt]

It's clear that there's a lot of demand for this, and putting them in separate modules would alleviate the concern of pollution that has prevented them from being added until now.

Would you like to put together a PR for what Data.Nat.Instance would look like? We can then discuss?

[xekoukou]

If you are asking me to provide rules on how to organize modules with regard to instance resolution, please note that I am very bad at "organizing". I would prefer if others provided the rules and I simply followed them.

Maybe others could take the lead in this one.

[WhatisRT]

Has there been any progress on this issue? I have written a lot of code that uses instance arguments which I would like to put in a pull request (Equality, Monoid, a couple of monad related classes).
My proposal would be to put the definitions (and functions that are defined on top of those classes) in a Class directory, such as Class.Show and then putting instances in *.Instance as previously suggested.

[MatthewDaggitt]

Has there been any progress on this issue?

I'm afraid not. I haven't really used instance arguments extensively myself, but the main requirements as I see it are:

• Instances should be separated out from the non-instance code, because, as I understand it, instances are imported automatically whenever you import a module.
• We should avoid the situation where we end up with parallel instance and non-instance definitions of common library concepts for which the theory then needs to be ported over. For example I'm a bit worried about the parallel definition of _≤_ in Data.Nat.Instance in PR Automated proof of permutation for Fin with instance resolution. #560.

My proposal would be to put the definitions (and functions that are defined on top of those classes) in a Class directory, such as Class.Show and then putting instances in *.Instance as previously suggested.

Would you mind fleshing out your proposal a little? Which definitions and functions would be put in the Class directory? What would the contents of Data.Nat.Instance then look like? Feel free to open a small example PR if that's easier to explain?

[WhatisRT]

• Instances should be separated out from the non-instance code, because, as I understand it, instances are imported automatically whenever you import a module.

Yes. I was hoping that the changes to instance arguments in 2.6 would also imply that this would be fixed, but it seems that this isn't the case (in my opinion the feature should be much more flexible in general, with commands to enable or disable instances at any point, not only when a symbol is first defined).

• We should avoid the situation where we end up with parallel instance and non-instance definitions of common library concepts for which the theory then needs to be ported over. For example I'm a bit worried about the parallel definition of _≤_ in Data.Nat.Instance in PR Automated proof of permutation for Fin with instance resolution. #560.

It would of course be possible to define a copy of something that just has different argument types. I've used this a few times already to get a more fine-grained control of when to use instance arguments.

Would you mind fleshing out your proposal a little? Which definitions and functions would be put in the Class directory? What would the contents of Data.Nat.Instance then look like? Feel free to open a small example PR if that's easier to explain?

In the Class directory, there should be the classes and any functions that depend only on the existance of the class (and its dependencies). So for example, Class/Monad.agda should contain functions such as _>>_, _>=>, void, etc., but not functions that depend on lists for example.

Data.Nat.Instance would export instances of any classes publicly, and other than that would contain only private helpers.

If a couple of classes and instances exist, one could then allow using instance arguments in other places.

I have some code that is already in this structure, so I'll try to make an example PR in the next couple of days.

[jespercockx]

Yes. I was hoping that the changes to instance arguments in 2.6 would also imply that this would be fixed, but it seems that this isn't the case (in my opinion the feature should be much more flexible in general, with commands to enable or disable instances at any point, not only when a symbol is first defined).

TBH I don't really get the problem with instances being in scope for instance search automatically, that's really how it should work since they are anyway 'in scope' under their qualified name. If you have some instances that you really don't want to import then you're likely using them wrong (I think @UlfNorell is with me on this, and he likely has the most experience with using instance arguments in practice).

[MatthewDaggitt]

TBH I don't really get the problem with instances being in scope for instance search automatically, that's really how it should work since they are anyway 'in scope' under their qualified name. If you have some instances that you really don't want to import then you're likely using them wrong (I think @UlfNorell is with me on this, and he likely has the most experience with using instance arguments in practice).

My understanding from the documentation is that instance search only works if there's a unique answer. I'm a bit worried about adding instances all over the standard library and then ending up in a situation where virtually no instance-search has a unique answer. As I said, I haven't used them extensively so in practice maybe this doesn't happen.

[UlfNorell]

The trick is to only add instances that are unique. For instance,

• List is a functor in exactly one way ✅
• Bool is a monoid in (at least) two ways ❌

[WhatisRT]

The code I'm working on right now uses instance arguments basically in two different ways:

• overloading of common notation (show, _≟_, >>=, ...)
• passing arguments that cannot be passed implicitly

The first of these needs instances, while the second might not need them (or can declare them privately).

I use this implicit passing of arguments for monad transformers with classes like MonadState, where most of the time I only care about having the correct class specified as an instance argument, and then once at the entry point of the program I stack a couple of monad transformers on top of each other. In particular, instance argument resolution doesn't seem to be clever enough to resolve the instances for this stack for me (I haven't tried this with 2.6 yet), so I derive the instances explicitly locally (I hope I could convey what I mean, otherwise I can provide an example).

The main point of the previous paragraph is that there is a lot of value in declaring functions that use instance arguments, even if there are no instances that are actually marked with the instance keyword. This would also benefit other things: If a monad class is defined, then even if there are monad instances in the context that are not marked as such, they can be used via instance _ = myMonadInstance.

The trick is to only add instances that are unique. For instance,

• List is a functor in exactly one way ✅
• Bool is a monoid in (at least) two ways ❌

I think this is a good point, but I had some issues with parametrized instances even when they seemed unique. If the instances are defined in a separate file, a project can easily make their own custom prelude that includes whatever instances work.