Anthony Di Franco wrote:
On Sun, Sep 13, 2009 at 12:32, Adam Chlipala <[email protected]> wrote:
Anthony Di Franco wrote:
- I just glanced at the paper "observational equality, now!" and it seemed
pretty appealing although I lack the background to grasp the finer points.
What is the relationship of the ur/web type system to one along the lines
therein, relative tradeoffs between them, could the ideas there be
implemented for ur/web, are they in some maybe partial sense already?
One of the main motivations for OTT (the system from that paper) is to make
it easier to reason about programs that manipulate proofs. There are no
non-trivial "proof objects" in Ur/Web, so it's not clear that the details of
a formal definitional equality are so important. The definitional equality
in Ur/Web is already fairly fancy, including some algebraic laws about
'map'; it's nowhere near as principled as the definitional equality of Coq
or OTT, since I add new typing heuristics as they seem useful. :)
So, could OTT be used among Ur's set of heuristics as a way to type
programs that works alongside your other heuristics? If not really,
what would need to change?
I'm having trouble understanding what you're proposing. Could you
describe a concrete change to the compiler and an example program that
would benefit from that change?
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
