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 ]

To my knowledge, the reference you ask for does not exist (and I would
be very interested if it did exist!). One reason I feel pessimistic
about such a reference is that it is not hard to throw in a few more
items to your list to end up with active research questions (for
example the best/right/satisfying way to combine "linearity" and
"dependent types" is still in discussion, as well as "dependent types"
plus "continuations").

You might however still be interested in references that cross
some of these non-trivial bridges between features, looking at
the elephant(s) from different angles. The pointers below are in no
way intended as pinpointing the first paper to discuss these ideas,
but rather entry points that I personally found enlightening on these
questions.

(1) Polymorphism, subtyping, and recursive types. An interesting work
on how to compose these features in a system that seeks to be
"maximally expressive" and remain sound is the following PhD thesis,

  "Erasable coercions: a unified approach to type systems"
  Julien Crétin, 2014
  http://phd.ia0.fr/

The system exposed in this work subsumes, in a composable way,
existing type systems mixing polymorphism and subtyping (such as
F-eta, various flavors of F-sub, MLF, and ML dialects with ground
subtyping constraints). It is however more on the semantic side: it
will show how to compose those features to automagically obtain an
expressive system (that is sound), but it does not tell you anything
about decidability of the resulting system or type-inference. (It also
contains a reconstruction of variance using refinement kinds.)

(2) Mutable references, subtyping and intersection/union types. I
appreciated the hands-on explanation of the interaction of mutable
state and intersection/union types in

  "Type Assignment for Intersections and Unions in Call-by-Value Languages"
  Joshua Dunfield and Frank Pfenning, 2003
  http://www.cs.cmu.edu/~joshuad/papers/union-assignment/

I found that they rather crisply motivate the need for a "context
restriction", which is the intriguing dual of the value restriction
that is not part of the working experience of ML programmers. (The
algorithmic aspect of the type system are not described in this paper
but in later work on "tridirectional type-checking"). At a more
semantic level, two papers explain *why* this phenomenon appear in
programming languages:

  "Refinement Types and Computational Duality",
  Noam Zeilberger, 2009
  http://www.cs.cmu.edu/~noam/refinements/

  "Focalisation and classical realisability",
  Guillaume Munch-Maccagnoni, 2009
  http://guillaume.munch.name/papers/#focreal

(It has been known for much longer than implicit union or existential
types require careful handling when doing syntactic soundness proof
through subject reduction, see for example "Intersection and Union
Types: Syntax and Semantics", Franco Barbanera, Mariangola
Dezani-Ciancaglini and Ugo De'Liguoro, 1995)

(3) Subtyping and mutable state, fine-grained. I was first surprised
to learn that, whereas ML-style "weak" references are invariant (and
in some sense this is the reason for the need for the value
restriction), linear, uniquely-owned "strong" references, which
support strong updates (changing the type of the reference), can
soundly be made covariant. The invariance requirement comes from the
sharing / duplicability of weak references, or the fact that its
implementation on top of strong references requires hidden state.
(There work on sound higher-order programming and sound concurrent
programming meet again: duplicable weak references and concurrent
locks seem to be two sides of the same coin.). See for example the
2014 online draft

  "The design and formalization of Mezzo, a permission-based
programming language",
  Thibaut Balabonski, François Pottier, and Jonathan Protzenko,
  http://gallium.inria.fr/~fpottier/publis/bpp-mezzo-journal.pdf
  (the relevant remark is the bottom half of page A:35)


(4) Making them work all together. Semantic techniques have been
unreasonably effective at making all these aspects work together. For
a model of all of subtyping, mutable references, and
union/intersection, universal and existential types, and recursive
types, see for example

  "A Very Modal Model of a Modern, Major, General Type System"
  Andrew Appel, Paul-André Melliès, Christopher D. Richards, Jérôme
Vouillon, 2007
  http://www.pps.univ-paris-diderot.fr/~vouillon/publi/modalmodel.pdf

On Mon, Jun 15, 2015 at 5:08 AM,  <[email protected]> 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?