javran / adding-gradual-types Goto Github PK

Need to cite and discuss Well-typed programs can’t be blamed by Wadler and Findler.
Also needs to cite preceding work by Tobin-Hochstadt and Felleisen.

The abstract needs to be shortened and put on the first page. I suggest cutting and tightening to at least 3/4 its current length.

• type consistency: static vs. dynamic checking
• type cast: when exactly does it happen?
  1. from and to dynamic types
  2. when subtyping is involved (OOP?)
• how to justify "pay-as-you-go": looks like there is an "all or nothing" runtime overhead
• observation: it's easier to extend a dynamically typed language to support gradual typing
  than extending a static one
• what are other alternatives that combines static and dynamic?
  • and description in short words
  • actually all of them could be related works: soft typing / contracts / liquid type / refinement type / dependent type
• gradual typing over other alternative solutions
  • no need of changing existing program
  • pay-as-you-go
• Safe TypeScript: appropriate to include TypeScript features?
• Typed Scheme: does it include a runtime typechecking mechanism?
• misc: proof tree in TeX?

The type consistency relation discussed in Gradual Typing for Functional Languages contains type consistency for lambda calculus, and I want to give an example that does not belong to this relation, a straightforward one is (dyn, dyn) vs. dyn -> dyn, but pairs are outside of lambda calculus. I'm wondering what to do: (1) extend the rule to support tuples, (2) Church encoding, not sure how though (3) find another example within lambda calculus

I'm wondering if there is any literature that summarizes the bad part of JavaScript

In Reticulated Python paper, they have the following type syntax:

I'm wondering how to do this with TeX, the only thing I can think of is using align* environment, are there better options?

I'm wondering is there a formal definition for this term? It seems to be used in many places in several papers and classify languages into dynamic and static ones.

Now this should be everything. Made some changes:

• Abstract is cut by about half. perhaps just read it through as most parts have been changes
• Tuned topic-of-content one layer deeper, it now looks more structured but I'm not sure whether it looks better?
• Changed some wording (mostly in section 2), but nothing major
• In Section 2.3, while talking about Reticulated Python, I included an align* environment to write out its type expression, not sure whether there is a better way of typesetting this? see #9
• Some structural change In Section 3, moving topics like "Type Inference" and "Type Erasure and Optional Typing" out of "Object-Oriented Programming", I believe this is just some formating error when adapting from the thesis style.
• Added few more sections:
  • 3.3 Blame Tracking
  • Reference this and self in 3.4 Object-Oriented Programming
  • Related Work: Added section "Like Types", "Contracts", "Blame Tracking"
  • Related Work: few more sentences in "Gradual typing" to mention about works dealing with mutable references
• Related work is reformatted using \paragraph{...} instead of \subsubsection, as it saves some spaces and looks more appropriate to me.

@dvanhorn Hi David, could you review these changes. After this I think it's good enough for final submission.

When citing multiple papers together use \cite{p1,p2} instead of \cite{p1} \cite{p2}.

Contract verification of type-like contracts gives the same blame theorem as gradual types and should be discussed in the related work section.