Gradual Typing Across the Spectrum

Projects

Reticulated Python

Reticulated Python adds optional static and runtime typechecking to Python. It lets programmers annotate functions and classes with types, and it enforces these types both before and during the execution of the program, providing early detection of errors. Crucially, Reticulated does not require that all parts of a program be given static types, or even any of it. In places where typed and untyped code interact — for example, when an untyped variable is passed into a function whose argument type is Int — Reticulated can perform runtime checks ensure that the values in variables always correspond to their expected types, even when this cannot be guaranteed statically.

Reticulated Python runs on both Python 3 and Python 2.7, although the type annotation syntax is different between the two versions. Reticulated on Python 3 uses the syntactic annotations provided by Python 3 as type annotations, while Reticulated on Python 2.7 uses decorators to specify types. In both cases, the absence of an annotation implies that the parameters or return values are dynamically typed, as in standard Python. We also provide "type functions" for creating types that correspond to higher-order values in Python, like functions and lists, and we provide the type <tt>Dyn</tt> (for dynamic) to allow for, for example, heterogeneous lists, which have the type List(Dyn).

Reticulated Python itself is written in Python (specifically, the subset of Python that is syntactically compatible with both Python 2.7 and 3). Its static, compile-time component is both a "linter" or static analyzer, and a source-to-source translator. This component parses source files (using the Python ast package) and searches for type errors, rejecting programs that have statically detectable errors and syntactically inserting runtime checks or casts at boundaries between typed and untyped code, where type errors may occur.

You can find more on this site: https://github.com/mvitousek/reticulated

Diamondback Ruby

Diamondback Ruby (DRuby) is an extension to Ruby that aims to bring the benefits of static typing to Ruby without compromising the expressiveness of the language. The main features of DRuby are:

  • Type inference: DRuby uses inference to model most of Ruby’s idioms as precisely as possible without any need for programmer intervention.
  • Type annotations: Methods may be given explicit type annotations with an RDoc-inspired syntax.
  • Dynamic checking: When necessary, methods can be type checked at runtime, using contracts to isolate and properly blame any errant code, similar to gradual typing.
  • Metaprogramming support: DRuby includes a combined static and dynamic analysis to precisely model dynamic meta-programming constructs, such as eval and method_missing.
You can find more on this site: http://www.cs.umd.edu/projects/PL/druby/

Typed Racket

Typed Racket is a sister language of Racket with statically-checked type annotations. Racket and Typed Racket programs are fully interoperable: any typed functions may be used freely in untyped code and any untyped functions may be imported to typed code by supplying a type annotation. Type soundness is enforced despite these interactions by interpreting types as higher-order contracts and dynamically enforcing type-correct use.

To accomodate the flow-sensitive reasoning commonly used in untyped programs, Typed Racket employs occurrence-typing: a technique for refining the type of variables based on predicates prior to each occurrence of the variable in the control flow graph. Typed Racket is also macro-extensible and includes types for variable-arity, polymorphic functions; continuations; and first-class classes.

You can find more on this site: https://docs.racket-lang.org/ts-guide/

Pyret

Pyret is a programming language designed to serve as an outstanding choice for programming education while exploring the confluence of scripting and functional programming. It's under active design and development, and free to use or modify.

  • Pyret has Python-inspired syntax for functions, lists, and operators. Iteration constructs are designed to be evocative of those in other languages.
  • Pyret makes testing a natural part of the programming process. Functions can end in a where: clause that holds unit tests for the function. These assertions are checked dynamically.
  • Pyret allows concise, expressive, recursive data declarations. Type annotations are optional and can be added incrementally, to serve a variety of pedagogic styles and curricular needs.
You can find more on this site: https://www.pyret.org/

Pycket

Pycket is a high-performance tracing JIT compiler for Racket. Pycket supports a wide variety of the sophisticated features in Racket such as contracts, continuations, classes, structures, and dynamic binding. Compiling standard Typed Racket code through Pycket can significantly reduce the performance overhead of sound gradual typing.

You can find more on this site: http://www.github.com/pycket/pycket

Typed Clojure

Typed Clojure is an optional type system for Clojure. It understands common idioms used by Clojure programmers like multimethods, local control flow, Java interoperability, and heterogeneous maps. It is a practical system used in industry and open source.

You can find more on this site: http://typedclojure.org