[Ur] Ur/web type system and security

[Anthony Di Franco]

On Mon, Sep 14, 2009 at 15:30, Adam Chlipala <adamc at impredicative.com> wrote:
> Anthony Di Franco wrote:
>>
>> On Mon, Sep 14, 2009 at 15:18, Adam Chlipala <adamc at impredicative.com>
>> 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.

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.  So I guess the
question becomes, is OTT incompatible with Ur's type system, and if
so, how?  Would the heuristic approach of Ur benefit from knowing
about the regularities OTT apparently (to me) can make evident,
practically speaking?

Formally speaking, how sure are you about Ur's heuristics?  How does
one falsify a wrong one?