[TYPES] RFC: ARF - An interprocedural flow-based type checker

[David Foster]

On 9/10/15, 1:48 AM, Gabriel Scherer wrote:
 > I was not entirely satisfied with the complexity argument you provide.
 > [...]
 > However, this assumption that the corner cases cover all possible
 > programs is not clear to me.

Indeed. This initial analysis is just a first approximation.

 > In particular, the work of Christian Mossin on flow analysis seems 
relevant.

Thanks! I will take a look.


On 9/10/15, 3:52 AM, Francois Pottier wrote:
 > It may be worth noting that the paper "Constraint Abstractions" by
 > J. Gustavsson and J. Svenningsson offers a pleasant, constraint-based 
view of
 > flow analysis and a significant improvement in complexity compared with
 > Mossin's algorithm.

Thanks! I will also take a look.


On 9/10/15, 8:41 AM, hgualandi at inf.puc-rio.br wrote:
> I am not familiar with the Whiley language and with the references that
> Gabriel and François provided but I am familiar with some of the
> literature on type inference for dynamically typed languages. So here
> comes a bit of a brain dump of things from my masters...

Thank you Hugo. These references are extremely useful.

 > On a cursory glance, the types you infer for Python are unions of base
 > types. This reminds me of the Soft Typing work for Scheme, from the 90s.

Indeed: If you have "if { x = <int> } else { x = <bool> }; return x;", 
the return type will be inferred as int|bool.

 > One of the interesting
 > features of soft typing systems is that by classifying operations 
this way
 > the output in case of a type error is more informative than just 
saying "I
 > failed to typecheck your program because some types didn't match".

That is encouraging to hear. Having extremely clear error messages from 
the type checker is a very high priority for the larger type checker I'm 
designing. (It's item #3 in the mission statement.)

 > One thing that  you should be aware of is that global type inference is
 > very brittle, which is partly a reason why people have been moving on to
 > Optional Typing and Gradual Typing for dynamic languages lately [8].

By brittle do you mean that small changes in the program source text can 
easily cause large parts of the program to type differently? Or some 
other property?