[Grace-core] Gradual Typing for Generics

[Kim Bruce]

Hi,

I finally got around to reading the core ideas in "Gradual Typing for Generics" by Ina and Igarashi.  It looks like exactly what we need for moving between the static and dynamic versions of Grace.  I haven't read the earlier papers by Siek and Taha that introduced the ideas, but this seems to go right where we need it.  Interestingly a key restriction of their work is they can't allow overloaded methods with their scheme -- so we made a good choice in banning them from Grace.

The system is a bit complex, but I'm not sure how that will impact the programmer.  They have subtyping as we know it for types that don't involve the type "dynamic", and then two other orderings that refer to a relation between types that indicates that it is plausible that the operation might be safe (as viewed statically) to allow a potentially unsafe operation to pass the type checker, and then a different and more restrictive ordering that is applied during a run-time check that ensures that everything will be OK.

In other words, the static check will fail if there is no way that the operation could succeed, while the dynamic one essentially is translated into a kind of type cast to make sure the object in focus has all operations needed at run time (i.e., to catch a "message-not-understood" error before it occurs at run-time).

I see this kind of mixed system as being mainly helpful either as a way of (implicitly) inserting run-time checks to verify the type assertions specified in the code of a dynamically typed program or as a tool to help move a dynamically typed program over to a system with all static guarantees.  I'm thus hoping that programmers need only understand the regular static checks found in standard statically typed languages and the relatively obvious run-time checks corresponding to message-not-understood kinds of errors and not need to understand the rules of the static system that just rules out totally impossible programs.  However, we would likely need real experience to see if this works.

Their system is aimed at a restricted version of Java with nominal types and an "erasure" semantics.  We won't have either of those, so hopefully we'll avoid some of their complexity.

The system essentially works by translating a program with "dynamic" occurring in a type to a program that does not involve dynamic, but inserts run-time checks (in their system using casts, in ours presumably with type-case).  A nice feature of their system is that it handles parameterized types, including those where the type parameter can be replaced by "dynamic" or (interestingly) by a bounded version of dynamic.  (See the paper for details).  The claim in the paper (I didn't read the proof) is that all "type errors" are guaranteed to occur in the cast statements, and that segments of programs without "dynamic" are guaranteed type-safe.

Given the skepticism we got last year at SPLASH about whether this was even possible, I'm hopeful that we now have a sample system to emulate (and hopefully simplify in our context).   I believe this will allow us to use dynamically typed library units in statically typed units and vice versa.

Kim


P.S.  It will take someone who has a really good understanding of this paper to implement the system, but it can essentially be seen as a pre-processor to generate a statically-typed programs with either type casts or type case.