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

[hgualandi at inf.puc-rio.br]

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.