Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

The great StandaloneKindSignatures patch of 2020 #432

Merged
merged 2 commits into from
Feb 10, 2020
Merged

Conversation

RyanGlScott
Copy link
Collaborator

This is a mega-patch that overhauls singletons to use StandaloneKindSignatures as a means to:

  1. Order kind variables more precisely (as a step towards Figure out how to promote visible type application sensibly #378).
  2. Greatly simplify the algorithm used for defunctionalization.

This is separated into two separate commits. Here is the first commit message:

Make TH generate standalone kind signatures

This patch addresses chunk (2) in
https://github.com/goldfirere/singletons/issues/378#issuecomment-528519679
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.

And here is the second commit message:

Make TH generate standalone kind signatures

This patch addresses chunk (2) in
https://github.com/goldfirere/singletons/issues/378#issuecomment-528519679
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`.

@RyanGlScott RyanGlScott requested review from goldfirere and removed request for goldfirere February 1, 2020 05:58
Copy link
Owner

@goldfirere goldfirere left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have not reviewed every line in detail, but I read the Notes carefully. I'm in favor. Thanks for doing this!

CHANGES.md Outdated Show resolved Hide resolved
src/Data/Singletons/Partition.hs Outdated Show resolved Hide resolved
src/Data/Singletons/Prelude/Monad/Internal.hs Show resolved Hide resolved
src/Data/Singletons/Promote.hs Show resolved Hide resolved
src/Data/Singletons/Promote.hs Show resolved Hide resolved
src/Data/Singletons/Promote.hs Outdated Show resolved Hide resolved
src/Data/Singletons/Promote/Defun.hs Outdated Show resolved Hide resolved
src/Data/Singletons/Promote/Defun.hs Outdated Show resolved Hide resolved
src/Data/Singletons/Promote/Defun.hs Show resolved Hide resolved
src/Data/Singletons/Promote/Defun.hs Show resolved Hide resolved
@RyanGlScott RyanGlScott force-pushed the saks-take-two branch 3 times, most recently from f24621b to e16731b Compare February 5, 2020 12:27
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.
This patch bestows various type-level declarations with standalone
kind signatures. Aside from making the kinds of everything easier to
read and more uniform, this has three benefits:

* The `ApplyTyCon` and `SndSigma` types are now forward-compatible
  with a future version of GHC that disables `-XCUSKs` by default.
* The code in `Data.Singletons.Prelude.*` and `tests/ByHand{,2}` more
  closely match the code that would be generated by the TH machinery.
* Now that `Σ` has a standalone kind signature, there is no longer
  any need to enable `ImpredicativeTypes` in `Data.Singletons.Sigma`,
  obsoleting the need for `Note [Impredicative Σ?]`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants