Serialising evidence generated by typechecker plugins

[Iavor Diatchki]

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>
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] On Behalf Of Adam
> | Gundry
> | Sent: 11 December 2014 12:23
> | To: Iavor Diatchki; Eric Seidel
> | Cc: 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
> |
> | 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 at haskell.org
> | http://www.haskell.org/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20141211/bebb7424/attachment.html>