<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"Calibri Light";
panose-1:2 15 3 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
h2
{mso-style-priority:9;
mso-style-link:"Heading 2 Char";
margin-top:2.0pt;
margin-right:0cm;
margin-bottom:0cm;
margin-left:0cm;
margin-bottom:.0001pt;
page-break-after:avoid;
font-size:13.0pt;
font-family:"Calibri Light",sans-serif;
color:#2F5496;
font-weight:normal;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:#954F72;
text-decoration:underline;}
p.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph
{mso-style-priority:34;
margin-top:0cm;
margin-right:0cm;
margin-bottom:0cm;
margin-left:36.0pt;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
p.Code, li.Code, div.Code
{mso-style-name:Code;
margin-top:0cm;
margin-right:0cm;
margin-bottom:0cm;
margin-left:14.2pt;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Courier New";
font-weight:bold;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.EmailStyle19
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
span.Heading2Char
{mso-style-name:"Heading 2 Char";
mso-style-priority:9;
mso-style-link:"Heading 2";
font-family:"Calibri Light",sans-serif;
color:#2F5496;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:198668638;
mso-list-type:hybrid;
mso-list-template-ids:-628690142 134807553 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l1
{mso-list-id:316419234;
mso-list-template-ids:-141793050;}
@list l2
{mso-list-id:1506701894;
mso-list-type:hybrid;
mso-list-template-ids:1909738248 134807553 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l2:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l2:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l2:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l2:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l2:level5
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l2:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l2:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l2:level8
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l2:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l3
{mso-list-id:2007129445;
mso-list-template-ids:1684948790;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-GB" link="#0563C1" vlink="#954F72">
<div class="WordSection1">
<p class="MsoNormal">Alexis<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">What you suggest sounds like an excellent idea. For some plugins, being able to extend the range of “built in” families might be all the plugin needs to do! (For others it might need to do some solving too.)<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
I’ve thought a bit about how to achieve this:<o:p></o:p></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-top:6.0pt;margin-bottom:6.0pt;margin-left:0cm;mso-list:l2 level1 lfo3">
The most direct thing would be for the solver, when initialised (via tcPluginInit), to return a [(Name, BuiltinSynFamily)] pairs as well as the solver and plugin-stop action. See Note 1 below.<o:p></o:p></li><li class="MsoListParagraph" style="margin-top:6.0pt;margin-bottom:6.0pt;margin-left:0cm;mso-list:l2 level1 lfo3">
Then the typechecker can keep (in tcg_plugins) a little (NameEnv BuiltinSynFamily), gotten by accumulating all the lists from all the plugins.<o:p></o:p></li><li class="MsoListParagraph" style="margin-top:6.0pt;margin-bottom:6.0pt;margin-left:0cm;mso-list:l2 level1 lfo3">
Now, in three places we need to look up in that env:<o:p></o:p></li><ul style="margin-top:0cm" type="circle">
<li class="MsoListParagraph" style="margin-top:6.0pt;margin-bottom:6.0pt;margin-left:0cm;mso-list:l2 level2 lfo3">
TcInteract.improveLocalFunEqs – see the use of sfInteractInert<o:p></o:p></li><li class="MsoListParagraph" style="margin-top:6.0pt;margin-bottom:6.0pt;margin-left:0cm;mso-list:l2 level2 lfo3">
TcInteract.improve_top_fun_eqs – see the use of sfInteractTop<o:p></o:p></li><li class="MsoListParagraph" style="margin-top:6.0pt;margin-bottom:6.0pt;margin-left:0cm;mso-list:l2 level2 lfo3">
FamInstEnv.reduceTyFamApp_maybe – see the use of isBuildintSynFamTyCon_maybe<o:p></o:p></li></ul>
</ul>
<p class="MsoListParagraph" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:36.0pt">
The easiest thing might be to extend the type FamInstEnvs to be a triple, with the (NameEnv BuiltinSymFamily) as one of the components.<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
That would make it possible for a plugin to “register” any number of type families as having a BuiltinSynFamily, which allows all the type-family matching and reduction to be done by code written by the plugin author. (Maybe “built in” is a misnomer... perhaps
“magic” or something would be less misleading.)<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
I don’t think this would be hard, and for the things it worked for it’d be much much better, I think.<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
If anyone wants to have a go, I’m happy to advise. <o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
NB: if we do this for type families, we should probably do it for<o:p></o:p></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-top:6.0pt;margin-bottom:6.0pt;margin-left:0cm;mso-list:l0 level1 lfo4">
<b>Type classes</b> (so the a plugin could implement new class-instance behaviour that needs code; c.f. the current ClsInst.matchGlobalInst which dispatches off to functions that handle the current built-in cases: Typeable, Coercible, HasField, etc.<o:p></o:p></li><li class="MsoListParagraph" style="margin-top:6.0pt;margin-bottom:6.0pt;margin-left:0cm;mso-list:l0 level1 lfo4">
<b>CoreRules</b> (so that a plugin could could add new BuitinRules)<o:p></o:p></li></ul>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Simon<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<o:p> </o:p></p>
<h2>Note 1. <o:p></o:p></h2>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
TcPlugin is defined oddly:<o:p></o:p></p>
<p class="Code">data TcPlugin = forall s. TcPlugin<o:p></o:p></p>
<p class="Code"> { tcPluginInit :: TcPluginM s<o:p></o:p></p>
<p class="Code"> -- ^ Initialize plugin, when entering type-checker.<o:p></o:p></p>
<p class="Code"><o:p> </o:p></p>
<p class="Code"> , tcPluginSolve :: s -> TcPluginSolver<o:p></o:p></p>
<p class="Code"> -- ^ Solve some constraints.<o:p></o:p></p>
<p class="Code"> -- TODO: WRITE MORE DETAILS ON HOW THIS WORKS.<o:p></o:p></p>
<p class="Code"><o:p> </o:p></p>
<p class="Code"> , tcPluginStop :: s -> TcPluginM ()<o:p></o:p></p>
<p class="Code"> -- ^ Clean up after the plugin, when exiting the type-checker.<o:p></o:p></p>
<p class="Code"> }<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
What is that bizarre existential ‘s’? All we can do is to apply tcPluginSolve and tcPluginStop to it, which happens immediately, in TcRnDriver.withTcPlugins. So I think it’d make more sense and simpler thus<o:p></o:p></p>
<p class="Code">type TcPlugin = TcM (TcPluginSolver, TcM ())<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
So, run that TcM action to initialise it; the action returns a solver, and a stop action. Neither initialisation nor stop action need to access that EvBindsVar.<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
You could make that tuple into a record with named fields.<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<o:p> </o:p></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> ghc-devs <ghc-devs-bounces@haskell.org>
<b>On Behalf Of </b>Alexis King<br>
<b>Sent:</b> 20 August 2019 09:17<br>
<b>To:</b> ghc-devs@haskell.org<br>
<b>Subject:</b> Typechecker plugins and BuiltInSynFamily<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Hello all,<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">As I’ve been dabbling with typechecker plugins, I’ve found myself primarily using them to define new “magic” type families, and I don’t think I’m alone—Sandy Maguire recently released the magic-tyfams package for precisely that purpose.
However, I can’t help but notice that GHC already has good <i>internal</i> support for such type families via BuiltInSynFamily and CoAxiomRule, which are mostly used to implement operations on Nats. As a plugin author, I would love to be able to use that functionality
directly instead of being forced to reimplement it myself, for two big reasons:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<ol start="1" type="1">
<li class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:12.0pt;mso-list:l3 level1 lfo1">
AxiomRuleCo provides significantly more safety from -dcore-lint than UnivCo, but UnivCo is currently the only way to provide evidence for plugin-solved families.<o:p></o:p></li><li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l3 level1 lfo1">
The sfInteractTop and sfInteractInert fields of BuiltInSynFamily make it easy to support improvement for custom type families, which I believe would take a non-trivial amount of tricky code to get right using the current typechecker plugin API.<o:p></o:p></li></ol>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
<div>
<p class="MsoNormal">Given the above, I started wondering if it is possible to define a BuiltInSynFamily from inside a plugin or, failing that, to modify GHC to expose that functionality to typechecker plugin authors. I am not familiar with GHC’s internals,
but in my brief reading of the source code, the following two things seem like the trickiest obstacles:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<ol start="1" type="1">
<li class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:12.0pt;mso-list:l1 level1 lfo2">
BuiltInSynFamily TyCons need to be injected into the initial name cache, since otherwise those names will get resolved to their ordinary, non-built-in counterparts (e.g. the ordinary open type families defined in GHC.TypeLits).<o:p></o:p></li><li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l1 level1 lfo2">
Since CoAxiomRule values actually have functions inside them, they can’t be serialized into interface files. Therefore, it looks like GHC currently maintains a hardcoded list of all the known CoAxiomRules, and tcIfaceCoAxiomRule just searches for a value in
that list using a well-known (i.e. not in any way namespaced!) string.<o:p></o:p></li></ol>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
<div>
<p class="MsoNormal">I am not knowledgable enough about GHC to say how hard overcoming either of those issues would be. Point 1 seems possible to achieve by arranging for plugins to export the built-in names they want to define and propagating those to the
initial name cache, but I don’t know enough about how plugins are loaded to know if that would create any possible circular dependencies (i.e. does the name cache need to already exist in order to load a plugin in the first place?).<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Point 2 seems harder. My gut instinct is that it could probably be overcome by somehow storing a reference to the plugin that defined the CoAxiomRule in the interface file (by, for example, storing its package-qualified module name), but
I’m not immediately certain when that reference should be resolved to the actual CoAxiomRule value. It also presumably needs to complain if the necessary plugin is not actually loaded when the CoAxiomRule needs to be resolved!<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I’m willing to try my hand at experimenting with an implementation of this if someone can give me a couple pointers on where to start on the above two issues (assuming people don’t think it’s a bad idea to do it at all). Any advice would
be appreciated!<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">Alexis<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
</div>
</body>
</html>