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 ]

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.