Anthony Di Franco wrote:
On Mon, Sep 14, 2009 at 15:18, Adam Chlipala <[email protected]> wrote:
Could you describe
a concrete change to the compiler and an example program that would benefit
from that change?
The concrete change to the compiler / language would be to make it use
OTT to type programs, instead of or in addition to the heuristics it
already uses. I'm incapable of thinking of an example program due to
lack of familiarity with the alternatives in question, but the general
idea is there might be something your heuristics can't type but that a
really principled but still powerful approach, which is what I take
OTT to be, could. No one may ever care in practice, of course. I'm
just interested from a distance in how things in dependently-typed
languages are shaking out.
OTT would be much less effective than what's currently implemented, to
the point of unusability for most functional programmers. I understand
that you're not familiar with the details of the type theory world, but
I really can't say anything more unless you present a concrete
proposal. "Use OTT to type programs" isn't concrete, because OTT is a
type system, not an algorithm. No one programs with
fully-type-annotated programs, so there's the critical element of
choosing a type inference algorithm.
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
