Re: Serialising evidence generated by typechecker plugins

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. 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! 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/