[Ur] Ur/web type system and security

[Adam Chlipala]

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.