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 ]


On Jun 16, 2015, at 11:23 AM, [email protected] wrote:

> 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. 


This is a mistaken assumption (as Michael indicated in his response). 

I have conducted research on adding types to untyped^1 languages since 1988, 
starting with a (failed) collaboration with Mike Fagan and Corky Cartwright. 

To be precise, I proposed viewing untyped languages as unityped languages 
with a universal type plus injections and projections. Fritz Henglein worked
out the idea in the mid 1990s. 

My goal has always been to work out the theory and to implement it to see 
whether it would work pragmatically. 

From ~92 to 2004, I focused on inferring types with three soft type systems: 
one based on Hindley-Milner type inference and another two using SBA (or CFA, 
almost) based type inference.  Andrew Wright's dissertation and Soft Typed Scheme
(co-adviced by Corky and myself), Cormac Flanagan's on SBA and MrSpidey Scheme, 
and Phiippe Meunier on contracted SBA were the major results along the way. 
Theoretically all three look fine. Pragmatically all three suffer from serious
problems when it comes to explaining failures of type inference. (And i can 
tell you from observations of numerous uses, that failure means suffering.)

Recognizing this problem in the late 90s, Robby Findler and I explored contracts
as (at first) a supplement for type inference and/or a replacement for type systems. 
His dissertation or our ICFP 2002 paper are good starting points. Racket (then
PLT Scheme) showed that contracts were useful, and programmers quickly started 
using them in lieu of types. 

Around 2005 I decided to try a new path with Sam Tobin-Hochstadt, the incremental 
addition of explicit type annotation. I realized that we needed to protect the 
already typed parts from untyped code, which may have different expectations of
the code than the type annotations express. Not surprisingly, contracts were the 
solution to this problem, which our experience with soft type systems had suggested. 

We immediately realized that these protection mechanisms would impose a significant
run-time cost so we focused on the conversion of entire modules. While our DSL 2006
paper does not use the slogan 'gradual typing', we essentially co-invented the 
idea one month apart from Siek and Taha (who published in the Scheme Workshop). 
Now we call 

 Siek and Taha's idea "micro gradual typing"  (applies to individual expressions) 
 our own approach we dubbed "macro gradual typing" (applies to modules only) 

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. For theoretical ideas on what we need to accommodate
idioms see 

 POPL 2008
 ESOP 2009  
 ICFP 2010
 OOPSLA 2012

For practical insights, see 

 Scheme 2007
 STOP 2009 
 PLDI 2011  
 PADL 2012 
 ECOOP 2015 (my favorite related work section, start tracing back from here) 

Both the Siek/Taha approach and the Tobin-Hochstadt/Felleisen approach emphasize SOUNDness 
of the interaction. See Dimoulas 2012 for a pragmatic proof technique; Wadler and Findler
introduced a theoretical proof technique (see Michael's message) but you should also look
at Fritz's work from the mid-90s for ideas here. 

In addition to sound gradual typing, people have also explored unsound gradual typing, 
which you may also dub optional type systems. My personal acquaintance with such approaches
dates back to Common Lisp's idea of "optional types" in the mid 1980s. 

The above is my personal strand of work, not a complete history: 

-- Soft typing was anticipated by work on SmallTalk in the early 1980s; see POPL. 
-- Theoretical approaches to (gradual?) types for Lisp show up in Cartwright's dissertation (76)
-- parallel to Fagan, we also have quasi-static typing (Thatte)
-- adding DYN to statically typed languages (Abadi Cardelli Pierce and Plotkin) 

And lastly, your mail implies a compiler-biased view. 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. 

-----
^1 While semantically such languages are unityped, pragmatically they 
are multi-typed. Sadly and contrary to Jim Morris's advice, and perhaps 
following his example, PL researchers tend to substitute 'easy' semantics
problems for the 'hard' pragmatics problem that real programmers face in 
the real world.