Rewriting plugins: request for feedback
Hi everyone, Recent refactors to the constraint solver have complicated the story for authors of type-checking plugins. Following a suggestion by Christiaan Baaij, and aided by Richard Eisenberg, I'm working on adding the ability for type-checking plugins to rewrite type family applications directly (hooking straight into GHC's type-family rewriting code). The goal is to ease migration for the plugin authors, hopefully simplifying the common operation of rewriting type family applications. Let me now describe the current API for this new functionality, for which I would like feedback. -------------------------------------------------------------------------- A new field is added to the TcPlugin data type, namely tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter Here s is the existential plugin state that users can choose as they wish for their own plugin. Plugins thus register which type family TyCons they are interested in rewriting, like so: myTcPluginRewrite :: MyPluginState -> UniqFM TyCon TcPluginRewriter myTcPluginRewrite s@(MyPluginState {myFam1TyCon, myFam2TyCon}) = listToUFM [ (myFam1TyCon, myFam1Rewriter s), (myFam2TyCon, myFam2Rewriter s) ] For each type family TyCon, the plugin should provide a rewriting function (corresponding to myFam1Rewriter and myFam2Rewriter above), of type type TcPluginRewriter = [Ct] -> [TcType] -> TcPluginM TcPluginRewriteResult This means that a rewriting function is supplied with the current Given constraints and the arguments of the (guaranteed to be saturated) type-family application, and should return a result of type: data TcPluginRewriteResult where TcPluginRewriteError :: (Diagnostic a, Typeable a) => a -> TcPluginRewriteResult TcPluginNoRewrite :: TcPluginRewriteResult TcPluginRewriteTo :: { rewriteTo :: TcType , rewriteEvidence :: TcCoercion } -> TcPluginRewriteResult That is, the plugin can specify what the type-family application should be rewritten to, throw an error, or do nothing. -------------------------------------------------------------------------- I'm hoping that the components of existing type-checking plugins concerned with type-family applications can instead use this mechanism and achieve more robust results by doing so, with less effort. I would like to hear from plugin authors whether this API suits their needs. If you know of someone not on this list that might be interested, please invite them to join the conversation. The current state of this patch can be found in the GHC MR 5909: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5909 Thanks, Sam
Hi again everyone, I've been making some more adjustments to the API of type-checking plugins. Following a suggestion by Richard, the mechanism for reporting errors while rewriting type family applications now consists of emitting a wanted constraint with a custom type error message. There are several technical reasons for this, which I will not get into. This means there are now only two constructors of TcPluginRewriteResult: TcPluginNoRewrite and TcPluginRewriteTo. Both of these now take an extra argument: additional wanted constraints, which will be processed and emitted by GHC. Coming back to the type-checking plugin API as a whole (not just the rewriting of type family applications), I've come to the realisation that it is probably best to keep GHC's interface as simple as possible, to allow library authors to write their own APIs. After all, most of the API doesn't need to live within the GHC codebase, and instead (in my opinion) belongs in libraries that simply import the ghc package (which thankfully doesn't hide any exports one might want to use). This means we don't have to tie any experimentation with type-checking plugin APIs to the GHC release schedule. To that end, I have concluded that one single non-backwards-compatible change seems important: changing the TcPluginM monad from being isomorphic to "ReaderT EvBindsVar TcM" to simply being a newtype around TcM. Then, we instead pass an EvBindsVar as an extra argument to tcPluginSolve. This avoids all the silly business with functions whose documentation said "only call this within tcPluginSolve or it will cause a crash" (a situation which was only made worse by the addition of rewriting plugins). It's also less opinionated: library authors can use a ReaderT wrapper in their API if they desire, but are not forced to do so. Please note that I don't make this change lightly, as I know it is already time-consuming enough to maintain type-checking plugins, especially as much more significant changes abound (removal of flattening variables in GHC 9.2, removal of derived constraints (possibly in GHC 9.4)). I hope nevertheless that you might find this acceptable. Finally, facilitated by the above, I have started implementing a library providing a simple API for type-checking plugins; see here https://github.com/sheaf/ghc-tcplugin-api. An example of a not-totally-trivial rewriting plugin is given here: https://github.com/sheaf/ghc-tcplugin-api/blob/ad6ca964c3b27c28bb27392d7ba40... . Note that I barely had to import anything from the ghc package; I hope this can remain true for more involved plugins (up to a point). Please let me know what you think, in particular if you think certain important functions are missing from the API. For this library specifically, I have added back ReaderT layers (but only in the appropriate situations, to avoid reintroducing the aforementioned problem with "only call this in tcPluginSolve"), and provided MTL-style typeclasses for operations that work with multiple different phases of the plugin. Other design options are of course possible; at any rate, I think it is preferable to be making these API choices outside of GHC itself whenever possible. I've also included helpers for creating custom type errors within type-checking plugins, as that was unnecessarily cumbersome. (One still needs to provide a CtLoc to inform GHC of the source location of the error; one can get this from a constraint fed to the plugin in a solver plugin, or from the rewriting environment in a rewriter plugin). Note that this all still depends on the WIP GHC MR 5909, available at https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5909. I look forward to your feedback, Thanks, Sam
Hey everyone, I've put up some haddocks for this new type-checking plugin API, see here: https://sheaf.github.io/ghc-tcplugin-api/GHC-TcPlugin-API.html. (The page is mainly meant to be navigated using the contents pane.) I hope this might be a more welcoming point of entry for people who are interested in learning about GHC typechecker plugins. Let me know what you think, Thanks, Sam
Hi Sam,
Thanks for picking this up, the API looks good so far.
I'll try to port our https://hackage.haskell.org/package/ghc-typelits-extra
package to the new API.
Though first I need to upgrade
https://hackage.haskell.org/package/ghc-typelits-natnormalise to the GHC
9.2+ API,
which is got somewhat more complicated than usual GHC upgrades due to a
change in representation of (<=? :: Nat -> Nat -> Bool) in
https://gitlab.haskell.org/ghc/ghc/-/commit/eea96042f1e8682605ae68db10f2bcdd...
I'll report back any issues I encounter if/when I encounter any.
Cheers,
Christiaan
On Wed, 16 Jun 2021 at 23:04, Sam Derbyshire
Hey everyone,
I've put up some haddocks for this new type-checking plugin API, see here: https://sheaf.github.io/ghc-tcplugin-api/GHC-TcPlugin-API.html. (The page is mainly meant to be navigated using the contents pane.)
I hope this might be a more welcoming point of entry for people who are interested in learning about GHC typechecker plugins.
Let me know what you think,
Thanks,
Sam _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Hi everyone, Just a short message to let authors of type-checking plugins know that I've updated the ghc-tcplugin-api library with backwards compatibility for GHC 9.0 and 9.2. The functionality for rewriting type family applications will obviously not be present on those versions, but I hope this will allow plugin authors to try out the API for themselves and see what they think. It shouldn't be much different from what you are used to; mostly a change from "TcPluginM a" to MTL-style "MonadTcPlugin m => m a", or explicit solver monad "TcPluginM Solve a". The main improvements that this library offers in its current state are, in my opinion, as follows: - Decoupling from GHC, which has several upsides: - needs of plugin authors can be addressed rapidly without needing to wait for new GHC releases (of course, this doesn't apply to the changes which require commensurate changes to GHC), - cross-compatibility across GHC versions, hopefully lightening the CPP burden on plugin authors. - More extensive documentation that should help people get started with typechecking plugins. The haddocks remain available at the same page: https://sheaf.github.io/ghc-tcplugin-api/GHC-TcPlugin-API.html The library is available on the GitHub repository as before: https://github.com/sheaf/ghc-tcplugin-api I will upload the library to Hackage soon. Thanks all, Sam
Hello everyone, I'm happy to report that I have implemented a compatibility layer in the ghc-tcplugin-api library which provides type-family rewriting functionality on GHC 9.0 and 9.2. This means that plugin authors should now be able to use the exact same API from GHC 9.0 onwards (and in particular, without waiting for a version of GHC containing the new implementation of type-family rewriting plugins). To refresh your memory, writing a type-checking plugin with this library currently consists of the provision of a record data TcPlugin = forall s. TcPlugin { tcPluginInit :: TcPluginM Init s , tcPluginSolve :: s -> TcPluginSolver , tcPluginRewrite :: s -> UniqFM TyCon TcPluginRewriter , tcPluginStop :: s -> TcPluginM Stop () } with the following type synonyms: type TcPluginSolver = [GHC.Ct] -- ^ Givens -> [GHC.Ct] -- ^ Wanteds -> TcPluginM Solve TcPluginSolveResult Note that Deriveds are no longer passed explicitly. (It is possible to retrieve the Derived constraints from the TcPluginM Solve monad; as they are not commonly used, it made sense to make them less conspicuous.) type TcPluginRewriter = [GHC.Ct] -- ^ Givens -> [GHC.Type] -- ^ Type family arguments (saturated) -> TcPluginM Rewrite TcPluginRewriteResult On GHC 9.0 and 9.2, the tcPluginRewrite function will get hooked in as a pre-pass of the user-supplied tcPluginSolve function. There are small differences in behaviour that arise from solver plugins not always getting a chance to run when GHC can solve the wanteds on its own, but I expect this to have minimal impact. On top of this, I expect (but have not measured) a performance degradation compared to the "native" plugin type-family rewriting functionality, as the solver plugin must traverse all constraints to find type-family applications. I have not tested this compatibility layer extensively, so I welcome all feedback from plugin authors. Note that I have also reduced the amount of re-exported datatype constructors and accessors in an attempt to improve cross compatibility. Please let me know of any difficulties that you encounter as a consequence, and I will endeavour to re-export cross-compatible non-internal definitions. Thanks, Sam
Hi all, I have now written a much more substantial type-checking plugin, which I used to typecheck an intrinsically typed implementation of System F. I've added the example to the repository ( https://github.com/sheaf/ghc-tcplugin-api), see the readme. This uncovered several bugs in the implementation of the aforementioned compatibility layer for GHC 9.0 and 9.2, which have all been fixed. I can now in good conscience recommend that type-checking plugin authors try it out for themselves! There are slight inconsistencies in behaviour around emitting additional constraints when rewriting a type-family application (which I hope to iron out soon), but I expect the impact of this to be very minimal. Other than that, you can expect feature and behaviour parity with the native implementation. Please let me know how you get on, and which pain points you would like to see addressed. My current ideas for improvement are as follows: - Functionality that would perform all the name resolution necessary in the plugin initialisation. The user would provide a record of the types to look up (a TyCon named ... in module ..., a Class named ... in module ...), and the library would look up everything. This would be quite straightforward with a library such as barbies, but I don't necessarily want to impose that cognitive overhead on users who are not familiar with it. - An interface for handling type family rewritings that provides a type system that kind checks everything. For instance, instead of manually calling splitTyConAppMaybe, we could feasibly instead use a pattern with existential variables (matching on this pattern would introduce the kinds), and then use a smart constructor instead of mkTyConApp (which would kind-check the application). I certainly would have appreciated something like this when writing my System F plugin, as handling all the kinds explicitly was rather tiresome and error prone. - Functionality for recognising that a type has a certain form, making use of Givens. For example, it can be quite annoying to find out whether a given type is a type family application, as one needs to look through the Givens to go through levels of indirection. For instance, one might come across a variable "x" (ostensibly not a type family application), but have Givens [G] y ~ x, [G] F a ~ y. (This happens often with flattening skolems.) Please let me know if you have any other ideas, or suggestions on how to tackle the above. Thanks. Best, Sam
This sounds very cool!
FYI the Inria paper link in the readme seems to not be correct?
On Fri, Jul 9, 2021 at 6:56 PM Sam Derbyshire
Hi all,
I have now written a much more substantial type-checking plugin, which I used to typecheck an intrinsically typed implementation of System F. I've added the example to the repository ( https://github.com/sheaf/ghc-tcplugin-api), see the readme.
This uncovered several bugs in the implementation of the aforementioned compatibility layer for GHC 9.0 and 9.2, which have all been fixed. I can now in good conscience recommend that type-checking plugin authors try it out for themselves! There are slight inconsistencies in behaviour around emitting additional constraints when rewriting a type-family application (which I hope to iron out soon), but I expect the impact of this to be very minimal. Other than that, you can expect feature and behaviour parity with the native implementation.
Please let me know how you get on, and which pain points you would like to see addressed. My current ideas for improvement are as follows:
- Functionality that would perform all the name resolution necessary in the plugin initialisation. The user would provide a record of the types to look up (a TyCon named ... in module ..., a Class named ... in module ...), and the library would look up everything. This would be quite straightforward with a library such as barbies, but I don't necessarily want to impose that cognitive overhead on users who are not familiar with it. - An interface for handling type family rewritings that provides a type system that kind checks everything. For instance, instead of manually calling splitTyConAppMaybe, we could feasibly instead use a pattern with existential variables (matching on this pattern would introduce the kinds), and then use a smart constructor instead of mkTyConApp (which would kind-check the application). I certainly would have appreciated something like this when writing my System F plugin, as handling all the kinds explicitly was rather tiresome and error prone. - Functionality for recognising that a type has a certain form, making use of Givens. For example, it can be quite annoying to find out whether a given type is a type family application, as one needs to look through the Givens to go through levels of indirection. For instance, one might come across a variable "x" (ostensibly not a type family application), but have Givens [G] y ~ x, [G] F a ~ y. (This happens often with flattening skolems.)
Please let me know if you have any other ideas, or suggestions on how to tackle the above. Thanks.
Best,
Sam
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Hi everyone, I've uploaded the new type-checking plugin API to Hackage: https://hackage.haskell.org/package/ghc-tcplugin-api. Let me know how you get on. It should be much easier to iterate on the design and add new functionality, now that the API isn't tied to GHC. Thanks, Sam
participants (3)
-
Carter Schonwald -
Christiaan Baaij -
Sam Derbyshire