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

[Michael Greenberg]

If you're interested in theoretical work on mixing types and dynamic
languages, the related work section of Wadler and Findler's 2007 Scheme
Workshop is a nice (but now slightly dated) place to start. Table 5.2 in my
thesis might be helpful, too (
http://repository.upenn.edu/dissertations/AAI3609166/).

There's been a lot of work on soundly mixing type disciplines with untyped
code---references (Siek and Taha 2006), effects (Bañados Schwerter, Garcia,
and Tanter 2014)---but some features have remained hard to incorporate. In
particular, parametric polymorphism is an open problem (but see Ahmed,
Findler, Siek, and Wadler http://plt.eecs.northwestern.edu/blame-for-all/).
People are just starting to work out details of how ADTs and other
structures work (how eagerly do we move a product type from dynamic to
static; how do we deal with wrapping and object equality [Allende, Fabry,
Garcia, Tanter 2014]).

There a lots of questions left about the right way to do things, soundness
aside (Siek, Vitousek, Cimini, and Boyland
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=5031). And of
course there's tons of work where people are trying these ideas out in real
languages (Typed Racket, Python, Ruby, JS, and I'm sure others).

Cheers,
Michael

On Tue, Jun 16, 2015 at 11:23 AM, <hgualandi at inf.puc-rio.br> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Thanks for the very helpful links, Julien and Gabriel. Its going to take a
> while for me to fully digest all of that (its slightly above by level :))
> but the basic impression I am getting so far is that it is important to at
> least separate "surface-level" type system features from "kernel-level"
> ones, in order to focus our attention on soundness instead of on type
> inference.
>
> Anyway, one last question: While getting a comprehensive list of how type
> systems interact runs into too many open research issues, is there at
> least such a thing as a "big list of kernel-level type system features"?
> Are Pierces "Types and programming languages" and "advanced topics in type
> systems" comprehensive or is there somewhere else I could go to if all I
> cared about was a big list?
>
> The reason I ask this is that I am working a survey on type systems for
> dynamically typed languages^1 and the impression I get from the literature
> on that is that it focuses a lot on type-inference issues (because you
> start out from languages with no type annotations) and that almost any
> kind of static program analysis counts as a type system^2. I think that a
> consistent list of kernel-level type system features might help me
> categorize things.
>
> ----
>
> 1^ If you want to be pedantic, type systems for statically typed dialects
> of unityped languages. :)
> 2^ For example, some "Soft Typing" systems are actually doing
> control-flow-analysis / closure-analysis to determine what lambdas from
> the source code flow into each call-site. The resulting "types" are things
> like "The variable f may reference the lambda from line #17 or the numeric
> constant from line #18" instead of things like "f is of type int->int".
> Mentioning line numbers like that is not like most type systems I am used
> to.
>