singletons
singletons copied to clipboard
goldfirere
Consider allowing promotion and singling of all rank-1 types
Currently, singletons-th adopts a hard-line stance regarding quantifiers in type signatures. Namely, they must all appear at the top level in this order:
forall tvb_1 ... tvb_m. ctx => arg_1 -> ... arg_n -> res
With the additional stipulations that:
- Only invisible
foralls are permitted. A type likeforall a -> a(with a visibleforall) is not allowed. - Nested
foralls and contexts are not permitted inctx, theargs, theres, or the kinds of thetvbs.
In singletons parlance, 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-th does not support all rank-1 types, as it will currently reject this one:
const2 :: forall a. a -> forall b. b -> a
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:
-- Definition:
idv :: forall a -> a -> a
idv (type a) x = x :: a
-- Usage:
n :: Bool
n = idv (type Bool) True
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:
-- Definition:
type Idv :: forall a -> a -> a
type family Idv a x where
Idv a x = x :: a
-- Usage:
type N :: Bool
type family N where
N = Idv Bool True
And singled:
-- Definition:
sIdv :: forall a -> forall (x :: a). Sing x -> Sing (Idv a x)
sIdv (type a) (sX :: Sing x) = sX :: Sing (x :: a)
-- Usage:
sN :: Sing N
sN = sIdv (type Bool) STrue
Note that when promoted (type a) simply becomes a, and (type a) isn't changed at all when singled. The most interesting difference when singled is the need to have a separate, invisible forall (x :: a). after the visible forall 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 Apply instances 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:
- For types with nested
foralls, the defunctionalization symbols would put all of theforalls up front to avoid the impredicativity issues described above. - For types with visible
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:
f :: forall tvb_1 ... tvb_m. arg_1 -> ... arg_n -> res
The singled type signature would become (roughly):
sF :: forall tvb_1 ... tvb_m
(s_1 :: arg_1) ... (s_n :: arg_n).
Sing s_1 -> ... -> Sing s_n -> Sing (F s_1 ... s_n :: res)
Where F and sF are the promoted and singled versions of f, respectively. Note that we introduce additional s type variables to instantiate Sing with. For lack of a better name, I'll call these "Sing type variables".
To handle all rank-1 types, this algorithm would need to be generalized slightly to be able to handle nested foralls and visible foralls. 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
- Quantify each
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. - If a
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
const :: forall a b. a -> b -> a
We need to quantify two Sing type variables, one for each of the arguments preceding a function arrow. The kinds of these Sing type variables are a and b, and the nearest forall telescope that we could pick after which a and b would be bound is forall a b.. As a result, we will quantify the Sing type variables directly after this telescope:
sConst :: forall a b.
forall (s1 :: a) (s2 :: b).
Sing s1 -> Sing s2 -> Sing (Const2 s1 s2 :: a)
Then, we would combine the Sing type variable telescope into the preceding one, which also uses invisible foralls:
sConst :: forall a b (s1 :: a) (s2 :: b).
Sing s1 -> Sing s2 -> Sing (Const2 s1 s2 :: a)
This is exactly the same type signature that sConst would receive in today's singletons-th.
An example with nested, invisible foralls
slurmp :: forall a.
a ->
forall b.
b -> a -> (a, b) -> a
This time, we need to quantify four Sing type variables. The first and third Sing type variables have kind a, and the nearest forall telescope that we could pick after which a would be bound is forall a.. The kind of the second Sing type variable is b, and the kind of the fourth Sing type variable is (a, b). Because both of these kinds mention b, the nearest forall telescope that we could pick after which b would be bound is forall b. These constraints give rise to the following type signature:
sSlurmp :: forall a.
forall (s1 :: a) (s3 :: a).
Sing s1 ->
forall b.
forall (s2 :: b) (s4 :: (a, b)).
Sing s2 -> Sing s3 -> Sing s4 -> Sing (Slurmp s1 s2 s3 s4 :: a)
Finally, we combine adjacent invisible forall telescopes to get:
sSlurmp :: forall a (s1 :: a) (s3 :: a).
Sing s1 ->
forall b (s2 :: b) (s4 :: (a, b)).
Sing s2 -> Sing s3 -> Sing s4 -> Sing (Slurmp s1 s2 s3 s4 :: a)
An example with a visible forall
slurmpVis :: forall a.
a ->
forall b ->
b -> a -> (a, b) -> a
The type of slurmpVis is identical to slurmp except that the b is quantified visibly. As a result, the forall b -> and forall (s2 :: b) (s4 :: (a, b)). telescopes would not be combined, resulting in a final singled type signature of:
sSlurmpVis :: forall a (s1 :: a) (s3 :: a).
Sing s1 ->
forall b ->
forall (s2 :: b) (s4 :: (a, b)).
Sing s2 -> Sing s3 -> Sing s4 -> Sing (SlurmpVis s1 b s2 s3 s4 :: a)
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 of foralls in singled type signatures. However, it is not obvious that Algorithm 1 produces the nicest type signatures for things with nested foralls. For instance, in the type of sSlurmp above, we quantified s3 before s2, which feels somewhat awkward.
Algorithm 2 (The nearest function argument algorithm) is an attempt to address this awkwardness. It only has one rule:
- Quantify each
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-th quantifies type variables.
Here are the same examples from above, but using Algorithm 2:
A vanilla type signature
const :: forall a b. a -> b -> a
would be singled to:
sConst :: forall a b.
forall (s1 :: a). Sing s1 ->
forall (s2 :: b). Sing s2 ->
Sing (Const s1 s2 :: a)
An example with nested, invisible foralls
slurmp :: forall a.
a ->
forall b.
b -> a -> (a, b) -> a
would be singled to:
sSlurmp :: forall a.
forall (s1 :: a). Sing s1 ->
forall b.
forall (s2 :: b). Sing s2 ->
forall (s3 :: a). Sing s3 ->
forall (s4 :: (a, b)). Sing s4 ->
Sing (Slurmp s1 s2 s3 s4 :: a)
An example with a visible forall
slurmpVis :: forall a.
a ->
forall b ->
b -> a -> (a, b) -> a
would be singled to:
sSlurmpVis :: forall a.
forall (s1 :: a). Sing s1 ->
forall b ->
forall (s2 :: b). Sing s2 ->
forall (s3 :: a). Sing s3 ->
forall (s4 :: (a, b)). Sing s4 ->
Sing (SlurmpVis s1 b s2 s3 s4 :: a)
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.
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!)
what's our current stance on promoting/singling code with type applications?
Our current stance is that singletons doesn't support type applications, and it will promote code like f @a x to F x. See this section of the README. As a result, we have the freedom to cut corners.
As that section of the README explains, we do try our best to preserve the order of foralls in type signatures whenever possible, but there are certain Haskell constructs for which this is not really possible. Defunctionalization symbols are a notable example of this: there is no sensible way to take const2 :: forall a. a -> forall b. b -> a and give it a defunctionalization symbol Const2Sym0 :: forall a. a ~> (forall b. b ~> a) for the reasons described in #401. This limitation seems pretty fundamental, and I can't think of a way to preserve the order of the foralls in the defunctionalization symbol (short of replacing defunctionalization with some other mechanism entirely).
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.
Indeed, I also prefer the second approach for the same reasons that you list.
Is there good motivation for doing this?
"Good" is subjective, but I am very keen to add support for visible dependent quantification in terms to singletons, for which this issue is a prerequisite. VDQ in terms is a stepping stone for full dependent types, and being able to promote/single types with forall a -> quantifiers would avoid the need for ugly kludges involving Proxy or TypeRep. (See this related issue.)
Additionally, I am definitely curious to see how far singletons can go in this particular direction. The decision to only permit prenex types in #401 has always struck me as a bit too conservative, and I wonder how many of our current assumptions can be relaxed.
I've been working on this issue for a while, and in the process of doing so, I've gained a better understanding of the code that governs how type variable binders are singled. This new insight has led to a number of simplifications to the code (see #545, #547, #551, and #550, as well as the respective fixes in #548, #549, #552, and #553). In this regard, I consider this issue to have been quite lucrative.
Unfortunately, I think I will have to admit defeat on the end goal of actually implementing the plan described in https://github.com/goldfirere/singletons/issues/542#issue-1446513186 — at least for now. The problem is that there is no way to uniformly implement the plan in all forms of type signatures. There are two places where the plan falls apart:
-
GADT constructor types. GHC flat-out disallows nested
foralls in the syntax of GADT constructors, so it would be impossible to write something like this:$(singletons [d| data Foo a b = MkFoo a b |]) -- ==> data SFoo z where SMkFoo :: forall a b. forall (x :: a). Sing x -> forall (y :: b). Sing y -> SFoo (MkFoo a b)Lifting this restriction would require fixing GHC#18389 first.
If this were the only obstacle, then I wouldn't be too bothered with just having a special case for data constructors, as they are quite special already. However, this isn't the only place where nested
foralls cause issues... -
Class method defaults. This one really surprised me, and it takes some explanation to see what goes wrong. First, consider a type class where the methods have default implementations, such as
Eq:$(singletons [d| class Eq a where (==) :: a -> a -> Bool x == y = not (x /= y) (/=) :: a -> a -> Bool x /= y = not (x == y) |])In today's
singletons-th, the generatedSEqclass will have default signatures for each of the method defaults:class SEq a where (%==) :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (x == y) default (%==) :: forall (x :: a) (y :: a). ((x == y) ~ Not (x /= y)) => Sing x -> Sing y -> Sing (x == y) sx %== sy = sNot (sx %/= sy) (%/=) :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (x /= y) default (%/=) :: forall (x :: a) (y :: a). ((x /= y) ~ Not (x == y)) => Sing x -> Sing y -> Sing (x /= y) sx %/= sy = sNot (sx %== sy)Note the equality constraints (e.g.,
(x == y) ~ Not (x /= y)) in each of the default type signatures, which are crucial to making the default implementations typecheck. Importantly, each of these equality constraints must mention bothxandy.Now imagine what would happen if we instead generated the types of
SEq's methods according to the plan above. It would look something like this:class SEq a where (%==) :: forall (x :: a). Sing x -> forall (y :: a). Sing y -> Sing (x == y) default (%==) :: forall (x :: a). Sing x -> forall (y :: a). Sing y -> ((x == y) ~ Not (x /= y)) => Sing (x == y) sx %== sy = sNot (sx %/= sy) (%/=) :: forall (x :: a). Sing x -> forall (y :: a). Sing y -> Sing (x /= y) default (%/=) :: forall (x :: a). Sing x -> forall (y :: a). Sing y -> ((x /= y) ~ Not (x == y)) => Sing (x /= y) sx %/= sy = sNot (sx %== sy)This class definition does typecheck, but we are on thin ice. In fact, the ice breaks completely when we try to define an instance of
SEqthat relies on one of these method defaults, e.g.,instance SEq Bool where SFalse %== SFalse = STrue STrue %== STrue = STrue SFalse %== STrue = SFalse STrue %== SFalse = SFalseThis will fail to typecheck with:
Bug.hs:78:10: error: • Couldn't match type: (Not (x == y) ~ Not (x == y)) => SBool (Not (x == y)) with: SBool (Not (x == y)) Expected: Sing x -> forall (y :: Bool). Sing y -> Sing (x /= y) Actual: Sing x -> forall (y :: Bool). Sing y -> ((x /= y) ~ Not (x == y)) => Sing (x /= y) • In the expression: Bug.$dm%/= @(Bool) In an equation for ‘%/=’: (%/=) = Bug.$dm%/= @(Bool) In the instance declaration for ‘SEq Bool’ • Relevant bindings include (%/=) :: Sing x -> forall (y :: Bool). Sing y -> Sing (x /= y) (bound at Bug.hs:78:10) | 78 | instance SEq Bool where | ^^^^^^^^Ouch! What happens here is that under the hood, GHC is filling in a default implementation for
(%/=)roughly like so:defaultImpl :: forall a. SEq a => forall (x :: a). Sing x -> forall (y :: a). Sing y -> ((x /= y) ~ Not (x == y)) => Sing (x /= y) defaultImpl sx sy = sNot (sx %== sy) instance SEq Bool where SFalse %== SFalse = STrue STrue %== STrue = STrue SFalse %== STrue = SFalse STrue %== SFalse = SFalse (%/=) = defaultImplThe
(%/=) = defaultImpldoes not typecheck under simplified subsumption, however. It would typecheck if GHC instead generated code likex %/= y = defaultImpl x y, butDefaultSignaturesdoes not attempt to eta expand default implementations like this. I even asked if GHC could do this for you in GHC#19432, but the consensus was that this would require a semantic change to the wayDefaultSignaturesworked, and I didn't feel like making a GHC proposal just for this one little thing.Unfortunately,
singletons-threally does need to useDefaultSignatureshere to makeSEqinstances with defaults typecheck—or, at the very least, something very close in spirit toDefaultSignatures. I can see the following ways to work around the issue, but I'm not particularly fond of any of them:- Carve out a special case for class methods and require them to have prenex
foralls. - Require
singletons-thusers to enableDeepSubsumptionto make the generated defaults typecheck. - Make a GHC proposal to change the behavior of
DefaultSignaturesto make it perform more eta expansion. - Instead of using
DefaultSignatures, manually generate top-leveldefaultImplfunctions and apply them in instances, using knowledge of how many visible arguments each method has to determine how many arguments should be eta expanded. This would imply thatsingletons-thusers would need to be aware of thesedefaultImplfunctions and export them from their modules, so we would have to come up with a suitable naming convention for them.
Ugh. What a headache.
- Carve out a special case for class methods and require them to have prenex
For now, I think I'm simply going to park this. My WIP implementation can be found in the T542-experiment branch.