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

[Gabriel Scherer]

On Wed, Jun 17, 2015 at 12:38 AM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
> There are numerous approaches
> to infer something like types inside the compilers for dynamically typed languages
> for performance reasons. While I can see classifying these 'things' as types, I would
> reserve the word 'type' and 'type system' for linguistic constructs that somehow
> interact with the compiler.

My personal take on the nuance between "program analysis" and "type
system" is that type systems, inside the space of program analyses,
are characterized by compositionality. It is arguably a side-effect of
type-system design that it gives a way to analyze a system without the
full view of its sub-parts, only their type -- it naturally comes from
having support for abstraction. (In the general program analysis
literature, what we consider "types" are called "summaries".)

The presence of types as linguistic constructs can be
backward-justified as a consequence of this compositionality
requirement: the guarantees given on open terms / partial components
by the type system are strong enough that providing them without
explicit annotations would be undecidable, and thus they must appear
in the syntax of programs. By contrast, many program analyses used
inside compiler are either (1) composable but pure approximations
providing no guarantees at all (eg. inlineability of small functions:
as "not inlineable" is always a valid answer, it is not affected by
Rice's theorem) or (2) non-composable / whole-program, and thus
significantly easier to compute without (linguistic) help from the
user.


On Wed, Jun 17, 2015 at 1:46 AM,  <hgualandi at inf.puc-rio.br> wrote:
> What confuses me is that in an attempt to tame these dynamic language
> idioms type system designers end up using almost every type system
> technology under the sun. Its very overwhelming and I naively wished that
> there might be something to help me organize the tools that all those
> languages use.

When designing type system or type analyses for dynamically-typed
languages, I think it is very important to have a clear picture of the
workflow you have in mind for your users: it will impact the design of
your analysis greatly.
For example, if you have a requirement to be able to analyze /
type-check large existing codebases without changing them, you cannot
afford to require your users to add type annotations. This gives
strong incentives to use a simple whole-program analysis. Yet that is
in tension with the need for scalability; it's still probably easier
to pick a global analysis requiring no annotations, sacrifice some
precision, and focus on making it go really fast.
If you design linguistic constructs for your user to support the
analysis, you may still expect to let your users write the code
exactly as before (only, annotated), or require changes of idioms in
the typed part. The former approach tends to require greater
sophistication; for example it led to the introduction of occurrence
typing for Typed Racket, which is arguably more complex to type-check
than ML-style pattern-matching but supports the idiomatic Scheme style
(in ML, constructor names are required, and serve as additional
annotations).

On Wed, Jun 17, 2015 at 1:46 AM,  <hgualandi at inf.puc-rio.br> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Maybe I shouldn't have mentioned the dynamic typing bit. That opened up a
> huge can of worms... Right now the part I am having more trouble with the
> "static type system" part than the "interacting between static and dynamic
> code" part.
>
> I appreciate the links on gradual typing and the discussion though. I
> thought that my bibliography on that was very comprehensive but this list
> is still proving me wrong :)
>
>> This is a mistaken assumption (as Michael indicated in his response).
>
> I agree, although I think part of it is just me not communicating precisely.
>
>> The theoretical difficulty of adding type annotations to untyped languages
>> is that untyped languages promote multi-typed thinking and the programming
>> idioms that develop show this. So your type system has to accommodate
> these grown
>> idioms, otherwise programmers reject this.
>
> Exactly! However what is idiomatic depends a lot on the original language.
> For example, Typed Lua devotes a big chunk of their type system to model
> incremental table definition via multiple assignment statements. In Typed
> Racket this isn't an issue because untyped Racket already encourages you
> to declare the field names in your data types. (OTOH, Typed Racket needs
> to model the numeric tower and variadic map and filter, which are not
> common in Lua)
>
> What confuses me is that in an attempt to tame these dynamic language
> idioms type system designers end up using almost every type system
> technology under the sun. Its very overwhelming and I naively wished that
> there might be something to help me organize the tools that all those
> languages use.