<div dir="ltr">Hi,<div><br></div><div>The source code is here: <a href="https://github.com/yav/type-nat-solver">https://github.com/yav/type-nat-solver</a></div><div>There is an example of a module using a plugin in `examples/A.hs`.</div><div><br></div><div>Things may be a bit broken at the moment though, as we've been changing things a bit, to work with the new constraint solver, and plugin system.</div><div><br></div><div>-Iavor</div><div><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Nov 14, 2014 at 9:45 AM, Francesco Mazzoli <span dir="ltr"><<a href="mailto:f@mazzo.li" target="_blank">f@mazzo.li</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">For what it's worth, I'd be very excited to have that feature in 7.10.<br>
<br>
Iavor, is there anywhere I can read on how to try your solver for<br>
type-level naturals?<br>
<span class="HOEnZb"><font color="#888888"><br>
Francesco<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
On 14 November 2014 18:14, Adam Gundry <<a href="mailto:adam@well-typed.com">adam@well-typed.com</a>> wrote:<br>
> Thanks, Simon! I've been convinced that TcS is more than we need, and I<br>
> think the right thing to do is to (optionally) invoke the plugin after<br>
> the constraints have been unflattened anyway. I've just pushed a commit<br>
> to wip/tc-plugins-amg that does this. Iavor, Eric, your views on how<br>
> convenient this alternative is would be most welcome. I'm also wondering<br>
> if the plugin should be told how many times it has been called, to make<br>
> it easier to prevent infinite loops.<br>
><br>
> I'm very keen to get this into 7.10, appropriately branded as a very<br>
> experimental feature. Austin, have I sufficiently addressed your<br>
> concerns about the hs-boot file and multiple flags? Is there anything<br>
> else we need, apart perhaps from tests and documentation, which I'll put<br>
> together next week?<br>
><br>
> Thanks,<br>
><br>
> Adam<br>
><br>
><br>
> On 12/11/14 11:16, Simon Peyton Jones wrote:<br>
>> Iavor, Adam, Eric<br>
>><br>
>><br>
>><br>
>> I’m happy with the general direction of the plugins stuff, so I’m mostly<br>
>> going to leave it to you guys to plough ahead; but I am happy to respond<br>
>> to questions.<br>
>><br>
>><br>
>><br>
>>  * I still think it would be better to provide an escape hatch to the<br>
>> TcS, not merely the TcM, alongside the nice TcPluginM wrapper. Notably,<br>
>> Simon's new TcFlatten.unflatten needs TcS...<br>
>><br>
>><br>
>><br>
>> It think the only reason for this is that ‘unflatten’ needs to set<br>
>> evidence bindings, which in turn requires access to tcs_ev_binds.  I<br>
>> think that everything else is in TcM.  So I suppose you could carry<br>
>> around the EvBindsVar if you really didn’t want TcS.  (And I can see why<br>
>> you wouldn’t; TcS has a lot of stuff you don’t need.)<br>
>><br>
>><br>
>><br>
>> Simon<br>
>><br>
>><br>
>><br>
>><br>
>><br>
>> *From:*Iavor Diatchki [mailto:<a href="mailto:iavor.diatchki@gmail.com">iavor.diatchki@gmail.com</a>]<br>
>> *Sent:* 10 November 2014 19:15<br>
>> *To:* Adam Gundry<br>
>> *Cc:* <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a>; Simon Peyton Jones<br>
>> *Subject:* Re: Typechecker plugins: request for review and another<br>
>> workflow question<br>
>><br>
>><br>
>><br>
>> Hi,<br>
>><br>
>><br>
>><br>
>> On Mon, Nov 10, 2014 at 1:31 AM, Adam Gundry <<a href="mailto:adam@well-typed.com">adam@well-typed.com</a><br>
>> <mailto:<a href="mailto:adam@well-typed.com">adam@well-typed.com</a>>> wrote:<br>
>><br>
>><br>
>>     On the subject of that "nearly", I'm interested to learn whether you<br>
>>     have a suggestion to deal with unflattening, because the interface still<br>
>>     works with flat constraints only. Simon's changes should make it more<br>
>>     practical to unflatten inside the plugin, but it would be far easier (at<br>
>>     least for my purposes) if it was simply given unflattened constraints. I<br>
>>     realise that this would require the plugin loop to be pushed further<br>
>>     out, however, which has other difficulties.<br>
>><br>
>><br>
>><br>
>> Not sure what to do about this.  With the current setup, I think either<br>
>> way, the plugin would have to do some extract work.   Perhaps we should<br>
>> run the plugins on the unflattened constraints, and leave to the plugins<br>
>> to manually temporarily "flatten" terms from external theories?  For<br>
>> example, if the type-nat plugin saw `2 * F a ~ 4`, it could temporarily<br>
>> work with `2 * x ~ 4`, and then when it figures out that `x ~ 2`, it<br>
>> could emit `F a ~ 2` (non-canonical), which would go around again, and<br>
>> hopefully get fully simplified.<br>
>><br>
>><br>
>><br>
>><br>
>><br>
>><br>
>>     A few other issues, of lesser importance:<br>
>><br>
>>      * I still think it would be better to provide an escape hatch to the<br>
>>     TcS, not merely the TcM, alongside the nice TcPluginM wrapper. Notably,<br>
>>     Simon's new TcFlatten.unflatten needs TcS...<br>
>><br>
>> I don't mind that but, if I recall correctly, to do this without more<br>
>> recursive modules, we had to split `TCSMonad` in two parts, one with the<br>
>> types, and one with other stuff.  Eric and I did this once, but we<br>
>> didn't commit it, because it seemed like an orthogonal change.<br>
>><br>
>><br>
>><br>
>><br>
>><br>
>>      * Is there a way for my plugin to "solve" a given constraint (e.g. to<br>
>>     discard the uninformative "a * 1 ~ a")?<br>
>><br>
>> Yes, you'd say something like: `TcPluginOK [(evidence, "a * 1 ~ a")] []`<br>
>><br>
>><br>
>><br>
>> The first field of `TcPluginOK` are things that are solved, the second<br>
>> one is new work.<br>
>><br>
>><br>
>><br>
>>      * It is unfortunately easy to create infinite loops by writing plugins<br>
>>     that emit wanteds but make no useful progress. Perhaps there should be a<br>
>>     limit on the number of times round the loop (like SubGoalDepth but for<br>
>>     all constraints)?<br>
>><br>
>><br>
>><br>
>> Indeed, if a plugin keeps generating new work, we could go in a loop, so<br>
>> maybe a limit of some sort is useful.  However, note that if the plugin<br>
>> generates things that are already in the inert set, GHC should notice<br>
>> this and filter them, so we won't keep going.<br>
>><br>
>><br>
>><br>
>><br>
>><br>
>>      * Perhaps runTcPlugin should skip invoking the plugin if there are no<br>
>>     wanteds?<br>
>><br>
>><br>
>><br>
>> Oh, there is an important detail here that needs documentation!   GHC<br>
>> will call the plugin twice: once to improve the givens, and once to<br>
>> solve the wanteds.   The way to distinguish the two is exactly by the<br>
>> presence of the wanteds.<br>
>><br>
>><br>
>><br>
>> Why might you want to improve the givens?  Suppose you had something<br>
>> like `x * 2 ~ 4` as a given:  then you'd really want the plugin to<br>
>> generate another given: `x ~ 2`, as this is likely to help the rest of<br>
>> the constraint solving process.<br>
>><br>
>><br>
>><br>
>><br>
>>      * The use of ctev_evar in runTcPlugin is partial, and fails with a<br>
>>     nasty error if the plugin returns a non-wanted in the solved constraints<br>
>>     list. Would it be worth catching this error and issuing a sensible<br>
>>     message that chastises the plugin author appropriately?<br>
>><br>
>><br>
>><br>
>> Aha, good idea. Bad plugin! :-)<br>
>><br>
>><br>
>><br>
>><br>
>><br>
>>      * Finally, I presume the comment on runTcPlugin that "The plugin is<br>
>>     provided only with CTyEq and CFunEq constraints" is simply outdated and<br>
>>     should be removed?<br>
>><br>
>> Yep, thanks!<br>
>><br>
>><br>
>><br>
>>     Apologies for the deluge of questions - please take them as evidence of<br>
>>     my eagerness to use this feature!<br>
>><br>
>><br>
>><br>
>> Thanks for your feedback!  Also, if you feel like doing some hacking<br>
>> please do so---I am quite busy at the moment so I don't  have a ton of<br>
>> time to work on it, so any help you be most appreciated.  I know Eric is<br>
>> also quite keen on helping out so we can just coordinate over e-mail.<br>
>><br>
>><br>
>><br>
>> -Iavor<br>
><br>
><br>
> --<br>
> Adam Gundry, Haskell Consultant<br>
> Well-Typed LLP, <a href="http://www.well-typed.com/" target="_blank">http://www.well-typed.com/</a><br>
</div></div><div class="HOEnZb"><div class="h5">> _______________________________________________<br>
> ghc-devs mailing list<br>
> <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/ghc-devs" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-devs</a><br>
</div></div></blockquote></div><br></div>