Swap Aeson for JSON

[tbidne]

Following up on this idea from the Call to Arms:

Some dependencies can be replaced with simpler ones. For instance, aeson could be replaced with json.

I've spent the past couple days trying this. It's mostly straightforward, though there are some nuances.

• JSON is bidirectional, as opposed to aeson's split FromJSON/ToJSON. This means where some types only have a ToJSON, we either need to use error or add analogous FromJSON functionality. I've chosen the latter for now, mainly because of a reluctance to use error, and having both means testing can be more robust (roundtrips).

Anyway, I wanted to open an issue for this before a PR, in case some discussion is warranted. Otherwise I'll press on.

[facundominguez]

Hello @tbidne. Thanks for trying this. I explored json in liquid-fixpoint here and tried it partially in liquidhaskell.

I've chosen the latter for now, mainly because of a reluctance to use error, and having both means testing can be more robust (roundtrips).

I don't have a strong feeling on this.

Something that gave me pause, though, is that I found large data structures being serialized and deserialized from json in LH. I don't remember which structures now but we'll come across them if we explore it again. The json package might make these operations noticeably slower. If we can confirm this, perhaps we should consider making the features that aeson supports optional, instead of trying to replace it with json.

Let me know what you think.

[tbidne]

My attempts are here:

• lh-fixpoint
• lh

The primary difference between it and yours is implementing the readJSON functions, and subsequent tests. This is why the diff is so much larger.

---

According to my CI --dry-runs (with aeson, with json), aeson is dragging in 13 extra packages:

• generically
• indexed-traversable-instances
• integer-conversion
• network-uri
• OneTuple
• semialign
• strict
• text-iso8601
• text-short
• these
• time-compat
• uuid-types
• witherable

This significantly decreases the motivation to switch IMO, when you consider aeson's advantages (de-facto standard, properly split FromJSON/ToJSON), and the possible downsides (potential performance regressions, as you say).

Putting aeson behind a flag is a nice idea, though. I have appreciated this when other packages have done it (e.g. refined). The only downside is how much the cpp degrades the code, but seems worth a try to me.

[facundominguez]

The only downside is how much the cpp degrades the code, but seems worth a try to me.

If aeson is used in a localized place in LH, then we could dump all the necessary instances in a single module near the place they are needed. Then we can avoid CPP by conditionally including the module with cabal flags. e.g.

other-modules: Language.Haskell.Liquid.AesonFeature
if flag(enable-aeson)
  hs-source-dirs: actual-aeson-feature
else
  hs-source-dirs: aeson-feature-dummy

[facundominguez]

I edited my description of the cabal configuration to something more sensible :) But we still need to earn clarity on what features in LH depend on aeson.

[tbidne]

I tried it out here: lh, lh-fixpoint (no single module, just cpp directly where needed). It appears json is used in the following places:

• Optional liquid-fixpoint output
• benchmark-timings (mix of csv and json)
• lh output (reportResultJson is called as part of its normal operation)
• Saving / loading results
• Curiously, Language.Haskell.Liquid.UX.Server.getType, which decodes a json file to AnnMap, does not appear to be in use anywhere.

[facundominguez]

Those patches are helpful to identify the json uses indeed.

lh output (reportResultJson is called as part of its normal operation)

This might be used by a text editor according to liquidhaskell/CHANGES.md. The output in the case of lh can be at least as large as to describe an annotated source code. They need to be requested with --json at the moment.

Looks like this feature could be disabled if not building with aeson.

Optional liquid-fixpoint output

This might be connected to the above, it was introduced in 19c22adc. The results are pretty small in general, so this could be done with the json package.

@ranjitjhala, do you have any insights about how these features are being used today?

Saving / loading results

Perhaps these refer to the --diffcheck feature. At least functions loadResult and saveResult appear in the module Language.Haskell.Liquid.UX.DiffCheck.

Looks like this feature could be disabled if not building with aeson.

benchmark-timings (mix of csv and json)

The json here looks rather small as well. This could still be candidate to switch to the json package.

Curiously, Language.Haskell.Liquid.UX.Server.getType, which decodes a json file to AnnMap, does not appear to be in use anywhere.

Well spotted. It became dead code after 955c9eb. I'm removing it in #2250.