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 > <simo...@microsoft.com <mailto:simo...@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-boun...@haskell.org > <mailto:ghc-devs-boun...@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/ _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
