Typechecker plugins: request for review and another workflow question

Iavor Diatchki iavor.diatchki at gmail.com
Fri Nov 14 18:53:31 UTC 2014 

Hi,

The source code is here: https://github.com/yav/type-nat-solver
There is an example of a module using a plugin in `examples/A.hs`.

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.

-Iavor




On Fri, Nov 14, 2014 at 9:45 AM, Francesco Mazzoli <f at mazzo.li> wrote:

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

More information about the ghc-devs mailing list