Gradual typing

Last updated December 06, 2023

Gradual typing is a type system in which some variables and expressions may be given types and the correctness of the typing is checked at compile time (which is static typing) and some expressions may be left untyped and eventual type errors are reported at runtime (which is dynamic typing). Gradual typing allows software developers to choose either type paradigm as appropriate, from within a single language.^[1] In many cases gradual typing is added to an existing dynamic language,^[2] creating a derived language allowing but not requiring static typing to be used. In some cases a language uses gradual typing from the start.

History

The term was coined by Jeremy Siek, who developed gradual typing in 2006 with Walid Taha.^[1]^{[ non-primary source needed ]}

Implementation

In gradual typing, a special type named dynamic is used to represent statically-unknown types. The notion of type equality is replaced by a new relation called consistency that relates the dynamic type to every other type. The consistency relation is reflexive and symmetric but not transitive.^[3]

Prior attempts at integrating static and dynamic typing tried to make the dynamic type be both the top and bottom of the subtype hierarchy. However, because subtyping is transitive, that results in every type becoming related to every other type, and so subtyping would no longer rule out any static type errors. The addition of a second phase of plausibility checking to the type system did not completely solve this problem.^[4]^[5]

Gradual typing can easily be integrated into the type system of an object-oriented language that already uses the subsumption rule to allow implicit upcasts with respect to subtyping. The main idea is that consistency and subtyping are orthogonal ideas that compose nicely. To add subtyping to a gradually-typed language, simply add the subsumption rule and add a subtyping rule that makes the dynamic type a subtype of itself, because subtyping is supposed to be reflexive. (But do not make the top of the subtyping order dynamic!)^[6]

Examples

Examples of gradually typed languages derived from existing dynamically typed languages include Closure Compiler, TypeScript (both for JavaScript ^[7]),^[8] Hack (for PHP), PHP (since 7.0^[9]), Typed Racket (for Racket ^[10]^[11]), Typed Clojure (for Clojure),^[12] Cython (a Python compiler), mypy (a static type checker for Python),^[13] pyre (alternative static type checker for Python),^[14] or cperl (a typed Perl 5). ActionScript is a gradually typed language^[15] that is now an implementation of ECMAScript, though it originally arose separately as a sibling, both influenced by Apple's HyperTalk.

A system for the J programming language has been developed,^[16] adding coercion, error propagation and filtering to the normal validation properties of the type system as well as applying type functions outside of function definitions, thereby the increasing flexibility of type definitions.

Conversely, C# started as a statically typed language, but as of version 4.0 is gradually typed, allowing variables to be explicitly marked as dynamic by using the dynamic type.^[17] Gradually typed languages not derived from a dynamically typed language include Dart, Dylan, and Raku.

Raku (formerly Perl6) has gradual typing implemented from the start. Type checks occur at all locations where values are assigned or bound. An "untyped" variable or parameter is typed as Any, which will match (almost) all values. The compiler flags type-checking conflicts at compile time if it can determine at compile time that they will never succeed.

Objective-C has gradual typing for object pointers with respect to method calls. Static typing is used when a variable is typed as pointer to a certain class of object: when a method call is made to the variable, the compiler statically checks that the class is declared to support such a method, or it generates a warning or error. However, if a variable of the type id is used, the compiler will allow any method to be called on it.

The JS++ programming language, released in 2011, is a superset of JavaScript (dynamically typed) with a gradual type system that is sound for ECMAScript and DOM API corner cases.^[18]

Related Research Articles

A programming language is a system of notation for writing computer programs.

Design by contract (DbC), also known as contract programming, programming by contract and design-by-contract programming, is an approach for designing software.

In computer programming, the scope of a name binding is the part of a program where the name binding is valid; that is, where the name can be used to refer to the entity. In other parts of the program, the name may refer to a different entity, or to nothing at all. Scope helps prevent name collisions by allowing the same name to refer to different objects – as long as the names have separate scopes. The scope of a name binding is also known as the visibility of an entity, particularly in older or more technical literature—this is in relation to the referenced entity, not the referencing name.

Multiple dispatch or multimethods is a feature of some programming languages in which a function or method can be dynamically dispatched based on the run-time (dynamic) type or, in the more general case, some other attribute of more than one of its arguments. This is a generalization of single-dispatch polymorphism where a function or method call is dynamically dispatched based on the derived type of the object on which the method has been called. Multiple dispatch routes the dynamic dispatch to the implementing function or method using the combined characteristics of one or more arguments.

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every term. Usually the terms are various language constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term. Type systems formalize and enforce the otherwise implicit categories the programmer uses for algebraic data types, data structures, or other components.

In computer science, a dynamic programming language is a class of high-level programming languages, which at runtime execute many common programming behaviours that static programming languages perform during compilation. These behaviors could include an extension of the program, by adding new code, by extending objects and definitions, or by modifying the type system. Although similar behaviors can be emulated in nearly any language, with varying degrees of difficulty, complexity and performance costs, dynamic languages provide direct tools to make use of them. Many of these features were first implemented as native features in the Lisp programming language.

Duck typing in computer programming is an application of the duck test—"If it walks like a duck and it quacks like a duck, then it must be a duck"—to determine whether an object can be used for a particular purpose. With nominative typing, an object is of a given type if it is declared as such. With duck typing, an object is of a given type if it has all methods and properties required by that type. Duck typing may be viewed as a usage-based structural equivalence between a given object and the requirements of a type.

Apache Groovy is a Java-syntax-compatible object-oriented programming language for the Java platform. It is both a static and dynamic language with features similar to those of Python, Ruby, and Smalltalk. It can be used as both a programming language and a scripting language for the Java Platform, is compiled to Java virtual machine (JVM) bytecode, and interoperates seamlessly with other Java code and libraries. Groovy uses a curly-bracket syntax similar to Java's. Groovy supports closures, multiline strings, and expressions embedded in strings. Much of Groovy's power lies in its AST transformations, triggered through annotations.

In computer science, type safety and type soundness are the extent to which a programming language discourages or prevents type errors. Type safety is sometimes alternatively considered to be a property of facilities of a computer language; that is, some facilities are type-safe and their usage will not result in type errors, while other facilities in the same language may be type-unsafe and a program using them may encounter type errors. The behaviors classified as type errors by a given programming language are usually those that result from attempts to perform operations on values that are not of the appropriate data type, e.g., adding a string to an integer when there's no definition on how to handle this case. This classification is partly based on opinion.

The term object-based language may be used in a technical sense to describe any programming language that uses the idea of encapsulating state and operations inside objects. Object-based languages need not support inheritance or subtyping, but those that do are also termed object-oriented. Object-based languages that do not support inheritance or subtyping are usually not considered to be true object-oriented languages.

Matthias Felleisen is a German-American computer science professor and author. He grew up in Germany and immigrated to the US in his twenties. He received his PhD from Indiana University under the direction of Daniel P. Friedman.

Racket is a general-purpose, multi-paradigm programming language and a multi-platform distribution that includes the Racket language, compiler, large standard library, IDE, development tools, and a set of additional languages including Typed Racket, Swindle, FrTime, Lazy Racket, R5RS & R6RS Scheme, Scribble, Datalog, Racklog, Algol 60 and several teaching languages.

In mathematical logic and computer science, some type theories and type systems include a top type that is commonly denoted with top or the symbol ⊤. The top type is sometimes called also universal type, or universal supertype as all other types in the type system of interest are subtypes of it, and in most cases, it contains every possible object of the type system. It is in contrast with the bottom type, or the universal subtype, which every other type is supertype of and it is often that the type contains no members at all.

Haxe is a high-level cross-platform programming language and compiler that can produce applications and source code for many different computing platforms from one code-base. It is free and open-source software, released under the MIT License. The compiler, written in OCaml, is released under the GNU General Public License (GPL) version 2.

In computer science, ahead-of-time compilation is the act of compiling an (often) higher-level programming language into an (often) lower-level language before execution of a program, usually at build-time, to reduce the amount of work needed to be performed at run time.

In computer programming, one of the many ways that programming languages are colloquially classified is whether the language's type system makes it strongly typed or weakly typed. However, there is no precise technical definition of what the terms mean and different authors disagree about the implied meaning of the terms and the relative rankings of the "strength" of the type systems of mainstream programming languages. For this reason, writers who wish to write unambiguously about type systems often eschew the terms "strong typing" and "weak typing" in favor of specific expressions such as "type safety".

Java bytecode is the instruction set of the Java virtual machine (JVM), crucial for executing programs written in the Java language and other JVM-compatible languages. Each bytecode operation in the JVM is represented by a single byte, hence the name "bytecode", making it a compact form of instruction. This intermediate form enables Java programs to be platform-independent, as they are compiled not to native machine code but to a universally executable format across different JVM implementations.

The Computer Language Benchmarks Game is a free software project for comparing how a given subset of simple algorithms can be implemented in various popular programming languages.

References

1 2 Siek, Jeremy (24 March 2014). "What is gradual typing?".
↑ Bracha, Gilad (2004). "Pluggable Type Systems". OOPSLA'04 Workshop on Revival of Dynamic Languages.
↑ Siek, Jeremy; Taha, Walid (September 2006). Gradual Typing for Functional Languages (PDF). Scheme and Functional Programming 2006. University of Chicago. pp. 81–92.
↑ Thatte, Satish (1990). "Quasi-static typing". Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90. ACM. pp. 367–381. doi:10.1145/96709.96747. ISBN 978-0897913430. S2CID 8725290.
↑ Oliart, Alberto (1994). An Algorithm for Inferring Quasi-Static Types (Technical report). Boston University. 1994-013.
↑ Siek, Jeremy; Taha, Walid (August 2007). "Gradual Typing for Objects". ECOOP 2007 – Object-Oriented Programming. Lecture Notes in Computer Science. Vol. 4609. Springer. pp. 2–27. doi:10.1007/978-3-540-73589-2_2. ISBN 978-3-540-73588-5.
↑ Feldthaus, Asger; Møller, Anders (2014). "Checking correctness of TypeScript interfaces for JavaScript libraries". Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications. Portland, Oregon, USA: ACM Press. pp. 1–16. doi:10.1145/2660193.2660215. ISBN 978-1-4503-2585-1.
↑ Swamy, N.; Fournet, C.; Rastogi, A.; Bhargavan, K.; Chen, J.; Strub, P. Y.; Bierman, G. (2014). "Gradual typing embedded securely in JavaScript" (PDF). Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '14. pp. 425–437. doi:10.1145/2535838.2535889. ISBN 9781450325448.
↑ "PHP: Function arguments - Manual » Strict typing".
↑ Tobin-Hochstadt, Sam; Felleisen, Matthias. "Interlanguage Migration: From Scripts to Programs". Proceedings of the Symposium on Object-Oriented Programming Systems, Companion Volume. Portland, OR. Tobin-Hochstadt06. Retrieved 2020-11-06.
↑ Tobin-Hochstadt, Sam; Felleisen, Matthias. "The Design and Implementation of Typed Scheme". Proceedings of the Principles of Programming Languages. San Diego, CA. Tobin-Hochstadt08. Retrieved 2020-11-06.
↑ Chas Emerick. "Typed Clojure User Guide". GitHub .
↑ Jukka Lehtosalo. "mypy - Optional Static Typing for Python".
↑ "Pyre - A performant type-checker for Python 3".
↑ Aseem Rastogi; Avik Chaudhuri; Basil Hosmer (January 2012). "The Ins and Outs of Gradual Type Inference" (PDF). Association for Computing Machinery (ACM). Retrieved 2014-09-23.
↑ "type-system-j". GitHub .
↑ "dynamic (C# Reference)". MSDN Library . Microsoft. Retrieved 14 January 2014.
↑ "The JS++ Type System, Appendix B: Problems (Why was this hard to solve?)" . Retrieved 10 February 2020.