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

[Peter Sewell]

You might want to look at Levin & Pierce's TinkerType:

http://www.cis.upenn.edu/~bcpierce/papers/index.shtml#Modular%20Type%20Systems

which IIRC had some notion of type-system-feature incompatibility.

Peter

On 16 June 2015 at 16:23,  <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.