[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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, [email protected] 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?
