Serialising evidence generated by typechecker plugins

[Adam Gundry]

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
> <simonpj at microsoft.com <mailto:simonpj at 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 at haskell.org
>     <mailto:ghc-devs-bounces at haskell.org>] On Behalf Of Adam
>     | Gundry
>     | Sent: 11 December 2014 12:23
>     | To: Iavor Diatchki; Eric Seidel
>     | Cc: ghc-devs at haskell.org <mailto:ghc-devs at 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/