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> 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] 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 >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs