Serialising evidence generated by typechecker plugins

[Richard Eisenberg]

On Dec 12, 2014, at 3:30 AM, Adam Gundry <adam at well-typed.com> 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
>> <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/