goldfirere / singletons

Fake dependent types in Haskell using singletons
287 stars 36 forks source link

Question: singletons-core? #420

Closed googleson78 closed 4 years ago

googleson78 commented 5 years ago

Sorry if this is not the right place to ask!

Question: Would it be desirable/possible to have a separate package with only the TH machinery for generating boilerplate? (+ general-purpose stuff like Sing SingI etc)

Motivation: Currently it takes a lot of time (~10minutes) to compile the entire package, even if I'm not using any of the "builtin" singletonised stuff. My current solution is to just hand-write the little bits I actually need, but I can foresee it quickly becoming overwhelming.

Thanks!

RyanGlScott commented 5 years ago

It's likely possible to do this, but I don't know if it would be desirable.

See the discussion starting at https://github.com/goldfirere/singletons/pull/224#issuecomment-314093372 for a previous debate about this topic, where the conclusion was that separating out the TH machinery into a separate package would not be as clean as one might imagine. The issue is that the Data.Singletons module (which you'd presumably lump under the "singletons-core" label) itself depends on the TH machinery for several of the instances that it defines for SomeSing and TyCon.

We could put these instances into the same hypothetical package that the TH machinery lives in, but then these instances would become orphans, which I find distasteful. The current design is heavyset, yes, but much of it is necessary to restrict the use of orphan instances to internal modules so that any adverse behavior does not leak to the outside world.

goldfirere commented 5 years ago

I actually think that @googleson78 is advocating for a different split.

I think that singletons has 3 parts:

  1. Data.Singletons: no TH, just lots of fancy types.
  2. TH
  3. Libraries

@RyanGlScott observes that it's hard to split 1 and 2 because of orphans. But perhaps we can split 1&2 and 3, which it appears is what @googleson78 wants.

googleson78 commented 5 years ago

From what I understood it's also hard to split 1 and 3 because of orphans?

From this hypothetical "core" library I would want to be able to refer to:

RyanGlScott commented 5 years ago

@googleson78 is right—it's not splitting off 1 from 2 that leads to orphan instance issues, it's splitting off 1 from 3. This is because SomeSing (a central part of the "Working with singletons" section) has instances like these:

SBounded k => Bounded (SomeSing k) 
SEnum k => Enum (SomeSing k)
SEq k => Eq (SomeSing k)
SNum k => Num (SomeSing k)
SOrd k => Ord (SomeSing k)
ShowSing k => Show (SomeSing k)
SIsString k => IsString (SomeSing k)
SSemigroup k => Semigroup (SomeSing k)
SMonoid k => Monoid (SomeSing k)

Unless SomeSing is defined in the same package as SEq, SNum, etc., there is no viable way to define these instances without necessarily introducing orphan instances. We could consider ripping SomeSing out of a hypothetical singletons-core, but then we could lose the ability to define the toSing method of SingKind, so we would have to move that out as well. That's a pretty big schism for the sake of slightly finer package granularity.

goldfirere commented 5 years ago

Right. What would be so bad if we introduce orphans? The big problem with orphans is package clash. I don't see that being a problem here, though... Are there other problems?

RyanGlScott commented 5 years ago

Are there other problems?

Certainly. @googleson78 has indicated a desire to use the Data.Singletons.TH.singletons function—that is, a part of singletons' TH machinery—from the hypothetical singletons core library. This would definitely be a sticking point because the TH machinery must have a certain amount of knowledge about the types living in the "libraries" portion of singletons in order to do their job. For example, any time you write this:

$(singletons [d| data Foo = ... deriving Eq |])

The TH machinery will generate:

Other derivable type classes have similar issues. We could envision a design in which the core singletons library generates code involving the raw names "PEq", "SEq", etc. and expects these names to have been imported from somewhere else. Of course, if you forgot to import these names, you'll get extremely confusing error messages—not to mention that any code that currently derives these instances in a $(singletons [d| ... |]) block will suddenly break.

RyanGlScott commented 5 years ago

Another point in the design space is having the core library just contain (1)—that is, Data.Singletons and nothing else. (2) and (3) (the TH machinery and promoted/singled libraries) would live in a separate library. This has the advantage of avoiding the problem in https://github.com/goldfirere/singletons/issues/420#issuecomment-531203690, as the TH machinery can be aware of the Names in the promoted/singled libraries once more.

As an experiment, I decided to see if this would be possible to implement, and it turns out that it is. You can see the prototype at https://github.com/goldfirere/singletons/tree/singletons-batteries. In this prototype, the core library is named singletons, and the beefy library with all of the extras is called singletons-batteries. The downsides of this approach are:

  1. I have to put orphan instances for SomeSing in a dedicated Data.Singletons.SomeSing module in singletons-batteries, as alluded to in https://github.com/goldfirere/singletons/issues/420#issuecomment-531193798.
  2. Because I don't have access to the TH machinery in the core singletons library, I have to write out quite a few defunctionalization symbols and SingI instances for TyCon{N} by hand. This is certainly doable, albeit rather tedious.

I don't know if this is something anyone (@googleson78 or otherwise) would even want, but it does show that it is possible.

goldfirere commented 5 years ago

Another thought in favor of this separation is that it allows the use of singletons in an environment where TH is not allowed.

I think that we shouldn't do this without a specific client who wants it, though.

epicallan commented 5 years ago

I actually want something close to the separation explained above.

I am writing some code using singletons and the only thing I am largely using is Sing and SingI instance for my types and the in-built ones that come with singleton libraries for lists, tuples and Type. So a trimmed down core providing these which is also compatible with at least the 3 latest GHC releases would be good. I am not even using the TH machinery.

RyanGlScott commented 5 years ago

@epicallan, do bear in mind that the arrangement I propose in https://github.com/goldfirere/singletons/issues/420#issuecomment-531881033 would not give you what you seek, since instances for Sing/SingI would only be available in the full singletons-batteries package.

epicallan commented 5 years ago

@RyanGlScott I get your point. Thanks

Just for FYI

This is what I would have wanted in a small core https://github.com/epicallan/hreq/blob/master/src/Data/Singletons.hs. Its basically what you did in your experiment with a few custom written Sing and SingI instances. I think something like this on hackage would be ideal for people who don't want to have TH in their projects. It could even be a small separate project with in the singleton-eco system if it can't fit right into the current project.

RyanGlScott commented 5 years ago

To reiterate, it's not obvious how to separate the instances that singletons-batteries provides from the TH machinery that produces them. One could conceivably write the code that the TH machinery produces by hand to avoid Template Haskell, but that would come at a steep maintenance cost, since every time one uses genSingletons, you get:

  1. A singled version of the data type
  2. A Sing instance that uses the data type from (1)
  3. A SingKind instance
  4. SingI instances for each data constructor
  5. Defunctionalization symbols for every partial application of each data constructor
  6. SingI instances for each defunctionalization symbol
  7. Promoted versions of each record selector used in a data constructor
  8. Promoted and singled versions of each derived instance
  9. Promoted and singled versions of each associated fixity declaration

That's a lot of code! Not only would it be a lot of work to hand-write this, it would also be easy to forget to keep this code in sync if we ever change some aspect of the way TH code generation works (which happens fairly often).

Moreover, it's not clear to me which instances ought to be privileged enough to live outside of singletons-batteries and in a separate library. Here is a non-exhaustive list of data types that we call genSingletons on:

https://github.com/goldfirere/singletons/blob/b0e0faf5cf8ab9754e1f60a3ce15c801297d3a26/src/Data/Singletons/Util.hs#L39-L60

This includes far more data types than just lists, tuples, and TypeRep. It seems unlikely that we would move all of these instances out of singletons-batteries, but by a similar token, I can't justify only moving a subset of these out either. After all, there's nothing innately special about lists or tuples that sets them apart from other data types in this list—they're all just names to singletons. If we carve out exceptions from this list, I think it would only be a matter of time before people started demanding more exceptions. I don't know where to draw the line.

epicallan commented 5 years ago

I now fully understand the complexity involved, Thanks.

RyanGlScott commented 4 years ago

As one point in the design space, the singlethongs package offers a stripped-down version of singletons that only defines Sing, SingI, SingKind, and bare-bones TH machinery to generate instances thereof.

goldfirere commented 4 years ago

I've often wondered about at least breaking Data.Singletons out into its own package, without TH. That's not quite singlethongs, but doing this would at least allow singletons and singlethongs to build off the same types.

RyanGlScott commented 4 years ago

I've often wondered about at least breaking Data.Singletons out into its own package, without TH.

To be clear, that's exactly what the proposal in https://github.com/goldfirere/singletons/issues/420#issuecomment-531881033 would do. I haven't acted on this yet because thus far, every user testimony in this issue has expressed a desire to put more things in the minimalist package. Perhaps this is a sign that even if we do split off Data.Singletons, there will still be a need for packages like singlethongs, which provide a middle ground between the no-frills minimalist package and the full-fledged singletons-batteries package.

RyanGlScott commented 4 years ago

Perhaps @k0001, the author of singlethongs, can chime in here?

goldfirere commented 4 years ago

I agree that Data.Singletons on its own is hard to use. But it seems sad to force users of singlethongs to be incompatible with singletons.

k0001 commented 4 years ago

I love singletons, thank you all for such an amazing library! Please consider singlethongs a compliment, not competition :)

My most frequent use case for singletons involves using probably less than 1% of what singletons offers: I mostly use it to build strongly-typed RPC services over the network, with help of things like exinst and exinst-aeson. Often, this communication happens between projects that need to be compiled with both GHC and GHCJS at the same time. singletons is always on the bleeding edge of GHC, and GHCJS is always playing catch-up, so getting a particular version of singletons to build with both these compilers is tricky. Also, because of the large amount of TemplateHaskell, singletons takes a very long time to compile in GHCJS.

The current GHCJS is mostly compatible with GHC 8.6, which in theory should be compatible with singletons-2.5.1, but I haven't managed to get that to compile with GHCJS. To be fair, I haven't tried too hard to make the relevant changes necessary to get it to compile, seeing as 2.5.1 is an “old” version of singletons that doesn't seem to be maintained anymore.

I would love to use the same singletons types. I wish there was a singletons-core package or something along those lines. It could be singlethongs itself, even, if you fancy the name and want to put the core things there. It's disappointing to recreate Sing and the like in an incompatible manner. However, for my needs, even if those core types existed in a small library, it must be possible to compile them with both GHC and GHCJS. For example, I'm not sure if the Sing-as-type-family approach used since singletons-2.6 is compatible with the current GHCJS, which is why I went with the previous Sing-as-data-family. I didn't really research this.

Regarding the TemplateHaskell and why I included it in singlethongs: For my use case, where the sum types I treat as singletons have a lot of constructors, writing the boilerplate by hand is very inconvenient. Very. So, having that TH, in my case, is crucial for adoption, even in a core library.

RyanGlScott commented 4 years ago

Thanks for taking the time to respond, @k0001. Your input is extremely valuable, since I can see the reverse dependencies that singletons has, but not the projects that would have used singletons but didn't for reasons like the ones you list.

My most frequent use case for singletons involves using probably less than 1% of what singletons offers

Indeed, that seems to be a common theme from the user testimonies that I have access to. It's proved surprisingly difficult to agree on what that <1% should be, however! I'm hoping that conversations like these can help move towards a consensus on that point.

Also, because of the large amount of TemplateHaskell, singletons takes a very long time to compile in GHCJS.

I feel your pain. I don't even use GHCJS that often and I dread having to compile all of singletons from scratch.

However, for my needs, even if those core types existed in a small library, it must be possible to compile them with both GHC and GHCJS. For example, I'm not sure if the Sing-as-type-family approach used since singletons-2.6 is compatible with the current GHCJS, which is why I went with the previous Sing-as-data-family. I didn't really research this.

I'm surprised to read that GHCJS wouldn't be able to work if Sing is a type family. Do you recall what the issue was? As a quick experiment, I installed GHCJS 8.4 from https://launchpad.net/~hvr/+archive/ubuntu/ghcjs and was able to compile this code without any issue:

```hs {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Demo where import Data.Kind type family Sing :: k -> Type data SList :: forall a. [a] -> Type where SNil :: SList '[] SCons :: Sing x -> Sing xs -> SList (x:xs) type instance Sing = SList type family (xs :: [a]) ++ (ys :: [a]) :: [a] where '[] ++ ys = ys (x:xs) ++ ys = x:(xs ++ ys) (%++) :: forall a (xs :: [a]) (ys :: [a]). Sing xs -> Sing ys -> Sing (xs ++ ys) SNil %++ sys = sys (sx `SCons` sxs) %++ sys = sx `SCons` (sxs %++ sys) ```

I don't have access to GHCJS 8.6, however, so it's possible that there is an issue that is exclusive to that version. I'd nevertheless be shocked if that were the case, however, since GHCJS ought to be able to (at the very least) typecheck any code that GHC can.

Regarding the TemplateHaskell and why I included it in singlethongs: For my use case, where the sum types I treat as singletons have a lot of constructors, writing the boilerplate by hand is very inconvenient. Very. So, having that TH, in my case, is crucial for adoption, even in a core library.

That's quite understandable. Even if we do split off the TH machinery in singletons into its own package, it would still likely be too bulky for your needs. But it's encouraging to hear that it's possible to reimplement a minimal subset of it without too much hassle, and singlethongs could be useful for occupying that niche.


I'm curious to know what your thoughts are on the singletons-batteries design that I proposed in https://github.com/goldfirere/singletons/issues/420#issuecomment-531881033. This would give you a minimalist singletons that contains everything in singlethongs except for the TH bits. But, as I remark above, I don't think that's a dealbreaker, as your TH machinery can be implemented independently of singletons quite easily.

k0001 commented 4 years ago

Thanks for your feedback @RyanGlScott.

I'm surprised to read that GHCJS wouldn't be able to work if Sing is a type family.

As I mentioned, I didn't attempt this, nor did I research whether it was possible at all. I simply kept what singletons-2.5.1 was doing because that approach was the one I was using privately already, which addressed my needs. Also, 2.5.1 was the last singletons version that the changelog advertised as compatible with GHC 8.6, so that kept me from even looking at what >=2.6 was doing differently.

But I'm glad to learn that it works! Thank you for taking the time to do this! I could switch to this approach in singlethongs to reduce the already introduced friction and make it easier to replace singlethongs with singletons when necessary. Or, even better, … (read on) …

This would give you a minimalist singletons that contains everything in singlethongs except for the TH bits.

That sounds great to me! I'll be happy to maintain a very minimal TH in singlethongs if necessary. And if the core singletons ever decides to ship minimal TH bits along these lines, then I'll happily deprecate singlethongs altogether, as it would serve no purpose.

It's not my intention for singlethongs to negatively impact the development of singletons in any way. And as much as possible, if singlethongs really needs to continue to exist, I'll try to make it as easy as possible for it to be a drop-in replacement by reusing the same names, etc.

It's proved surprisingly difficult to agree on what that <1% should be, however!

I suppose one could rename the current singletons to singletons-batteries, create an empty singletons package, and over time move things from singletons-batteries to singletons as necessary. Always keeping in mind that this core singletons package should be more generous than singletons-batteries regarding the GHC/GHCJS versions it supports.

k0001 commented 4 years ago

I suppose one could rename the current singletons to singletons-batteries, create an empty singletons package, and over time move things from singletons-batteries to singletons as necessary. Always keeping in mind that this core singletons package should be more generous than singletons-batteries regarding the GHC/GHCJS versions it supports.

… or, better yet, keep singletons as it is now, and slowly start moving small things to a new package called singletons-core, named as originally suggested in this issue. singletons-core could export everything from a single module Data.Singletons.Core, say, and Data.Singletons from the current singletons module could simply re-export things from there. Those interested only on what the full-blown singletons offers can ignore the new singletons-core altogether.

Also, if this hypothetical core library were to export TH functionality: Other than the cost of maintaining the TH code for multiple template-haskell versions, downstream users wouldn't really be affected by the presence of this code. If they don't want to use TH, they can just not use it. It might be necessary to split the TH into different functions, though. Perhaps singletons-core exports genSingletonsCore that does something along the lines of what singlethongs does, and then the usual genSingletons from singletons composes genSingletonsCore with some extra stuff.

RyanGlScott commented 4 years ago

Always keeping in mind that this core singletons package should be more generous than singletons-batteries regarding the GHC/GHCJS versions it supports.

Of course. The current state of the singletons-batteries branch doesn't reflect this yet, but my intention would be to make the minimalist singletons package support as many GHC releases back as possible. I'm not sure exactly how far back that would be off the top of my head, but I'm fairly confident that we could support back to, say, GHC 8.0 if we so decided. (Some CPP might be required for things like these pattern synonyms, but I don't expect it to be unbearable.)

And if the core singletons ever decides to ship minimal TH bits along these lines, then I'll happily deprecate singlethongs altogether, as it would serve no purpose.

While splitting off Data.Singletons off in a backwards-compatible way is quite doable, I'm less sure about Data.Singletons.TH. I see three problems:

  1. The dependency footprint. singletons' TH machinery crucially relies on th-desugar, which incurs various dependencies.
  2. The reliance on the latest GHC. Data.Singletons.TH uses bleeding-edge GHC features to make its job easier. As one example, Data.Singletons.TH now generates code with StandaloneKindSignatures, which is exclusive to GHC 8.10+. Trying to tweak Data.Singletons.TH to support a range of GHCs is a herculean task that I don't exactly want to take up.
  3. The compile times. Data.Singletons.TH re-exports various things from the Data.Singletons.Prelude.*, which takes up the bulk of the time it takes to compile singletons. This is mostly to ensure that putting import Data.Singletons.TH provides you with everything that the generated code might mention (e.g., deriving Eq would generate code that mentions STrue/SFalse, so Data.Singletons.TH re-exports SBool).

I think (3) is actually quite fixable—we could create a minimal version of Data.Singletons.TH that doesn't re-export anything from Data.Singletons.Prelude.*. (1) and (2), on the other hand, are sticking points that I don't see an easy way to resolve.

RyanGlScott commented 4 years ago

Having thought about this some more, I'd like to put forth a slightly modified version of the proposal in https://github.com/goldfirere/singletons/issues/420#issuecomment-546310379. I'll start my laying by proposing a three-way split of the current singletons library:

  1. A minimal singletons library with no dependencies and a wide GHC support window. This would consist of the following modules:
    • Data.Singletons, but without any instances for SomeSing
    • Data.Singletons.Decide
    • Data.Singletons.ShowSing (on GHC 8.6 or later)
    • Data.Singletons.Sigma
  2. A singletons-th library that contains all of the Template Haskell machinery, but nothing else. This would depend on th-desugar and the latest version of GHC. This would consist of the following modules:

    • Data.Singletons.CustomStar
    • Data.Singletons.TH, but without re-exporting anything from Data.Singletons.Prelude.*
    • Data.Singletons.TH.Options
    • Data.Singletons.SuppressUnusedWarnings

    As well as the following internal modules:

    • Data.Singletons.Deriving.*
    • Data.Singletons.Promote.*
    • Data.Singletons.Single.*
    • Data.Singletons.Names
    • Data.Singletons.Partition
    • Data.Singletons.Syntax
    • Data.Singletons.Utils

    Note that this library will not contain any of Data.Singletons.Prelude.*, which means that any attempt to promote/single code from base is likely to fail. In order to do this, you'll need the third library, which is...

  3. A singletons-base library whose mission is to provide a promoted/singled version of the base library. (Alternatively, we could call this singletons-prelude, but it contains more than just the Prelude.) Again, this would depend on th-desugar and the latest version of GHC. This would consist of the following modules:
    • Data.Singletons.Prelude.*
    • Data.Singletons.TypeError
    • Data.Singletons.TypeLits
    • Data.Singletons.TypeRepTYPE
    • A new Data.Singletons.Prelude.CustomStar, which re-exports Data.Singletons.CustomStar (from singletons-th) plus re-exports of various things from Data.Singletons.Prelude.*. This would be equivalent in functionality to today's Data.Singletons.CustomStar.
    • A new Data.Singletons.Prelude.TH, which re-exports Data.Singletons.TH (from singletons-th) plus re-exports of various things from Data.Singletons.Prelude.*. This would be equivalent in functionality to today's Data.Singletons.TH.
    • A new Data.Singletons.Prelude.SomeSing module for SomeSing's orphan instances, which would also be re-exported from Data.Singletons.Prelude.

Now, let me explain further about why I think this design hits a sweet spot in terms of aligning with various users' needs. The way I see it, users of singletons fall along a spectrum in terms of how much functionality they need.

  1. At one end of the spectrum are those users who want the basic singletons types (i.e., Sing, SingI, SingKind, etc.) and nothing else—no Template Haskell, no TH-generated instances, or anything else of this sort. @phadej has expressed an interest in this elsewhere, as this would allow him to combine his singleton-bool library with the types in singletons. The minimal singletons library above should fill this niche.
  2. Some users want (1) plus a minimal amount of extra goodies. The phrase "extra goodies" is intentionally left vague, as it's proven hard to come to a consensus on what should be included. This ranges from:

    a. A small number of hand-defined Sing/SingI instances, without the need for Template Haskell. (This, as I understand it, is @epicallan's use case.) b. A subset of the Template Haskell machinery that works across multiple versions of GHC. (This is my take on @k0001's singlethongs library.) c. All of the Template Haskell machinery, but without the enormous compile times of the rest of the singletons library. (This, as I understand it, is @googleson78's desire.)

    As I've remarked elsewhere on this issue, it's difficult to fulfill all of these needs simultaneously, and I doubt that I will be able to please everyone here. One thing I can do is implement (2)(c) by splitting off singletons-th into its own library, as the time it takes to compile that portion of the library is quite small compared to the time it takes to compile everything else. Moreover, this schism won't impose a maintenance burden, since it's basically the same code that already exists today, but with a different name.

    (2)(a) is tricky because it's unclear where to draw the line in terms of which Sing/SingI instances should be blessed enough to deserve being implemented by hand. Moreover, this actually would increase the maintenance burden, since we would have to be careful to ensure that these hand-written instances stay in sync with what the Template Haskell machinery generates.

    (2)(b) is tricky because, again, it's hard to figure out where to draw the line in terms of which subset of the Template Haskell machinery should be blessed. The singlethongs library provides one point in the design space, but it's entirely conceivable that others might be annoyed at the things that singlethongs doesn't do (e.g., generating SDecide instances). It's also unclear to me how much CPP would be involved in making this work across multiple GHC versions, but I bet that it wouldn't be pleasant.

    I'll come back to points (2)(a) and (2)(b) a little bit later.

  3. Some users want absolutely everything (i.e., me). They will be the primary consumers of singletons-base.

The three-way split above covers use cases (1) and (3), and partially covers (2). The main downsides, as I see them, are:

  1. It introduces several orphan instances by separating singletons and singletons-base. This is unfortunate, but likely somewhat inevitable. (For what it's worth, most instances in today's singletons library are already orphans internally, but it's impossible to observe this due to the way the module imports are structured.)
  2. It takes an opinionated stance on use case (2). It draws a clear separation between singletons and singletons-th (i.e., the former has absolutely no TH machinery, while the latter has all of it), as well as between singletons and singletons-base (the former does not promote or single any definitions from base whatsoever).

    As a consequence, some users (e.g., advocates of (2)(a) and (2)(b)) might feel a bit left out. I don't think this is a fatal flaw in the design, however, since the existence of singletons as a minimal, standalone library means that others can create their own libraries on top of singletons with different points in the design space. For example, singlethongs can become a small layer on top of singletons. Theoretically, such a library could even be put alongside the other two libraries in this repo (singletons-th and singletons-base), but I would hate for me to become a bottleneck on these libraries' development cycles. Accordingly, I think it would be best for them to be developed independently of this repo.

What do others think of this plan?

goldfirere commented 4 years ago

For me, I think this second point is a blocker, unless I'm assured somehow that it will never happen.

phadej commented 4 years ago

I like the @RyanGlScott proposal. It would be very nice if singletons-bool could be a part where instances are defined without TH. (I can write that). singleton-bool is just too useful alone. (at least for myself = servant).

I.e.

singletons* -> singletons-th -> singletons-base
        \                           ^
           -> singleton-bool* --- /

Packages with * are supporting multiple GHC versions.

singleton-bool supports as old as GHC-7.6, but going up to GHC-8.0 is fine. I'd prefer having around 3 year support window of GHC for singletons (and thus singleton-bool).


Would there be any clients of just singletons-th? As you point out, any generated code is likely to fail.

-- I'd do that in boring business applications which wants to use as GADTs indexes:
$(singletons [d| data MyTag = Tag1 | Tag2 |])

Let me say, I have written manual singletons-like boilerplate a lot. In library code singletons-th would not be that useful, but in business applications (where single GHC is not a limitation) it's often ok.

Yet there is library on hackage, which would be fine with singletons-th AFAICS: https://hackage.haskell.org/package/singleton-nats-0.4.5/docs/src/Data.Nat.html

RyanGlScott commented 4 years ago
  • Right now, suppose someone wants to write package C which uses packages A and B, where A uses singletons and B uses singlethongs. This works fine. Maybe the Sing types leak out a bit, and the author of C has to use qualified imports and or write manual conversions. Annoying, but doable. However, under the plan above, if singlethongs just has a few instances (but not new types), C is hamstrung: the instances clash, and there is no workaround. Note that GHC's lazy detection of instance overlap does not help, because GHC is eager (as it must be) about detecting type instance overlap.

If there are two libraries that both define the same orphan instances for Sing, then you are correct in speculating that these two libraries cannot be used together. I am not quite as pessimistic about this as you are, however, since "orphan-instance packages" are a relatively common convention on Hackage (see, for instance, vector-binary-instances). As long as we clearly mark singletons-base as defining orphan instances, I believe the likelihood of there being Sing collisions is minimal. And if there are collisions between, say, singletons-base and a hypothetical singlethongs-base, these collisions can be easily mitigated by consistently using one orphan-instance package or the other.

RyanGlScott commented 4 years ago

It's also worth noting that the singletons-batteries proposal in https://github.com/goldfirere/singletons/issues/420#issuecomment-531881033 also splits off orphan instances in the exact same fashion that singletons-base does, so this is not a property that is unique to the newer proposal.

iamrecursion commented 4 years ago

Just to weigh in as a user of singletons, there have been a few times where my team has wanted to use parts of singletons, but haven't been willing to pay the compile-time hit. The proposal above would've let us pick and choose the bits we needed at the time, so I'm definitely supportive!

goldfirere commented 4 years ago

Here's an idea that might make me feel better about this: include in singletons-th only those instances and definitions that are required. For example, this would include the promoted and singled Eq class, but it would not include much of the Data.List module. Alternatively, these very basic instances could be included in a new singletons-prim (echoing ghc-prim) package that sits between singletons-th and singletons-base.

It's yet one more package, but it would seem to avoid the instance-clash problem and the compile-times problem in one blow.

RyanGlScott commented 4 years ago

Here's an idea that might make me feel better about this: include in singletons-th only those instances and definitions that are required.

I'm honestly not sure what you mean by "required" here. It's quite feasible to use singleton-th without anything from singletons-base whatsoever. The only difficulty you would run into is if you tried to promote or single code that involved definitions from base, but strictly speaking, singletons-base isn't required to solve this problem. For instance, you can just as well define your own versions of PEq/SEq if you want to use singletons-th to promote/single code involving Eq. In fact, you could even use singletons-th to do so!

Alternatively, these very basic instances could be included in a new singletons-prim (echoing ghc-prim) package that sits between singletons-th and singletons-base.

It's yet one more package, but it would seem to avoid the instance-clash problem and the compile-times problem in one blow.

Echoing my comments in https://github.com/goldfirere/singletons/issues/420#issuecomment-627322533, it's unclear what metric you're using to determine what falls under the label of "very basic". (Each person I've asked in this thread has different ideas about what the basics should be, so it's good to be explicit about this.) More importantly, I fail to see how this would solve the instance-clash problem, since it just shifts the problem to a new package. In the proposal in https://github.com/goldfirere/singletons/issues/420#issuecomment-627322533, users who define their own Sing instances would need to avoid combining their code with singletons-base. In your singletons-prim proposal, users would have to avoid not just singletons-base, but also singletons-prim. I don't see what this buys us.

goldfirere commented 4 years ago

Which instances?

Those which are invoked by code produced by singletons-th. I guess I'm just thinking of deriving code, really. Maybe that's too arbitrary, as you suggest.

More conflicts

But singletons-prim would be the One True Source for those instances, meaning that there wouldn't be clashes.

In any case, I see how this suggestion might be yet one more arbitrary choice, and so I'm happy to go on without it. In the end, I'm happy for you all to decide.

k0001 commented 4 years ago

Maybe trying to answer what's the smallest subset of singletons that deserves to be on its own small “core” package is the wrong quest. Presumably, the reason why folks can't just depend on singletons is not that it is “big”, but that it's tricky to get it (or its dependencies) to compile on their GHC/GHCJS versions. With this in mind, I'd say that the largest subset of singletons that can easily be compiled in multiple GHC/GHCJS version would qualify as a suitable candidate for a “core” package. Perhaps even some of the boilerplate that today is being generated by TH can go in this “core” package in hand-written form, making it easier and faster for it to compile there.

phadej commented 4 years ago

@k0001 good point. If singelons-core provides instances for Bool (handwritten), then singletons-base doesn't need to depend on singleton-bool (which may provide some extra utilities, or could be even deprecated if there aren't any).

RyanGlScott commented 4 years ago

As a general comment, I'd like to note that the bulk of the time singletons takes to compile is not spent splicing Template Haskell code, but rather optimizing the TH-generated code itself. In other words, even if we wrote every line of code in singletons by hand, it would still take a very long time to compile. (I don't have exact numbers to back up this claim, but this was my experience developing verified-classes, a singletons-like library where the vast majority of the code is hand-written.)

Now, in response to more specific comments:

@goldfirere:

Which instances?

Those which are invoked by code produced by singletons-th.

That's actually a vast majority of the instances in singletons, it turns out! Indeed, I can only think of a handful of base-related instances that aren't generated by singletons-th machinery. Mainly the ones in D.S.TypeLits.Internal and D.S.TypeRepTYPE, since they have to be written by hand.

I guess I'm just thinking of deriving code, really. Maybe that's too arbitrary, as you suggest.

That is indeed one way to divide up the instances, although it's not exactly a clean division. There are derived instances sprinkled all throughout D.S.Prelude.*, and moreover, generating these instances in the first place requires that the promoted versions of Bounded, Enum, Eq, Ord, Show, Functor, Foldable, and Traversable all exist. So by the time you've carved out the both the instances and supporting cast necessary to support the instances, you end up with a significant portion of singletons-base anyway.

But singletons-prim would be the One True Source for those instances, meaning that there wouldn't be clashes.

I must not be understanding the intent behind this library correctly. In https://github.com/goldfirere/singletons/issues/420#issuecomment-627935297, you note that the reason underlying your hesitation (paraphrased) is that if a package depends on both singletons-base and another package that defines conflicting Sing instances, then that will result in an error. That is a valid point, but singletons-prim has the exact same issue. Namely, you still wouldn't be able to have a library that combines singletons-prim and the other package that defines conflicting Sing instances.

@k0001:

Presumably, the reason why folks can't just depend on singletons is not that it is “big”, but that it's tricky to get it (or its dependencies) to compile on their GHC/GHCJS versions.

I think it's a little bit of both, actually. There have certainly been folks on this issue discussion who have cited the compile times as a key factor in their unwillingness to use singletons (see here and here for examples). As a result, I think it's important to keep the "core" libraries that we split off from growing too large.

With this in mind, I'd say that the largest subset of singletons that can easily be compiled in multiple GHC/GHCJS version would qualify as a suitable candidate for a “core” package.

I would argue that the minimal singletons library that I propose in https://github.com/goldfirere/singletons/issues/420#issuecomment-627322533 fulfills that criterion. You could hypothetically make singletons-th support multiple GHC versions, but aside from the maintenance difficulties this would impose, adapting to GHC differences would actually impact the user-facing API. Some examples off the top of my head:

I'm sure that there are other complications that I haven't thought of. My point being: maintaining backwards-compatibility in a GHC-extension-heavy library like singletons is hard, and the more things we put into the core subset of it, the more difficult this becomes.

Perhaps even some of the boilerplate that today is being generated by TH can go in this “core” package in hand-written form, making it easier and faster for it to compile there.

For what it's worth, that is already the case in the proposal in https://github.com/goldfirere/singletons/issues/420#issuecomment-627322533, since we'd need to hand-write the defunctionalization symbols for (~>), Apply, etc. by hand. This is rather tedious, of course, so I'd prefer to keep this to a minimum if at all possible, especially since this code would need to be updated manually to stay in sync with singletons-th changes (see "(2)(a) is tricky" in https://github.com/goldfirere/singletons/issues/420#issuecomment-627322533).

goldfirere commented 4 years ago

I think the first part of that last comment is the most interesting:

As a general comment, I'd like to note that the bulk of the time singletons takes to compile is not spent splicing Template Haskell code, but rather optimizing the TH-generated code itself.

That suggests that the folks who care about compile-times have an easy solution: don't optimize. It's far from clear that optimizing singletons code actually yields a runtime improvement, anyway. Or, if it does, that optimization could be saved for release situations.

More concretely, I believe there's a way in cabal files to expose a flag to clients. This flag can control whether -O0 is enabled for the libraries. If this approach satisfies one subset of users clamoring for a split-up of singletons, then we have an easier way forward in figuring out how to do the split.

phadej commented 4 years ago

For me, whether singletons-core uses TH is a deal breaker.

If it would contain any TH splices, fast or not to compile, I won't use it. TH restricts environments where I can compile that code (GHCJS is slow, cross-compiling maybe works, ghc-stage1 -like use cases are out of question).

In other words, I'd like singletons-core to become "foundational library" (= whether it's bundled with GHC is more of social discussion than technical one), but if it uses TH, it just cannot be.

RyanGlScott commented 4 years ago

For me, whether singletons-core uses TH is a deal breaker.

I was hoping that someone would chime in with this opinion, since this shows that while compile times are one important factor that hinders singletons' adoption, it's certainly not the only factor. There are multiple itches that a minimal singletons library would need to scratch.


Just for the sake of having some numbers to point to, I performed a quick experiment where I compiled singletons (commit 5f8f2b418989ba0109e965f634f0cf7a850f9191) with -O0 and with -O1 (the default with cabal-install). Here are the results on my machine with GHC 8.10.1:

It looks like enabling -O0 cuts the compilation times by approximately half, which is certainly a sizeable gain. But then again, it's not a cure-all, since it still takes over a minute to compile the whole library. In short, I agree that it would be worthwhile to advertise this -O0 trick as a potential way to lessen the symptoms, but it's no substitute for a minimal version of singletons.

RyanGlScott commented 4 years ago

I've submited a PR which implements the proposal in https://github.com/goldfirere/singletons/issues/420#issuecomment-627322533 at #463. Any feedback you could provide on the design would be appreciated.