A Limited Case for Reification by Type Inference
Proof by reflection is a common and well-studied automation tool. Reification—generally written using Ltac, OCaml, typeclasses, or canonical structures—is the means by which a structured representation is derived from an unstructured representation. The reflective automation then operates on the structured representation, relying on an interpretation or denotation function to justify a correspondence between the structured and unstructured representations.
A couple of years ago, I presented a trick for blazing fast reification in two lines of Ltac—using the
pattern tactic—which I termed reification by parametricity. While I still advocate for parametricity as the preferred method of domain-specific reification, I would like to present here yet another method.
While reification typically requires meta-programming features, I was surprised and delighted to discover that, in some restricted cases, reification can be performed entirely by a combination of the notation system and type inference. In some sense, this is trivial: by redefining the basic syntactic notations, a term can be “reified” merely by writing the same symbols in another scope. In another sense, though, this trick is quite surprising: we use the notation system merely to insert “reify here” functions at every atom, and the reification itself is in fact performed by type inference. My hope is that the audience will walk away with this new trick in their toolbox, and that some day some problem will come along demanding a slight generalization of this trick, and that generalization will be new and interesting in its own right. This, after all, is how reification by parametricity was discovered.
I propose to present the one example I have for this trick: reifying the type structure of a function in a way that allows manipulations of the arguments, such as uncurrying, reassociation of the uncurried structure, and reordering. I will present the simple code for this example in detail. My goal will be that the audience understand completely how it works, why it works, and how it might be used elsewhere.
Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:30
|A Limited Case for Reification by Type Inference|
Jason Gross MIT CSAILMedia Attached File Attached
|Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml|
|Record Updates in Coq|
Tej Chajed Massachusetts Institute of Technology, USAMedia Attached File Attached
|The B+-tree Index as a Verified Software Unit|
Anastasiya Kravchuk-Kirilyuk Harvard University, Andrew Appel Princeton, Lennart Beringer Princeton UniversityFile Attached
|Automated Synthesis of Verified Firewalls|
Shardul Chiplunkar Massachusetts Institute of Technology, Clément Pit-Claudel Massachusetts Institute of Technology, USA, Adam Chlipala Massachusetts Institute of TechnologyFile Attached