Flow-sensitive Typing
   HOME

TheInfoList



OR:

In
programming language theory Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is clos ...
, flow-sensitive typing (also called flow typing or occurrence typing) is a
type system In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a ''type'' (for example, integer, floating point, string) to every '' term'' (a word, phrase, or other set of symbols). Usu ...
where the type of an expression depends on its position in the
control flow In computer science, control flow (or flow of control) is the order in which individual statements, instructions or function calls of an imperative program are executed or evaluated. The emphasis on explicit control flow distinguishes an '' ...
. In statically typed languages, a type of an expression is determined by the types of the sub-expressions that compose it. However, in flow-sensitive typing, an expression's type may be updated to a more specific type if it follows an operation that validates its type. Validating operations can include type predicates, imperative updates, and control flow.


Examples


Ceylon

See the following example in
Ceylon Sri Lanka, officially the Democratic Socialist Republic of Sri Lanka, also known historically as Ceylon, is an island country in South Asia. It lies in the Indian Ocean, southwest of the Bay of Bengal, separated from the Indian subcontinent, ...
which illustrates the concept: // Object? means the variable "name" is of type Object or else null void hello(Object? name) hello(null); hello(1); hello("John Doe"); and which outputs:
Hello, world!
Hello, object 1!
Hello, John Doe!
 String.size is 8


Kotlin

See this example in Kotlin: fun hello(obj: Any) hello("Mooooo")


Benefits

This technique coupled with type inference reduces the need for writing type annotations for all variables or to do type casting, like is seen with dynamic languages that use
duck typing In computer programming, duck typing 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 ...
. It reduces
verbosity Verbosity, or verboseness, is speech or writing that uses more words than necessary. The opposite of verbosity is succinctness. Some teachers, including the author of ''The Elements of Style'', warn against verbosity. Similarly Mark Twain and ...
and makes for terser code, easier to read and modify. It can also help language implementers provide implementations that execute dynamic languages faster by predicting the type of objects statically. Finally, it increases
type safety 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 ...
and can prevent problems due to
null pointer In computing, a null pointer (sometimes shortened to nullptr or null) or null reference is a value saved for indicating that the Pointer (computer programming), pointer or reference (computer science), reference does not refer to a valid Object (c ...
s, labeled by C.A.R. Hoare—the null reference inventor—as "the billion dollar mistake" From a Programming Languages perspective, it's reasonable to say that flow-sensitive typing is the feature that finally made it possible to build usable type-safe programming languages with union types and without rampant dynamic checking. Until this point, attempts to add this feature to languages such as Scheme generally resulted in intractably large type representations. One example of a system with limited support for union types is Wright and Cartwright's "Soft Scheme."


Implementations

Typed Scheme, a type system for Scheme, was the first type system with this feature. Its successor, Typed Racket (a dialect of Racket), is also based on occurrence typing. Shortly after Typed Scheme, David J. Pearce independently reinvented flow-typing in
Whiley Whiley is the surname of: * Manning Whiley (1915–1975), British actor * Richard Whiley (born 1935), English cricketer * Jo Whiley (born 1965), English DJ * Matthew Whiley (born 1980), English cricketer * Jordanne Whiley (born 1992), British w ...
. Typed JavaScript observed that in "scripting" languages, flow-typing depends on more than conditional predicates; it also depends on state and control flow. This style has since been adopted in languages like
Ceylon Sri Lanka, officially the Democratic Socialist Republic of Sri Lanka, also known historically as Ceylon, is an island country in South Asia. It lies in the Indian Ocean, southwest of the Bay of Bengal, separated from the Indian subcontinent, ...
,
TypeScript TypeScript (abbreviated as TS) is a high-level programming language that adds static typing with optional type annotations to JavaScript. It is designed for developing large applications and transpiles to JavaScript. It is developed by Micr ...
and
Facebook Facebook is a social media and social networking service owned by the American technology conglomerate Meta Platforms, Meta. Created in 2004 by Mark Zuckerberg with four other Harvard College students and roommates, Eduardo Saverin, Andre ...
Flow. There are also a few languages that don't have union types but do have nullable types, that have a limited form of this feature that only applies to nullable types, such as C#, Kotlin, and Lobster.


Alternatives

Pattern matching In computer science, pattern matching is the act of checking a given sequence of tokens for the presence of the constituents of some pattern. In contrast to pattern recognition, the match usually must be exact: "either it will or will not be a ...
reaches the same goals as flow-sensitive typing, namely reducing
verbosity Verbosity, or verboseness, is speech or writing that uses more words than necessary. The opposite of verbosity is succinctness. Some teachers, including the author of ''The Elements of Style'', warn against verbosity. Similarly Mark Twain and ...
and making up for terser code, easier to read and modify. It achieves this is in a different way, it allows to match the type of a structure, extract data out of it at the same time by declaring new variable. As such, it reduces the ceremony around type casting and value extraction. Pattern matching works best when used in conjunction with
algebraic data types In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite data type, i.e., a data type formed by combining other types. Two common classes of algebraic types are product type ...
because all the cases can be enumerated and statically checked by the compiler. See this example mock for Java: int eval(Node n) In a statically typed language, the advantage of pattern matching over flow-sensitive typing is that the type of a variable always stays the same: it does not change depending on control flow. When writing down the pattern to be matched, a new variable is declared that will have the new type.


References

{{Data types Type systems Data types Program analysis Type theory