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

[Derek Dreyer]

To inject a different point of view into this discussion:

There's a lot more to the "interaction" of different type system
features than just how the combination of those features affects
typechecking, type soundness, etc., which seems to be the main focus
of the discussion so far.  In particular, from my perspective, one of
the most important functions of types (particularly ADTs) is to enable
programmers to reason modularly about their code.  And indeed
programmers often do alarmingly sophisticated (informal) modular
reasoning about their code without batting an eye.  But the
correctness of such reasoning can be easily subverted by subtle
interaction of language features.

I myself got interested in semantics and verification research about 8
years ago, when I realized that the correctness of very standard kinds
of programming patterns, involving the ubiquitous combination of
higher-order functions, ADTs and mutable state, did not rest on any
solid semantic foundations.  There had been a long line of prior work
attempting to build such foundations, by Reynolds, Oles, O'Hearn,
Tennent, Felleisen, Hieb, Mason, Talcott, Birkedal, Harper, Pitts,
Stark, Reddy, Benton, Sumii, Pierce, Støvring, Lassen, Levy, and
Sangiorgi, among others, but it was not up to the task of accounting
for the unrestricted combination of such features that one finds in,
say, ML.  This led us to a series of papers attempting to establish
such foundations, building on recent developments in Kripke logical
relations (notably Appel et al.'s "step-indexing" technique).  A good
entry point would be these two papers (although I would suggest you
gloss over the technical details at first and focus on the informal
exposition):

- "State-dependent representation independence."
Ahmed, Dreyer, Rossberg.  In POPL 2009.
http://www.mpi-sws.org/~dreyer/papers/sdri/main-short.pdf

- "The impact of higher-order state and control effects on local
relational reasoning."
Dreyer, Neis, Birkedal.  In ICFP 2010, later in JFP'12.
http://www.mpi-sws.org/~dreyer/papers/stslr/journal.pdf

There were also various competing approaches based on different kinds
of bisimulations -- see the latter paper above for citations and
comparison.  That paper in particular was inspired by Abramsky et
al.'s work on the "semantic cube", a programme in game semantics
research to build fully abstract characterizations of different axes
in the design space of language expressiveness (e.g. control
operators, higher-order state) in terms of the presence/absence of
various restrictions on game strategies.  We developed some analogous
axes in the reasoning space of Kripke logical relations.  However, the
particular techniques we used were pretty different from the
game-semantic ones, and our focus was on developing practical
techniques for reasoning about common programming patterns rather than
on full abstraction.

In more recent years, we (and various collaborators) have extended
these kinds of semantic models to handle features like concurrency and
substructural typing as well, and we have developed higher-order
separation logics for abstracting the relevant reasoning principles
that these models support.  We have not (yet) looked at
intersection/union types or subtyping.

Best regards,
Derek


On Sun, Jun 14, 2015 at 8:08 PM,  <hgualandi at inf.puc-rio.br> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> I'm interested in the problems that appear when you mix together different
> programming language features in the same language and type system. For
> example, parametric polymorphism and subtyping are very simple and easy to
> use by themselves but lots of tricky variance and type inference problems
> pop up when you mix both of them in a single language.
>
> I was wondering if there exists a comprehensive survey somewhere that
> covers how different type system features interact with each other. The
> only one I know of is Barendregt's Lambda Cube -- each axis of the cube is
> a different "feature" and each vertex corresponds to a different
> combination of features. However, the Lambda Cube doesn't cover things
> like subtyping, mutable references, intersection/union types, etc. Is
> there something out there that does?