Re: [TYPES] I'm searching for a survey on type system feature combinations

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


On Jun 16, 2015, at 7:46 PM, [email protected] wrote:

>> The theoretical difficulty of adding type annotations to untyped languages
>> is that untyped languages promote multi-typed thinking and the programming
>> idioms that develop show this. So your type system has to accommodate
> these grown
>> idioms, otherwise programmers reject this.
> 
> Exactly! However what is idiomatic depends a lot on the original language.
> For example, Typed Lua devotes a big chunk of their type system to model
> incremental table definition via multiple assignment statements. In Typed
> Racket this isn't an issue because untyped Racket already encourages you
> to declare the field names in your data types. (OTOH, Typed Racket needs
> to model the numeric tower and variadic map and filter, which are not
> common in Lua)


This is totally correct. A (sound) gradual type system must be tailored to 
the existing language because programmers (on the average) will not 
tolerate breaking their habits, i.e., changing their idioms to accommodate
the type checker. They already have (probably subconsciously) incorporated
a type-like system for thinking about their code and impedance mismatches
between two different systems of thinking are hard to overcome. (This
doesn't just apply to type systems.) 

My hunch is that 
 (1) even Lua can benefit from FP TR's most interesting innovation 
       (occurrence typing; NOTE: contrary to the implication in Gabriel's 
        next message, TR does of course NOT require a global program 
        analysis.) 

 (2) Lua might benefit from Asumu Takikawa's approach to OO TR

 (3) you would most likely benefit from Shriram Krishnamurthi and Arjun 
       Gua's work on JavaScript types because (a) they also face a table-ish 
       and imperative approach to typing. They have also pioneered an 
       elegant integration of type checking and flow analysis (and yet, 
       they integrate occurrence typing too). 

[This is partly based on meetings with Roberto.]


> What confuses me is that in an attempt to tame these dynamic language
> idioms type system designers end up using almost every type system
> technology under the sun. Its very overwhelming and I naively wished that
> there might be something to help me organize the tools that all those
> languages use.


Not only did we integrate a lot of features from existing type system work 
(true unions, parametric polymorphism; first-class polymorphism;;  local inference), we 
also had to invent and add new ideas (occurrence typing, variable-arity polymorphism, 
row-polymorphism, for mixins). Beyond that, sound gradual typing work had to 
ensure that every linguistic construct in the type language can be compiled to 
contracts (or at least, we need to error out if someone connects typed and 
untyped modules when the former use non-dynamic feature).^1 

Again the key is that dynamically typed (untyped) languages have developed
idioms that are based on programmers' ways of mixing and matching "type 
systems" to reason about their code. Whether they do it explicitly (like I do) 
or implicitly (I assume the vast majority) doesn't matter. A type system
must accommodate this mixing and matching. 

Theoreticians ought to have fun with this playing field, but I will admit, it 
first takes a lot of labor to understand the pragmatics behind a code base. 

-- Matthias

-----
^1 Always keep in mind that 'type systems' can express more properties
about program (values) than code.