Hello, the reason there's a function there is that the type-nats are using an infinite family of axioms (e..g, the axiom `AddDef` which can be applied to any two concrete number, so `AddDef 1 2 : (1 + 2) ~ 3`). Do you think it'd be possible to allow plugins to "register" a list of axioms, so that when we load interfaces, we lookup axioms not only in the built-in type-nats list, but also in the axioms provided by various plugins? -Iavor On Thu, Dec 11, 2014 at 12:46 PM, Simon Peyton Jones wrote:

Go ahead and make suggestions here. Since a CoAxiomRule embodies essentially arbitrary computation, it's hardly surprising that there's a fixed range of possibilities.

I suppose that for extensibilty, any particular plugin could say "TypeNats:Rule1", "TypeNats:Rule" etc, and recognise that at the other end. We'd just need generic way to identify a plugin, plus an Int to say which axiom from that plugin.

Anyway, it's all to play for.

Simon

| -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Adam | Gundry | Sent: 11 December 2014 12:23 | To: Iavor Diatchki; Eric Seidel | Cc: ghc-devs@haskell.org | Subject: Serialising evidence generated by typechecker plugins | | Hi folks, | | I've just discovered tcIfaceCoAxiomRule, which is used when typechecking | a coercion from an interface file. It turns out that CoAxiomRules are | represented in interface files by their names, so tcIfaceCoAxiomRule | looks up this name in a map containing all the built-in | typeNatCoAxiomRules. | | Unfortunately, this lookup fails when a plugin has defined its own | CoAxiomRule (as both uom-plugin and type-nat-solver do)! This means that | if a module uses a plugin and exports some of the evidence generated via | an unfolding, importing the module may result in a tcIfaceCoAxiomRule | panic. | | At the moment, both plugins generate fake CoAxiomRules that can prove | the equality of any types, so one workaround would be to expose this | ability in the TcCoercion type (i.e. add the equivalent of UnivCo). In | the future, however, it would be nice if plugins could actually generate | bona fide evidence based on their own axioms (e.g. the abelian group | laws, for uom-plugin). | | We can't currently serialise CoAxiomRule directly, because it contains a | function in the coaxrProves field. Could we support an alternative | first-order representation that could be serialised? This probably | wouldn't be as expressive, in particular it might not cover the built-in | axioms that define type-level comparison functions and arithmetic | operators, but it would allow plugins to axiomatize algebraic theories. | | Any thoughts? | | Adam | | P.S. I've updated https://phabricator.haskell.org/D553 with the | TcPluginM changes we discussed. | | | -- | Adam Gundry, Haskell Consultant | Well-Typed LLP, http://www.well-typed.com/ | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://www.haskell.org/mailman/listinfo/ghc-devs

On Dec 12, 2014, at 3:30 AM, Adam Gundry wrote:

I did vaguely wonder about doing something like this, but was worried about the complexity. Since you all seem keen, though, I'll have a go and see if I can make it work. I'd imagine using the (plugin module name, axiom name) pair to identify the axiom, and adding a new field to plugins that implements coaxrProves.

I don't think (plugin module name, axiom name) is quite enough. It's possible that the plugin was updated in the meantime, and that could lead to obscure errors. I would prefer (plugin module name, plugin checksum, axiom name), for some appropriate definition of (plugin checksum). Although, as I write this, I realize GHC must have a mechanism for dealing with updated dependencies, because this exact same issue can arise absent plugins.

Re Richard's point:

...

Suppose plugin P is responsible for producing CoAxiomRule R while compiling module M. I think it's reasonable to require any module N that imports M to have access to plugin P. (And, perhaps, to specify the use of P in GHC options while compiling N.)

I agree with N requiring access to P, as a transitive dependency, but I'd rather not have to specify P up front when compiling N. One library's use of a plugin shouldn't force it on all its users!

It seems there are now two ways a module may use a plugin: 1) the module can require the plugin for its own code to typecheck, or 2) the module just depends on another module that uses the plugin. Are these specified differently? It sounds like you want (2) to impose no annotation burden on the user. I've argued in the past that, sometimes, (1) should also require only a small burden (perhaps -XTypecheckerPlugins). Say I am writing a module that depends on several libraries which use fancy types. I don't want to have to look up the names of all the plugins that help solve for the types that I'm using. Instead, I'm happy to tell GHC that it can do fancy, library-specified things and let it figure out what plugins to use. (I do think we should require a language extension here, or perhaps some other command-line flag that doesn't name the plugins used, so that plugins don't represent an unavoidable security hole.) Richard

Thanks,

Adam

On 11/12/14 22:44, Iavor Diatchki wrote:

...

Hello,

the reason there's a function there is that the type-nats are using an infinite family of axioms (e..g, the axiom `AddDef` which can be applied to any two concrete number, so `AddDef 1 2 : (1 + 2) ~ 3`).

Do you think it'd be possible to allow plugins to "register" a list of axioms, so that when we load interfaces, we lookup axioms not only in the built-in type-nats list, but also in the axioms provided by various plugins?

-Iavor

On Thu, Dec 11, 2014 at 12:46 PM, Simon Peyton Jones mailto:simonpj@microsoft.com> wrote:

Go ahead and make suggestions here. Since a CoAxiomRule embodies essentially arbitrary computation, it's hardly surprising that there's a fixed range of possibilities.

I suppose that for extensibilty, any particular plugin could say "TypeNats:Rule1", "TypeNats:Rule" etc, and recognise that at the other end. We'd just need generic way to identify a plugin, plus an Int to say which axiom from that plugin.

Anyway, it's all to play for.

Simon

| -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org mailto:ghc-devs-bounces@haskell.org] On Behalf Of Adam | Gundry | Sent: 11 December 2014 12:23 | To: Iavor Diatchki; Eric Seidel | Cc: ghc-devs@haskell.org mailto:ghc-devs@haskell.org | Subject: Serialising evidence generated by typechecker plugins | | Hi folks, | | I've just discovered tcIfaceCoAxiomRule, which is used when typechecking | a coercion from an interface file. It turns out that CoAxiomRules are | represented in interface files by their names, so tcIfaceCoAxiomRule | looks up this name in a map containing all the built-in | typeNatCoAxiomRules. | | Unfortunately, this lookup fails when a plugin has defined its own | CoAxiomRule (as both uom-plugin and type-nat-solver do)! This means that | if a module uses a plugin and exports some of the evidence generated via | an unfolding, importing the module may result in a tcIfaceCoAxiomRule | panic. | | At the moment, both plugins generate fake CoAxiomRules that can prove | the equality of any types, so one workaround would be to expose this | ability in the TcCoercion type (i.e. add the equivalent of UnivCo). In | the future, however, it would be nice if plugins could actually generate | bona fide evidence based on their own axioms (e.g. the abelian group | laws, for uom-plugin). | | We can't currently serialise CoAxiomRule directly, because it contains a | function in the coaxrProves field. Could we support an alternative | first-order representation that could be serialised? This probably | wouldn't be as expressive, in particular it might not cover the built-in | axioms that define type-level comparison functions and arithmetic | operators, but it would allow plugins to axiomatize algebraic theories. | | Any thoughts? | | Adam

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