yay :) On Mon, Oct 6, 2014 at 2:42 PM, Iavor Diatchki wrote:

Hi Adam,

I am back from vacation, and I think I should have some time to try to implement something along these lines.

Cheers, -Iavor

On Fri, Sep 12, 2014 at 9:41 AM, Adam Gundry wrote:

...

Hi folks,

Those of you at HIW last week might have been subjected to my lightning talk on plugins for the GHC type checker, which should allow us to properly implement nifty features like units of measure or type-level numbers without recompiling GHC. I've written up a wiki page summarising the idea:

https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker

Feedback is very welcome, particularly if (a) you have an interesting use for this feature or (b) you think this is a terrible idea!

Thanks,

Adam

-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Iavor, Wow, this is one of the coolest new features I've seen in a while, I have to say. I hope we can see it in GHC sometime soon. :) On Mon, Oct 13, 2014 at 3:34 PM, Iavor Diatchki wrote:

Hello,

We now have an implementation of type-checker with plugin support. If you are interested in trying it out:

- Checkout and build the `wip/tc-plugins` branch of GHC

- As an example, I've extracted my work on using an SMT solver at the type level as a separate plugin:

https://github.com/yav/type-nat-solver

- To see how to invoke a module that uses a plugin, have a look in `examples/A.hs`. (Currently, the plugin assumes that you have `cvc4` installed and available in the path).

- Besides this, we don't have much documentation yet. For hackers: we tried to use `tcPlugin` on `TcPlugin` in the names of all things plugin related, so you could grep for this. The basic API types and functions are defined in `TcRnTypes` and `TcRnMonad`.

Happy hacking, -Iavor

On Mon, Oct 6, 2014 at 11:53 AM, Carter Schonwald wrote:

...

yay :)

On Mon, Oct 6, 2014 at 2:42 PM, Iavor Diatchki wrote:

...

Hi Adam,

I am back from vacation, and I think I should have some time to try to implement something along these lines.

Cheers, -Iavor

On Fri, Sep 12, 2014 at 9:41 AM, Adam Gundry wrote:

...

Hi folks,

Those of you at HIW last week might have been subjected to my lightning talk on plugins for the GHC type checker, which should allow us to properly implement nifty features like units of measure or type-level numbers without recompiling GHC. I've written up a wiki page summarising the idea:

https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker

Feedback is very welcome, particularly if (a) you have an interesting use for this feature or (b) you think this is a terrible idea!

Thanks,

Adam

-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-- Regards, Austin Seipp, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/

This will become easier, I think. look on wip/new-flatten-skoelms-Aug14. I'm now unflattening after solving the flat constraints. Simon | -----Original Message----- | From: Glasgow-haskell-users [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Adam Gundry | Sent: 16 October 2014 11:59 | To: Iavor Diatchki | Cc: glasgow-haskell-users@haskell.org | Subject: Re: Type checker plugins | | Hi Iavor, | | | On 13/10/14 21:34, Iavor Diatchki wrote: | > Hello, | > | > We now have an implementation of type-checker with plugin support. | If | > you are interested in trying it out: | > | > - Checkout and build the `wip/tc-plugins` branch of GHC | | | Thanks, this is great! I'd been working on a similar implementation, | but yours is much better integrated. I am trying to adapt my units of | measure plugin to work with this interface, and work out what else I | need in TcPluginM. | | One problem I've run into is transforming the flattened CFunEqCans | into unflattened form (so the flatten-skolems don't get in the way of | AG-unification). Do you know if there is an easy way to do this, or do | I need to rebuild the tree manually in the plugin? | | Also, I notice that you are providing only equality constraints to the | plugin. Is there any reason we can't make other types of constraint | available as well? For example, one might want to introduce a | typeclass with a special solution strategy (cf. Coercible, or the Has | class in OverloadedRecordFields). | | | Cheers, | | Adam | | | > - As an example, I've extracted my work on using an SMT solver at | > the type level as a separate plugin: | > | > https://github.com/yav/type-nat-solver | > | > - To see how to invoke a module that uses a plugin, have a look | in | > `examples/A.hs`. | > (Currently, the plugin assumes that you have `cvc4` installed | and | > available in the path). | > | > - Besides this, we don't have much documentation yet. For | hackers: | > we tried to use `tcPlugin` on | > `TcPlugin` in the names of all things plugin related, so you | could | > grep for this. The basic API | > types and functions are defined in `TcRnTypes` and `TcRnMonad`. | > | > Happy hacking, | > -Iavor | | | -- | Adam Gundry, Haskell Consultant | Well-Typed LLP, http://www.well-typed.com/ | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Hello, Just a heads up, if anyone is playing around with this: I just updated the plugin interface a bit. Here are the changes: - A plugin now gets 3 sets of constraints: given, derived, and wanted (in that order) - Plugins are now also presented with dictionary constraints (i.e., you may see equalities, function equalities, and dictionaries) - A plugin does not need to return all constraints that need to be put back in the inert set. This is both simpler and more efficient, I think. So, now a plugin can return one of these two results: - All is good: plugin returns some solved constraints, and some new constraints to be processed by the constraint solver. The solved constraints are removed from the inert set, and their evidence variables are defined. The new work is added to the work list. - Found contradiction: plugin returns a list of the conflicting constraint; these are removed from the inert set, and re-added as insoluable. Happy hacking, -Iavor On Fri, Oct 17, 2014 at 3:36 PM, Iavor Diatchki wrote:

Hello,

On Thu, Oct 16, 2014 at 3:58 AM, Adam Gundry wrote:

...

One problem I've run into is transforming the flattened CFunEqCans into unflattened form (so the flatten-skolems don't get in the way of AG-unification). Do you know if there is an easy way to do this, or do I need to rebuild the tree manually in the plugin?

One thing that occurred to me about this: when constraints are "flattened", it is easy for a plugin to pick-out only the one that it cares about. If things were fully unflattened, this would not be the case... For example, if I have a constraint:

(2 + F a) ~ F a + F a

In the flattened form, this will become: (F a ~ f1, 2 + f1 ~ f2, f1 + f2 ~ f3, f2 ~ f3)

So, the type-nats plugin would pick out: (2 + f1 ~ f2, f1 + f2 ~ f3, f2 ~ f3), and ignore (F a ~ f1), as it knows nothing about arbitrary type functions.

So, if we want to do un-flattening, I think we should do it only on those constraints that are of interest to the plugin.

...

Also, I notice that you are providing only equality constraints to the plugin. Is there any reason we can't make other types of constraint available as well? For example, one might want to introduce a typeclass with a special solution strategy (cf. Coercible, or the Has class in OverloadedRecordFields).

Yeah, we should probably pass-in all constraints, inlcluding derived ones. The reason it is not like that is pretty much historical now. So I'll have a go at making this change.

-Iavor

...

...

- As an example, I've extracted my work on using an SMT solver at the type level as a separate plugin:

https://github.com/yav/type-nat-solver

- To see how to invoke a module that uses a plugin, have a look in `examples/A.hs`. (Currently, the plugin assumes that you have `cvc4` installed and available in the path).

- Besides this, we don't have much documentation yet. For hackers: we tried to use `tcPlugin` on `TcPlugin` in the names of all things plugin related, so you could grep for this. The basic API types and functions are defined in `TcRnTypes` and `TcRnMonad`.

Happy hacking, -Iavor

-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/

Hi, It shouldn't be hard to do the merge, but I am not sure that I'll have time to do it before the weekend---I'll give it a go then. -Iavor On Tue, Oct 21, 2014 at 9:40 AM, Adam Gundry wrote:

Thanks Iavor, this is really helpful!

If you have a moment to merge Simon's more recent changes on wip/new-flatten-skolems-Aug14, I'm keen to try out the new unflattening... or I can have a go at the merge if it would help?

You may be right that flattened constraints are easier to work with in some cases, so it would be great if the plugin could choose which it sees. Unfortunately I'm not sure we can easily unflatten *some* constraints, given the way unflattening will work in the new getInertUnsolved. One option might be for tcPluginSolve to be called in both places, with a boolean parameter.

Cheers,

Adam

On 18/10/14 23:33, Iavor Diatchki wrote:

...

Hello,

Just a heads up, if anyone is playing around with this: I just updated the plugin interface a bit.

Here are the changes: - A plugin now gets 3 sets of constraints: given, derived, and wanted (in that order) - Plugins are now also presented with dictionary constraints (i.e., you may see equalities, function equalities, and dictionaries) - A plugin does not need to return all constraints that need to be put back in the inert set. This is both simpler and more efficient, I think. So, now a plugin can return one of these two results: - All is good: plugin returns some solved constraints, and some new constraints to be processed by the constraint solver. The solved constraints are removed from the inert set, and their evidence variables are defined. The new work is added to the work list. - Found contradiction: plugin returns a list of the conflicting constraint; these are removed from the inert set, and re-added as insoluable.

Happy hacking, -Iavor

On Fri, Oct 17, 2014 at 3:36 PM, Iavor Diatchki mailto:iavor.diatchki@gmail.com> wrote:

Hello,

On Thu, Oct 16, 2014 at 3:58 AM, Adam Gundry mailto:adam@well-typed.com> wrote:

One problem I've run into is transforming the flattened CFunEqCans into unflattened form (so the flatten-skolems don't get in the way of AG-unification). Do you know if there is an easy way to do this, or do I need to rebuild the tree manually in the plugin?

One thing that occurred to me about this: when constraints are "flattened", it is easy for a plugin to pick-out only the one that it cares about. If things were fully unflattened, this would not be the case... For example, if I have a constraint:

(2 + F a) ~ F a + F a

In the flattened form, this will become: (F a ~ f1, 2 + f1 ~ f2, f1 + f2 ~ f3, f2 ~ f3)

So, the type-nats plugin would pick out: (2 + f1 ~ f2, f1 + f2 ~ f3, f2 ~ f3), and ignore (F a ~ f1), as it knows nothing about arbitrary type functions.

So, if we want to do un-flattening, I think we should do it only on those constraints that are of interest to the plugin.

Also, I notice that you are providing only equality constraints to the plugin. Is there any reason we can't make other types of constraint available as well? For example, one might want to introduce a typeclass with a special solution strategy (cf. Coercible, or the Has class in OverloadedRecordFields).

Yeah, we should probably pass-in all constraints, inlcluding derived ones. The reason it is not like that is pretty much historical now. So I'll have a go at making this change.

-Iavor

> - As an example, I've extracted my work on using an SMT solver at the > type level as a separate plugin: > > https://github.com/yav/type-nat-solver > > - To see how to invoke a module that uses a plugin, have a look in > `examples/A.hs`. > (Currently, the plugin assumes that you have `cvc4` installed and > available in the path). > > - Besides this, we don't have much documentation yet. For hackers: > we tried to use `tcPlugin` on > `TcPlugin` in the names of all things plugin related, so you could > grep for this. The basic API > types and functions are defined in `TcRnTypes` and `TcRnMonad`. > > Happy hacking, > -Iavor

-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/