Figure out how to promote visible type application sensibly #378

RyanGlScott · 2019-01-14T18:46:33Z

There's currently this line in Data.Singletons.Promote:

singletons/src/Data/Singletons/Promote.hs

Lines 762 to 765 in fb5e005

    
           -- Until we get visible kind applications, this is the best we can do. 
        
           promoteExp (DAppTypeE exp _) = do 
        
             qReportWarning "Visible type applications are ignored by `singletons`." 
        
             promoteExp exp

Darn, if only we had visible kind applications! But hey, we're getting just that in GHC 8.8! Surely this means that we can rip out this antiquated code and treat visible type applications as a first-class citizen in singletons...

...but not so fast. It turns out that having visible kind applications isn't enough—we also need to figure out how to use it properly. Here's a function to help illustrate some of the challenges that VTA presents:

constBA :: forall b a. a -> b -> a
constBA x _ = x

constBA is exactly the same as the familiar const function, except I've deliberately swapped the conventional order that the type variables are quantified in. One interesting observation, right off the bat, is that when constBA is promoted to a type family:

type family ConstBA (x :: a) (y :: b) :: a where ...

The kind of ConstBA is now forall a b. a -> b -> a, not forall b a. a -> b -> a! What's worse, there is no reliable way of swapping the order that a and b are quantified in until we get top-level kind signatures. Blast.

But that's far from the only sticky thing about this situation. Let's suppose you want to use constBA, like in the following function:

blah :: forall b a. [a] -> [b -> a]
blah x = map (constBA @b) x

How should this promote? This is what currently happens in today's singletons, which simply drops VTAs:

type family Blah (x :: [a]) :: [b ~> a] where
  Blah x = Apply (Apply MapSym0 ConstBASym0) x

Notice that singletons always uses defunctionalization symbols when promoting function application, so if we want to promote constBA @b, this suggests that the output should be something like ConstBASym0 @b. But that presents its own set of challenges, because this is the code that gets generated for ConstBASym0:

data ConstBASym0 :: forall a b. a ~> b ~> a

This happens because during defunctionalization, we take the type a ~> b ~> a and quantify over it by simply gathering the free variables in left-to-right order. Unfortunately, this means that we get forall a b. <...> instead of forall b a. <...>. Double blast.

One could envision tweaking defunctionalization to remember the original order of type variables so that we generate data ConstBASym0 :: forall b a. a ~> b ~> a instead. That would fix blah, but we're not out of the clear yet. There's one more defunctionalization symbol to consider: ConstBASym1, which arises from this generated code:

data ConstSym1 (x :: a) :: forall b. b ~> a

This is even gnarlier than ConstSym0. The kind of ConstSym1 is forall a. a -> forall b. b ~> a, and this time, it's not simple to rearrange the foralls so that b is quantified before a due to the syntax used. One way forward is to declare ConstSym1 like so:

data ConstSym1 :: forall b a. a -> (b ~> a)

This works, although this trick currently won't work for anything that involves visible dependent quantification. (We could carve out a special case when defunctionalizing things without visible dependent quantification, although that would be a bit messy.)

By sheer accident, constBA is singled correctly... at least, some of the time. That is to say, this is generated for sConstBA:

sConstBA :: forall b_1 a_2 (x :: a_2) (y :: b_1). Sing x -> Sing y -> Sing (Apply (Apply ConstBASym0 x) y :: a_2)

This works only because b_1's unique happens to come before a_2's unique, so b_1 comes before a_2 when they're both put into a Set. (If compiled with -dunique-increment=-1, however, then you'd get the opposite order!)

That's not to say that singling VTAs is already a solved problem. Consider what happens when you single blah today:

sBlah :: forall b a (x :: [a]). Sing x -> Sing (Apply BlahSym0 x :: [b ~> a])
sBlah (sX :: Sing x) = (applySing ((applySing ((singFun2 @MapSym0) sMap)) ((singFun2 @ConstBASym0) sConstBA))) sX

Once again, we single function application by leveraging defunctionalization symbols. Therefore, in order to single blah correctly, we'd need to change singFun2 @ConstBASym0 to singFun2 @(ConstBASym0 @b), and moreover, we'd need to ensure that ConstBASym0 :: forall b a. a ~> b ~> a.

The text was updated successfully, but these errors were encountered:

goldfirere · 2019-01-14T19:41:58Z

Even worse: we really should include the visible dependent stuff in the defunctionalization symbols, making something like forall b ~> forall a ~> a ~> b ~> a. Actually, maybe that point is moot, because (->) is to (~>) as forall is to foreach, and kind-level forall already means foreach.

But it looks like this is a no-go at least until with have top-level signatures. I wouldn't even try this before we have that.

RyanGlScott · 2019-09-05T18:41:34Z

One thing that may not be evident from the wall of text in #378 (comment) is that fixing this issue can be divided into three relatively self-contained chunks:

Change singling to produce type signatures with correct type variable orders.
Change promotion to produce standalone kind signatures with correct type variable orders.
Make promotion/singling preserve visible type applications.

Chunk (2) depends on having standalone kind signatures, and chunk (3) depends on chunk (2). Chunk (1), on the other hand, is quite feasible to implement today. PR #408 knocks out chunk (1).

@t1

This patch tweaks `singType` (and its sister function `singCtor`) to produce type signatures that preserve the order in which type variables appear. For instance, if one writes this: ```hs const2 :: forall b a. a -> b -> a ``` Then its singled counterpart will now quantify `b` and `a` in the same order: ```hs sConst2 :: forall b a (x :: a) (y :: b). Sing x -> Sing y -> Sing (Const2 x y) ``` This is important if one wants to combine `sConst2` with visible type applications, as this means that the meaning of `@T1 @T2` in `const @t1 @T2` will be preserved when one writes `sConst2 @t1 @T2`. This also paves the way for #378, which seeks to fully support promoting/singling type applications in the TH machinery. Most of the interesting parts of this patch are described in `Note [Preserve the order of type variables during singling]` in `D.S.Single.Type`, so start that is a good starting point when looking at this patch for the first time. Fixes chunk (1) in #378 (comment), but there are still other parts of #378 that remain to be fixed.

@t1

This patch tweaks `singType` (and its sister function `singCtor`) to produce type signatures that preserve the order in which type variables appear. For instance, if one writes this: ```hs const2 :: forall b a. a -> b -> a ``` Then its singled counterpart will now quantify `b` and `a` in the same order: ```hs sConst2 :: forall b a (x :: a) (y :: b). Sing x -> Sing y -> Sing (Const2 x y) ``` This is important if one wants to combine `sConst2` with visible type applications, as this means that the meaning of `@T1 @T2` in `const @t1 @T2` will be preserved when one writes `sConst2 @t1 @T2`. This also paves the way for #378, which seeks to fully support promoting/singling type applications in the TH machinery. Most of the interesting parts of this patch are described in `Note [Preserve the order of type variables during singling]` in `D.S.Single.Type`, so start that is a good starting point when looking at this patch for the first time. Fixes chunk (1) in #378 (comment), but there are still other parts of #378 that remain to be fixed.

@t1

This patch tweaks `singType` (and its sister function `singCtor`) to produce type signatures that preserve the order in which type variables appear. For instance, if one writes this: ```hs const2 :: forall b a. a -> b -> a ``` Then its singled counterpart will now quantify `b` and `a` in the same order: ```hs sConst2 :: forall b a (x :: a) (y :: b). Sing x -> Sing y -> Sing (Const2 x y) ``` This is important if one wants to combine `sConst2` with visible type applications, as this means that the meaning of `@T1 @T2` in `const @t1 @T2` will be preserved when one writes `sConst2 @t1 @T2`. This also paves the way for #378, which seeks to fully support promoting/singling type applications in the TH machinery. Most of the interesting parts of this patch are described in `Note [Preserve the order of type variables during singling]` in `D.S.Single.Type`, so start that is a good starting point when looking at this patch for the first time. Fixes chunk (1) in #378 (comment), but there are still other parts of #378 that remain to be fixed.

While looking at the defunctionalization code recently, I discovered several smelly aspects of the code. This patch does not fix all such code smells (I plan to tackle more of them while tackling #378), but this does pick some of the lower-hanging fruit. Here are the highlights: 1. The `reverse` function is used an awful lot in `D.S.Promote.Defun.defunctionalize`. It's used here, when the inner loop (`go`) is first invoked: https://github.com/goldfirere/singletons/blob/2ec18435b8c57afcfcec0b7da872621b1179d45f/src/Data/Singletons/Promote/Defun.hs#L299 And it's also used here, inside of `go` itself: https://github.com/goldfirere/singletons/blob/2ec18435b8c57afcfcec0b7da872621b1179d45f/src/Data/Singletons/Promote/Defun.hs#L237-L240 This makes my head spin. Moreover, there other some parts of `go` that use `m_args` instead of using `reverse m_args`, which causes some odd-looking code to be generated (e.g., generating both `data BlahSym2 x y :: z ~> Type` _and_ `type instance Apply (BlahSym2 y x) z = BlahSym3 y x z`). None of this is technially wrong, but I find it hard to follow. Luckily, we can get away without needing either use of `reverse`. Instead of processing a single list of `TyVarBndr`s in reverse order inside of `go`, we can track two lists of `TyVarBndr`s. To how this works, imagine we are to generate these defunctionalization symbols: ```hs data BlahSym0 :: x ~> y ~> z ~> Type data BlahSym1 x :: y ~> z ~> Type data BlahSym2 x y :: z ~> Type ``` We can accomplish this by "cycling" through the `TyVarBndr`s with two lists: one for the arguments and another for the result kind. Or, in code: ```hs [] [x, y, z] -- BlahSym0 [x] [y, z] -- BlahSym1 [x, y] [z] -- BlahSym2 ``` Notice that at each iteration of `go`, we take the first `TyVarBndr` from the second list and append it to the end of the first. This makes `go` run in quadratic time, but this is not a new precedent, since `go` was quadratic before due to invoking `reverse` in each iteration. Given the choice between these two quadratic-time designs, I prefer the new one. I've applied this refactor to the `go` functions in `D.S.Promote.Defun.defunctionalize` and `D.S.Single.Defun.singDefuns`, and left some comments explaining what is going on. 2. The inner loop of `D.S.Promote.Defun.defunctionalize` works by starting from `n - 1` (where `n` is the number of arguments) and iterating until `0` is reached. On the flip side, the inner loop of `D.S.Single.Defun.singDefuns` works by starting from `0` and iterating until `n - 1` is reached. For the sake of consistency, I have adopted the `singDefuns` convention (start from `0` and count up) for both pieces of code. 3. The inner loops of `D.S.Promote.Defun.defunctionalize` and `D.S.Single.Defun.singDefuns` are monadic, but they don't need to be. The only monadic things they do are generate unique names, but this can be done more easily outside of the inner loops themselves. This patch refactors the code to do just that, making the inner loop code pure. A consequence of (2) is that `D.S.Promote.Defun.defunctionalize` now generates defunctionalization symbols in the opposite order that it used to. This causes many, many test cases to have different expected output, making the patch appear larger than it actually is.

This patch addresses chunk (2) in #378 (comment) by making the TH machinery generate standalone kind signatures wherever possible, inching closer to the goal of preserving the order of `forall`'s type variables in all promoted and singled code. I say "inching" since this post does not quite get there (see the "Caveats" section at the bottom of this commit message), but it comes very close. In brief, the TH machinery now generates SAKS for the following: * Promoted top-level functions See `D.S.Promote.promoteLetDecRHS` for how this is implemented. * Defunctionalization symbols SAKS provide a wonderful opportunity to clean up the implementation in `D.S.Promote.Defun`, which is currently somewhat crufty. The code used to jump through hoops in order to give defunctionalization symbols CUSKs, but now that we live in a post-CUSKs world, we can get rid of all the ad hoc-ness in `Note [Defunctionalization and dependent quantification]`. Instead, we now use a much simpler algorithm that only depends on whether the thing being defunctionalized has a SAK or not. See `Note [Defunctionalization game plan]` in `D.S.Promote.Defun`. * Singled data type declarations If a data type's order of kind variables is known (e.g., if it was declared with a SAK), then the singled version of the data type will use a SAK to preserve the same kind variable order. See the code in `D.S.Single.Data.singDataD`. * Promoted and singled class declarations Similarly, if the order of kind variables is known for a class `C`, then the TH machinery will generate SAKS for `PC` and `SC` to preserve the same kind variable order. See the code in `D.S.Promote.promoteClassDec` and `D.S.Single.singClassD`. Naturally, lots of test cases' expected outputs change as a result of this patch. See `Singletons.T378{a,b}` for some new (or altered) cases that test new code paths. ------------- -- Caveats -- ------------- Alas, not everything preserves the order of type variables after this patch. Some notable exceptions are: * `let`- or `where`-bound functions When promoting this function: ```hs f :: Bool f = let x = True g :: () -> Bool g _ = x in g () ``` The TH machinery will give the promoted `F` type family a SAK, but not the `G` type family. See `Note [No SAKs for let-decs with local variables]` in `D.S.Promote` for an explanation. * Promoted class methods This class: ```hs class C (b :: Type) where m :: forall a. a -> b -> a ``` Is promoted like so: ```hs class PC (b :: Type) where type M (x :: a) (y :: b) :: a ``` The order of the variables `a` and `b` are different between the type of `m` and the kind of `M`. See `Note [Promoted class methods and kind variable ordering]` in `D.S.Promote`. * Fully saturated defunctionalization symbols If you defunctionalize the `Id` type family, you'll generate two defunctionalization symbols: ```hs type IdSym0 :: forall a. a ~> a data IdSym0 f where ... type IdSym1 (x :: a) = Id x :: a ``` Notice that unlike `IdSym0`, `IdSym1` (the "fully saturated" defunctionalization symbol) does _not_ have a SAK. This is because in general, giving fully saturated defunctionalization symbols SAKS can lead to kind errors. See `Note [No SAKs for fully saturated defunctionalization symbols]` in `D.S.Promote.Defun` for the sordid story.

RyanGlScott · 2020-02-10T12:19:43Z

PR #432 knocked out chunk (2). Unfortunately, I don't think we're ready to tackle chunk (3) yet for various reasons:

Even after The great StandaloneKindSignatures patch of 2020 #432, there are still ~~three~~ two situations where singletons won't preserve the order of kind variables during promotion:
- let- or where-bound functions won't be given SAKS. To give a particular example:
```
f :: Bool
f = let x = True
        g :: () -> Bool
        g _ = x
    in g ()
```
  The TH machinery will give the promoted F type family a SAK, but not the G type family. See Note [No SAKs for let-decs with local variables] in D.S.Promote for an explanation.
- Promoted class methods cannot be given SAKS. For example, this class:
```
class C (b :: Type) where
  m :: forall a. a -> b -> a
```
  Is promoted like so:
```
class PC (b :: Type) where
  type M (x :: a) (y :: b) :: a
```
  The order of the variables a and b are different between the type of m and the kind of M. See Note [Promoted class methods and kind variable ordering] in D.S.Promote.
- EDIT: This is no longer the case after Declare fully saturated defun symbols as type families #446.
  
  ~~Fully saturated defunctionalization symbols won't be given SAKS. For example, if you defunctionalize the Id type family, you'll generate two defunctionalization symbols:~~
```
type IdSym0 :: forall a. a ~> a
data IdSym0 f where ...

type IdSym1 (x :: a) = Id x :: a
```
  Notice that unlike IdSym0, IdSym1 (the "fully saturated" defunctionalization symbol) does not have a SAK. This is because in general, giving fully saturated defunctionalization symbols SAKS can lead to kind errors. See Note [No SAKs for fully saturated defunctionalization symbols] in D.S.Promote.Defun for the sordid story.
Even if we did generate exactly the right order of kind variables for all promoted declarations, there is an even larger issue: functions that make use of scoped type variables do not reliably promote. See Promoting expression signatures can fail on GHC 8.10+ #433. This is rather annoying since scoped type variables and TypeApplications are often used in tandem, such as in the following example (which is affected by Promoting expression signatures can fail on GHC 8.10+ #433):
```
$(singletons [d|
  f :: forall a. a -> a
  f x = id @a x
  |])
```

These issues essentially boil down to limitations in the way type families work in GHC, and as a result, they are difficult to work around on singletons end. As a result, I am inclined to park this issue pending further developments on GHC's side. That is not to say that the work spent fixing chunks (1) and (2) was wasted. We can now use TypeApplications in manually written singletons code much more reliably than before, which is a huge win. I'm personally benefitting from this work, at the very least, and I imagine others will too.

RyanGlScott added the enhancement label Jan 14, 2019

RyanGlScott added the Blocked upstream label Jan 15, 2019

RyanGlScott mentioned this issue Sep 3, 2019

Properly reject higher-rank types during promotion/singling #406

Merged

RyanGlScott mentioned this issue Sep 5, 2019

Make singling preserve type variable order in type signatures #408

Merged

RyanGlScott mentioned this issue Sep 26, 2019

GHC 8.10 checklist #385

Closed

4 tasks

RyanGlScott mentioned this issue Nov 24, 2019

Clean up some code smells in D.S.{Promote,Single}.Defun #424

Merged

RyanGlScott mentioned this issue Jan 26, 2020

The great StandaloneKindSignatures patch of 2020 #432

Merged

RyanGlScott mentioned this issue Feb 6, 2020

Promoting expression signatures can fail on GHC 8.10+ #433

Closed

RyanGlScott mentioned this issue Mar 24, 2021

Allow promoting and singling of visible type applications in data constructor patterns #489

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Figure out how to promote visible type application sensibly #378

Figure out how to promote visible type application sensibly #378

RyanGlScott commented Jan 14, 2019

goldfirere commented Jan 14, 2019

RyanGlScott commented Sep 5, 2019 •

edited

RyanGlScott commented Feb 10, 2020 •

edited

Figure out how to promote visible type application sensibly #378

Figure out how to promote visible type application sensibly #378

Comments

RyanGlScott commented Jan 14, 2019

goldfirere commented Jan 14, 2019

RyanGlScott commented Sep 5, 2019 • edited

RyanGlScott commented Feb 10, 2020 • edited

RyanGlScott commented Sep 5, 2019 •

edited

RyanGlScott commented Feb 10, 2020 •

edited