search

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.
https://code.google.com/p/epigram
MIT License
47 stars 7 forks source link

Reversible Elaborator #42

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
To change from my usual software-engineering dogma, here is a funny request.

Right now, we have an Elaborator from Display syntax to Evidences. This 
elaborator is written in the ElabMonad DSL. Then, we have written a Distiller, 
from Evidences to Display syntax. 

Ideally, we have the invariants that Elaboration . Distillation == id and 
Distillation . Elaboration == id. (btw, this is an invariant that ought to be 
stated and, if possible, quickchecked)

Well, if we could automatically compute the "reverse" of an elaboration 
program, we would get the corresponding distiller, and ensure these invariants 
once and for all.

As Adam pointed out when discussing this, the current DSL is too powerful for 
doing that. It is also not powerful enough to do other things (related to 
solving goals on the fly). So, there is some kind of trade-off to be had in the 
re-design of the ElabMonad DSL.

Original issue reported on code.google.com by pedag...@gmail.com on 11 Aug 2010 at 7:09