Anthony Di Franco wrote:
Ok, I thought there were both a type system with some nice properties and at least the starting makings of or hints at an inference algorithm that exploits them in the OTT paper.
General type inference is undecidable in any of the languages that the OTT proposal is targeting. You either apply some very domain-specific rules, or you get very weak inference.
So I guess the question becomes, is OTT incompatible with Ur's type system, and if so, how?
Ur's type system is much simpler, in terms of which constructs appear. The magic in the Ur/Web compiler is in applying high-level "definitional equality rules" that would show up as explicit coercions in Coq or OTT.
Would the heuristic approach of Ur benefit from knowing about the regularities OTT apparently (to me) can make evident, practically speaking?
I see no advantages for folks programming with Ur/Web. Most of the type constructors treated explicitly in the OTT paper are not present in Ur.
Formally speaking, how sure are you about Ur's heuristics? How does one falsify a wrong one?
In src/coq in the distribution, you can see a formal embedding of the key features of Ur into Coq. The heuristics correspond to equality lemmas, which can be proved sound with respect to that model.
_______________________________________________ Ur mailing list Ur@impredicative.com http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
