andrewthad / quantification

Data types and type classes for universally and existentially quantified types
4 stars 3 forks source link

Does quantification really need to many dependencies? #9

Open edemko opened 10 months ago

edemko commented 10 months ago

(Hey lookatthat, I'm doing code things again 0o0 Anyway...)

I just wanted to pull in the Exists type real quick, but instead I also had to wait for the notoriously expensive aeson compile. While it's merely a time-wasting issue, on reflection it seems a little unusual that a type theoretic primitive would require so many dependencies. /understatement I could have just implemented a simple Exists by hand without so much as the prelude!, and it probably would have taken less time than waiting for aeson 🙃

Would you be amenable to splitting out a new quantification-aeson library from quantification? Or even pulling a quantification-core library out that just defines the Exist* types and some instances? Obviously, this will mean creating orphan instances, but the way I see it: that's just what happens when Alice and Bob independently write libraries (the concept of existential quantification, and then aeson), and then Charlie wants to use both of their work meshed together (how quantification currently stands).

andrewthad commented 10 months ago

The aeson thing is annoying and also causes some kind of build plan failure about once a year since aeson keeps tweaking its API. I'd be fine with moving the aeson instances to a separate package as orphan instances. Fortunately, this repository is already structured as a multi-library repo, so if you PR a change adding a quantification-aeson library that exposes a Data.Exists.Aeson module (with orphan instances and all the FromJSONForall stuff), I'd accept that.

Related thoughts:

edemko commented 9 months ago

I've gone ahead and pulled out the aeon-related stuff as described (#10). As far as the other thoughts: