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 clo ...
, 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 to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer progra ...
where the type of an
expression
Expression may refer to:
Linguistics
* Expression (linguistics), a word, phrase, or sentence
* Fixed expression, a form of words with a specific meaning
* Idiom, a type of fixed expression
* Metaphorical expression, a particular word, phrase, ...
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 (, ; si, ශ්රී ලංකා, Śrī Laṅkā, translit-std=ISO (); ta, இலங்கை, Ilaṅkai, translit-std=ISO ()), formerly known as Ceylon and officially the Democratic Socialist Republic of Sri Lanka, is an ...
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
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 t ...
. It reduces
verbosity
Verbosity or verboseness is speech or writing that uses more words than necessary. The opposite of verbosity is plain language. Some teachers, including the author of ''The Elements of Style'', warn against verbosity; similarly Mark Twain and Er ...
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 i ...
and can prevent problems due to
null pointer
In computing, a null pointer or null reference is a value saved for indicating that the pointer or reference does not refer to a valid object. Programs routinely use null pointers to represent conditions such as the end of a list of unknown lengt ...
s, labeled by
C.A.R. Hoare
Sir Charles Antony Richard Hoare (Tony Hoare or C. A. R. Hoare) (born 11 January 1934) is a British computer scientist who has made foundational contributions to programming languages, algorithms, operating systems, formal verification, and c ...
—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 A scheme is a systematic plan for the implementation of a certain idea.
Scheme or schemer may refer to:
Arts and entertainment
* ''The Scheme'' (TV series), a BBC Scotland documentary series
* The Scheme (band), an English pop band
* ''The Schem ...
, 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 whe ...
.
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 (, ; si, ශ්රී ලංකා, Śrī Laṅkā, translit-std=ISO (); ta, இலங்கை, Ilaṅkai, translit-std=ISO ()), formerly known as Ceylon and officially the Democratic Socialist Republic of Sri Lanka, is an ...
,
TypeScript
TypeScript is a free and open source programming language developed and maintained by Microsoft. It is a strict syntactical superset of JavaScript and adds optional static typing to the language. It is designed for the development of large appl ...
and
Facebook
Facebook is an online social media and social networking service owned by American company Meta Platforms. Founded in 2004 by Mark Zuckerberg with fellow Harvard College students and roommates Eduardo Saverin, Andrew McCollum, Dustin ...
Flow.
There are also a few languages that don't have
union types but do have
nullable types
Nullable types are a feature of some programming languages which allow a value to be set to the special value NULL instead of the usual possible values of the data type. In statically typed languages, a nullable type is an option type, while in ...
, 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 has to be exact: "either it will or will not be ...
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 plain language. Some teachers, including the author of ''The Elements of Style'', warn against verbosity; similarly Mark Twain and Er ...
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 type, i.e., a type formed by combining other types.
Two common classes of algebraic types are product types (i.e., t ...
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