Regarding the names: there was some discussion that it would be nice to actually rename Symbol to String (#3103) and have the same names at the type level, especially if we had datakinds at some point. That would be invasive, so we don't necessarily have to do that. But is it at least possible with polykinds/type-in-type now? Can we create one Prim.Natural and have it work at the term and type levels? If so, maybe we could consider adopting term-level Natural into Prelude, with a very small API, and deprecating other packages that define it.

I suppose the problem is that we don't have dedicated natural literals at the term level, so it quickly gets to be a lot of work, sorry.

@MonoidMusician So, if I understand correctly, we can introduce term-level Naturals to mirror the relationship between String and Symbol, right? e.g. Prim introduces the Natural type, then prelude/natural exposes Data.Natural and typelevel-prelude exposes Type.Data.Natural.

It's definitely quite a lot of work but I do think that this would be pretty nice.

I don't see the point of dedicated Sub, Div, Mod classes when these things could just be implemented with functional dependencies on Add and Mul. Am I wrong about that, or is there a reason the former would be better?

More broadly, and probably more controversially, should we be adding new type-level literals ad-hoc like this? As @MonoidMusician reminded us, we're already possibly regretting the separation between Symbol and String. I wonder if in the future we'll want to support all PS literals at the type level, and have a primitive class like

class IsReflectable t v | v -> t where
  reflectType :: forall proxy. proxy v -> t

which would subsume both IsSymbol and IsNat. We'd also be wrestling with the Int versus Nat distinction there.

I bring this up because, if the compiler is going to implement Add and Compare, do we lose anything by using type-level Ints instead of a new Nat kind? I know this was previously discussed here. I'm not strongly swayed by the counterarguments there; they may well be correct, but I might need to see a worked example of something that is made worse or impossible by using type-level ints with appropriate constraints instead of type-level nats. If we can get away with type-level ints, then maybe we should go straight to IsReflectable instead of IsInt, even if we don't implement other type-level literals right now.

I don't see the point of dedicated Sub, Div, Mod classes when these things could just be implemented with functional dependencies on Add and Mul. Am I wrong about that, or is there a reason the former would be better?

Personally, I think that having separate type classes for these operations is much more intuitive than having different fundeps provide different solutions. Row.Cons, for example, is an example of a pretty overloaded type class whose name doesn't really help make its purpose understandable. If we could rename Add/Mul to something that reflects that it can also solve Sub/Div, I'd definitely be more inclined towards this.

I wonder if in the future we'll want to support all PS literals at the type level [...]

We already 2/5 of the non-container literals at the type-level (Boolean, String/Symbol), and so far we've only really gotten it "right" with Boolean. If it is an inevitability, then yeah, I do agree that IsReflectable is what we should go with, to at least help ease future implementations (see also #3102).

[...] do we lose anything by using type-level Ints instead of a new Nat kind? [...]

For use-cases that require non-negative numbers, I agree that Compare is a good compromise over losing the convenience of intrinsically only having natural numbers.

Am I wrong about that, or is there a reason the former would be better?

I'm not sure, but how would you implement Sub using just Add with only one functional dependency of l r -> o, which corresponds to l + r == o? Would you recursively search what the values of r are (e.g. l + 1, l + 2, etc.) until you found a value that worked?

No no, in a Sub-less world, Add would go back to having l r -> o, l o -> r, r o -> l fundeps, and each one would be solved by the compiler with the appropriate expression (o = l + r, r = o - l, l = o - r respectively). For Mul, and for Add as well if we stick to nats and not ints, some constraints will be rejected instead if the result is not a member of the expected domain (Mul 5 r 17, for example, should not have an instance).

I know I already said it, but I'm for Reflectable

By NonZero, you mean something like this?

class NonZero :: Int -> Constraint
class NonZero i

instance Fail (Text "Got a zero!") => NonZero 0
else instance NonZero (i :: Int)

Could the same thing be achieved via an IsZero constraint?

class IsZero :: Int -> Boolean -> Constraint
class IsZero i b | i -> b

class (IsZero i False) <= DivMod ...

Re NonZero etc.: the question is what does any of this get us? DivMod is not going to be implemented by users, so the only point of giving it superclasses is making those superclass instances available in any context where you have a DivMod. If these superclasses are memberless, then the only point of having instances of them is if people design APIs that consume these instances. So show me the designs for APIs that consume NonZero etc.

My reluctance for including DivMod, as I tried to explain in a previous comment, is that there are lots of relationships that are true and expressible just with Compare between numerator, denominator, quotient, and remainder, but only if the sign of the denominator is known. To wit:

• if d > 0, then d > r >= 0
• if d < 0, then d < r <= 0
• if d > 0, then q < 0 iff n < 0
• if d < 0, then q < 0 iff n > 0

Our options are:

1. ignore these relationships, which I think will hinder the utility of DivMod, but that depends on the use cases
2. constrain DivMod to require the denominator, and possibly even the numerator, to be positive, which may also hinder the utility of DivMod but in a different way, again depending on the use cases (but also frees us from having to think about NonZero as a special case)
3. come up with even more type-level stuff to capture the conditionality of these relationships, which I think is probably too speculative to be worth it

The reason I keep saying to hold off on DivMod until we have use cases is that I want to be able to distinguish between 1 and 2. Once we figure out which path is more useful, then we'll know whether we want a NonZero-like thing or not, and then we can bikeshed about how it works.

then the only point of having instances of them is if people design APIs that consume these instances. So show me the designs for APIs that consume NonZero etc.

Good point.

Correct me if I'm wrong, but can't DivMod be added in the future as a non-breaking change? If that's the case, then I'd agree that excluding it for the time being is worth doing. If this PR (without DivMod) gets included in a release, then we'll likely run into more design issues that DivMod would fix besides those mentioned in the Discourse post.

By NonZero, you mean something like this?

Yes, although I haven't added solving for the NonZero constraint yet, it only really exists to constrain DivMod; refactoring to IsZero should also be fairly trivial.

but can't DivMod be added in the future as a non-breaking change?

I'd be more than happy to do this as well. I think having a dedicated issue for it would flesh out the implementation better.

Correct me if I'm wrong, but this should be the final sets of primary changes right? I hope I'm not forgetting anything that was discussed a few weeks back 😄.

So, have we reached consensus that the following changes need to be made before this PR will be merged?

• Rename IsReflectable to Reflectable
• Drop DivMod and NonZero

@JordanMartinez I believe it was solely because of the introduction of the Nat type, which is used by some packages.

I'll be merging master to resolve the conflict here

Looks like there's another merge conflict due to #4239.

Test failures are related to the bundler because of 516abc2, it seems like. Tests for type-level ints are all passing.

Yes, sorry, these failures are indeed not your fault. Because ES module support is currently in development, the tests currently depend on some temporary forks of PureScript libraries that have been changed to be compatible with the new module format, and those forks are getting some cowboy commits at the moment that are breaking everyone else. This will affect local and CI builds (if your local build isn't affected yet, it's because your cached test dependencies haven't expired yet—you have at most a day before this affects you). Please stand by while we restore order.

CI builds now.