Add JSON manipulation functions

[madman-bob]

Add JSON Eq interface, and lookup, update, and traversal functions.

[gallais]

Is the order of the entries in the JObject supposed to matter?

[madman-bob]

Good catch. It varies between implementations, but I'm a fan of the order not mattering.

The tests are failing because lsp-lib defines its own Eq JSON. I'm not sure how to work around this.

[gallais]

Ping @stefan-hoeck. How do you want to proceed? Is this a sign to fork json out of contrib? 👼

[stefan-hoeck]

Ping @stefan-hoeck. How do you want to proceed? Is this a sign to fork json out of contrib? 👼

Tricky one. Obviously, idris2-lsp depends on the JSON part of contrib and defines its own implementation of Eq, which leads to the error we are observing here (see here). So, in order for JSON to go out of contrib, idris2-lsp would have to be adjusted accordingly (I'm not one of the lsp maintainers), but it would also have to be adjusted to use the new Eq implementation from this PR before this PR would be merged.

As for external options: There is idris2-json with a parser that is an order of magnitude faster than the one from contrib plus automatically derivable marshallers (with a customizable deriving mechanism). So, there are already viable external options that are at least on par with what is offered in contrib.

My personal opinion is to no longer accpect new stuff into contrib if we ever want to get rid of it.

[madman-bob]

Your two external libraries are both JSON parsing libraries. Neither library has JSON manipulation features. For my immediate problem, I've got a large JSON object, that I'm making a small tweak to, before outputting it again. Encoding the full schema in Idris is overkill.

Taking a step back, I'm a fan of the "batteries-included" approach. So I'd prefer a basic JSON library in base.

As for contrib, I agree that we shouldn't accept entirely new modules. But we should still maintain existing modules, until we're ready to deprecate them.

[mattpolzin]

We can ignore the CI failure of LSP-lib for the purposes of this PR and I’ll fix that lib after this merges; the CI job will have served its purpose in giving a heads up about the breaking change at least.

I had assumed (based partly on the contrib reorganization document in the wiki) that the contrib JSON module would move to a new repo under idris-community in time. I don’t see any inherent problem in that package coexisting with Stefan’s package, though ideally the two would not have the same name for obvious reasons.

RE the idea of moving JSON to base: although I don’t have strong opinions of my own, I’ll mention Edwin’s intention that base be light weight and not batteries included so that we can weigh that as well. I’ve always considered his word to carry the most weight, but that’s just me.

[mattpolzin]

Sidenote: The specific error that comes out is a bit surprising. Rather than complaining about finding multiple Eq it complains it can't find specifically Eq (List JSON) while evaluating the JArray case of Eq JSON. I can't imagine the problem is anything other than ambiguity in fact, just an odd place for the compiler to get confused in that particular way.

[stefan-hoeck]

Your two external libraries are both JSON parsing libraries. Neither library has JSON manipulation features. For my immediate problem, I've got a large JSON object, that I'm making a small tweak to, before outputting it again. Encoding the full schema in Idris is overkill.

Taking a step back, I'm a fan of the "batteries-included" approach. So I'd prefer a basic JSON library in base.

As for contrib, I agree that we shouldn't accept entirely new modules. But we should still maintain existing modules, until we're ready to deprecate them.

About moving Language.JSON to base: That would mean to also move some parsing capabilities to base. That's not exactly lightweight. But that's just my opinion and others should decide how to proceed.

If you'd like to add JSON-manipulating capabilities to idris2-json, I'll be happy to accept PRs. Ideally, JSON manipulation would be implemented via optics. We have libraries for those as well. Again, with auto-deriving included.

[andrevidela]

I'm also a fan of batteries-included languages but Idris isn't one. I think we should get this in because I can't believe we don't have any way to equate and update json files by default. But we should definitely start moving documentation away from contrib and into other libraries like idris2-json

[mattpolzin]

If I've collected thoughts above correctly, the only comment in opposition to merging this PR is:

My personal opinion is to no longer accpect new stuff into contrib if we ever want to get rid of it.

I generally agree (and think that's roughly the consensus others have reached as well), though I would interpret the sentiment much the same as this comment (also from above):

As for contrib, I agree that we shouldn't accept entirely new modules. But we should still maintain existing modules, until we're ready to deprecate them.

So, I think if we go another day or so without more conversation on this changeset, someone ought to merge it.

The only thing stopping us from moving contrib's JSON to its own repo is a volunteer to do the work. If we want to deprecate instead of relocate, that might take a bit more coordination. I'm ok either way, but it almost sounds easier to me to move the JSON module from contrib into its own repo and name it something arbitrary like og-json so folks can transition their projects from using contrib to using that new package trivially (not withstanding the fact that the new package won't ship with the compiler) -- and that doesn't preclude us from pushing people toward using a different JSON library as the community recommendation.

[jfdm]

Some thoughts, especially as @madman-bob is not the only one who uses the JSON from contrib, and a gentle reminder that there are those of us who use Idris for research and would like to be conservative in our library usage (fast moving third party libraries are not great; stability is good).

For a long time, we (the small group of us at the very beginning) did see Idris as being towards the 'batteries included' side of things. The rationale being that making Idris quicker to get going (i.e. 'whip-it-up-atude') was more beneficial than having to navigate through dependencies and different packages. The latter could be done later. Our attitude did mean that contrib grew more than it probably should have. Moreover, with how the Communities surrounding Idris have grown, having a 'single' contrib attached to the base installation can be argued as no longer ideal/practical.

Whilst I am not looking to keep contrib alive, I do agree that it also would be worth our while to ensure that contrib is at least maintained. I disagree that its contents should be deprecated in favour of external third-party libraries. I disagree that it should be moved to its own external repo.

Perhaps an intermediate solution would be to move the JSON library (and parsing and prettying printing /ex cetera/) to a separate package within the base installation (as we do with linear and networking). This way the original 'batteries' are there if people do require them, and if they want something more substantial they can be pointed in the right direction.

[mattpolzin]

Perhaps an intermediate solution would be to move the JSON library (and parsing and prettying printing /ex cetera/) to a separate package within the base installation

I've had this thought before just purely for the fact that it may be a lighter lift for the implementor as a first step, so I am definitely not opposed to us taking that first step without having decided concretely how long we wait after that to take the second step. I mean, I'm not even personally opposed to deciding that JSON in particular is an important thing to ship alongside the compiler as a builtin library (past the point where other more tertiary contrib modules have been moved to other repos). Seems to me that the first step is agreeable to both ends of the spectrum (from batteries included all the way to super light-weight).