goldfirere
commented
1 year ago I'd like to hear more about your thoughts on promotion and defunctionalization symbols. It doesn't surprise me that singling is possible. But I worry about promotion. In particular, what's our current stance on promoting/singling code with type applications? If we support that, then we're pretty constrained in how to proceed. But if we don't support that today, then we have more freedom.
Of the two singling approaches you propose, I prefer the second. This would be incompatible with current usage if someone uses visible type application to (redundantly) choose singleton arguments. But singletons hasn't, I think, stressed backward compatibility, so I'm not terribly bothered by this.
Regardless of the approach, there is a non-trivial amount of work here. (It's not all that much, but more than an hour!) Is there good motivation for doing this? (Just seeing how far singletons can go is somewhat decent motivation -- especially if it's what actually motivates you!)
RyanGlScott
Currently,
singletons-thadopts a hard-line stance regarding quantifiers in type signatures. Namely, they must all appear at the top level in this order:With the additional stipulations that:
foralls are permitted. A type likeforall a -> a(with a visibleforall) is not allowed.foralls and contexts are not permitted inctx, theargs, theres, or the kinds of thetvbs.In
singletonsparlance, this sort of type is referred to as a vanilla type. Vanilla types are a subset of rank-1 types, where quantifiers are allowed to appear contravariantly at a depth of at most 1.¹singletons-thdoes not support all rank-1 types, as it will currently reject this one:In #401, I originally came to the conclusion that we should not support anything more sophisticated than vanilla types. Recently, however, I'm reconsidering that stance. One thing that is making me reconsider my stance is the advent of visible
foralls in types, where you can write things like this:This is an exciting step towards full dependent types. Moreover, it would be interesting to support this feature in
singletons. On the surface, it appears simple to support. Here is roughly how the example above would look when promoted:And singled:
Note that when promoted
(type a)simply becomesa, and(type a)isn't changed at all when singled. The most interesting difference when singled is the need to have a separate, invisibleforall (x :: a).after the visibleforall a ->. (More on this in a bit.)As cool as this idea is, it is not possible within
singletons-th's current restriction that all types must be vanilla. What if we relaxed this restriction to allow all rank-1 types, however? Although I decided against this in #401, all of the problematic examples that I came up with are actually rank-2 types, not rank-1. As it turns out, each of the issues that I identified in #401 are manageable when the scope is limited to rank-1 types:Defunctionalization symbols
You definitely can't make defunctionalization symbols for rank-2 or higher of types, as you would need to define
Applyinstances with polytypes as arguments. This just isn't possible in GHC, even with the advent of Quick Look impredicativity.With rank-1 types, we can avoid this problem by applying the workaround described in Wrinkle 2: Non-vanilla kinds in
Note [Defunctionalization game plan]. The trick is that we can still generate defunctionalization symbols for things with non-vanilla types, but we may have to make some sacrifices:foralls, the defunctionalization symbols would put all of theforalls up front to avoid the impredicativity issues described above.foralls, the defunctionalization symbols would turn something likeforall a -> aintoforall a. Type ~> a.For many use cases, these sacrifices are acceptable, as you can still profitably use the defunctionalization symbols even with the slightly different treatment of
foralls.In singled definitions
Singling rank-2 or higher definitions would be tricky, as the examples in #401 demonstrate. Singling rank-1 definitions, on the other hand, would be much more tractable. In today's
singletons-th, the algorithm works roughly like so: given a (vanilla) type signature of the form:The singled type signature would become (roughly):
Where
FandsFare the promoted and singled versions off, respectively. Note that we introduce additionalstype variables to instantiateSingwith. For lack of a better name, I'll call these "Singtype variables".To handle all rank-1 types, this algorithm would need to be generalized slightly to be able to handle nested
foralls and visibleforalls. Here are two possible algorithms for making this work. (Feel free to skip reading the algorithm descriptions if you don't care about the ugly details.)Algorithm 1: The nearest telescope algorithm
Singtype variable in an invisibleforalltelescope directly after the nearestforalltelescope (starting from the::) in which all of the variables in theSingtype variable's kind have been bound by preceding telescopes.Singtype variable telescope appears directly after another invisibleforalltelescope, combine the two telescopes into one.Here are some examples of how this would work:
A vanilla type signature
We need to quantify two
Singtype variables, one for each of the arguments preceding a function arrow. The kinds of theseSingtype variables areaandb, and the nearestforalltelescope that we could pick after whichaandbwould be bound isforall a b.. As a result, we will quantify theSingtype variables directly after this telescope:Then, we would combine the
Singtype variable telescope into the preceding one, which also uses invisibleforalls:This is exactly the same type signature that
sConstwould receive in today'ssingletons-th.An example with nested, invisible
forallsThis time, we need to quantify four
Singtype variables. The first and thirdSingtype variables have kinda, and the nearestforalltelescope that we could pick after whichawould be bound isforall a.. The kind of the secondSingtype variable isb, and the kind of the fourthSingtype variable is(a, b). Because both of these kinds mentionb, the nearestforalltelescope that we could pick after whichbwould be bound isforall b.These constraints give rise to the following type signature:Finally, we combine adjacent invisible
foralltelescopes to get:An example with a visible
forallThe type of
slurmpVisis identical toslurmpexcept that thebis quantified visibly. As a result, theforall b ->andforall (s2 :: b) (s4 :: (a, b)).telescopes would not be combined, resulting in a final singled type signature of:Algorithm 2: The nearest function argument algorithm
Algorithm 1 (the nearest telescope algorithm) is designed to maintain backwards compatibility with
singletons-th's existing treatment offoralls in singled type signatures. However, it is not obvious that Algorithm 1 produces the nicest type signatures for things with nestedforalls. For instance, in the type ofsSlurmpabove, we quantifieds3befores2, which feels somewhat awkward.Algorithm 2 (The nearest function argument algorithm) is an attempt to address this awkwardness. It only has one rule:
Singtype variables_idirectly before the function argumentSing s_i.That's it. There's no mention of telescopes in this algorithm, which makes it conceptually simpler. On the other hand, it does not preserve the existing behavior of how
singletons-thquantifies type variables.Here are the same examples from above, but using Algorithm 2:
A vanilla type signature
would be singled to:
An example with nested, invisible
forallswould be singled to:
An example with a visible
forallwould be singled to:
Either algorithm should suffice, but we will have to think carefully about the tradeoffs involved.
tl;dr It is quite possible to promote and single all rank-1 type signatures, even those with visible
foralls. The downside is that we may have to sacrifice the fidelity of the defunctionalization symbols involved a little. I think this is an acceptable price to pay, but others may feel differently. What are your thoughts?¹For a more formal definition of what a rank-1 type is, see Section 3.1 of Practical type inference for arbitrary-rank types.