Content deleted Content added
m →Example: remove lines |
→Implementations: Reference an early form of this idea in a 1966 work of Hoare, and make explicit Tobin-Hochstadt's name for stylistic consistency within the section. |
||
| (21 intermediate revisions by 12 users not shown) | |||
Line 1:
{{Type systems}}
In [[programming language theory]], '''flow-sensitive typing''' (
In [[Static typing|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
==
=== Ceylon ===
Line 35:
</syntaxhighlight>
Hello, object 1!
Hello, John Doe!
String.size is 8</
=== Kotlin ===
Line 62:
== Benefits ==
This technique coupled with type inference reduces the need for writing [[Type signature|type annotations]] for all variables or to do [[Type conversion|type casting]], like is seen with [[Dynamic typing|dynamic languages]] that use [[duck typing]]. It reduces [[verbosity]] and makes
It can also help language implementers
Finally, it increases [[type safety]] and can prevent problems due to [[null pointer]]s{{How|date=March 2020|title=The citation later is for the quote, flow sensitive typing doesn't seem to improve null-safety, a null-safe type system will. Possible confusion as these languages have nullable/non-nullable types, as checking null-safety through flow-sensitive typing generally equates to a null check without it}}, labeled by [[C.A.R. Hoare]]—the null reference inventor—as "the billion dollar mistake"<ref>{{cite web
|url=http://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare
|title=Null References: The Billion Dollar Mistake
Line 74:
|quote=I call it my billion-dollar mistake. It was the invention of the null reference in 1965. At that time, I was designing the first comprehensive type system for references in an object oriented language ([[ALGOL W]]). My goal was to ensure that all use of references should be absolutely safe, with checking performed automatically by the compiler. But I couldn't resist the temptation to put in a null reference, simply because it was so easy to implement. This has led to innumerable errors, vulnerabilities, and system crashes, which have probably caused a billion dollars of pain and damage in the last forty years.}}</ref>
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."<ref>{{cite journal |last1=Wright |first1=Andrew |last2=Cartwright |first2=Robert |title=A practical soft type system for scheme |journal=ACM Transactions on Programming Languages and Systems |date=1 Jan 1997 |volume=19 |issue=1 |pages=87--152 |doi=10.1145/239912.239917 |url=https://dl.acm.org/doi/abs/10.1145/239912.239917 |access-date=2024-05-04}}</ref>
==Implementations==▼
▲==History and Implementations==
The history of the idea goes back at least to [[Tony Hoare]]'s "record class discriminators" from the mid-1960s.<ref>{{cite conference |last=Hoare |first=C. A. R. |date=September 12–16, 1966 |title=Record Handling |url=https://archive.computerhistory.org/resources/text/Knuth_Don_X4100/PDF_index/k-9-pdf/k-9-u2293-Record-Handling-Hoare.pdf |conference=NATO Summer School |___location=Villard-de-Lans |access-date=2025-08-16 |quote-page=18, section 3.4 |quote=The result of using a construction of this form is that whichever of the alternative sections of program is selected at run time, the translator knows at compile time which subclass of record is actually referenced by the variable e at the time when execution of that section of program is initiated. Thus within each of the sections of program, the variable e may safely be used in field designators for private fields of the relevant subclass, exactly as if it had been restricted by declaration to point only to records of that subclass.}}</ref> However, practical type systems including it as a feature are much more recent.
Since this introduction, other languages have made use of it, namely [[Ceylon (programming language)|Ceylon]],<ref>{{cite web | url=http://ceylon-lang.org/documentation/1.2/introduction/#typesafe_null_and_flow_sensitive_typing | title=Ceylon - Quick introduction - Typesafe null and flow-sensitive typing | publisher=ceylon-lang.org | accessdate=11 March 2016}}</ref> [[Kotlin (programming language)|Kotlin]],<ref>{{cite web | url=https://kotlinlang.org/docs/reference/null-safety.html | title=Null Safety | publisher=kotlinlang.org | accessdate=11 March 2016}}</ref><ref>{{cite web | url=https://kotlinlang.org/docs/reference/typecasts.html | title=Type Checks and Casts | publisher=kotlinlang.org | accessdate=11 March 2016}}</ref> [[TypeScript]]<ref>{{cite web | url=https://blogs.msdn.microsoft.com/typescript/2014/11/18/typescript-1-4-sneak-peek-union-types-type-guards-and-more | title=TypeScript 1.4 sneak peek: union types, type guards, and more | publisher=blogs.msdn.microsoft.com | date=18 November 2014 | accessdate=11 March 2016 | author=Ryan Cavanaugh}}</ref> and [[Facebook]] Flow.<ref>{{cite web | url=https://code.facebook.com/posts/1505962329687926/flow-a-new-static-type-checker-for-javascript | title=Flow, a new static type checker for JavaScript | publisher=code.facebook.com | date=18 November 2014 | accessdate=11 March 2016 | authors=Avik Chaudhuri, Basil Hosmer, Gabriel Levi}}</ref>▼
Typed Scheme, a type system for [[Scheme (programming language)|Scheme]] developed by Sam Tobin-Hochstadt and first published in 2008, was the first type system to include occurrence typing.<ref>{{cite web |title=The Design and Implementation of Typed Scheme {{!}} POPL, 2008 |url=https://dl.acm.org/doi/10.1145/1328438.1328486 |website=dl.acm.org}}</ref> Its successor, Typed Racket (a dialect of [[Racket (programming language)|Racket]]), is also based on occurrence typing.<ref>{{cite web |title=5 Occurrence Typing |url=https://docs.racket-lang.org/ts-guide/occurrence-typing.html |website=docs.racket-lang.org}}</ref> Shortly after Typed Scheme, David J. Pearce independently reinvented flow-typing in [[Whiley (programming language)|Whiley]].<ref>{{cite web | url=http://whiley.org/2010/09/22/on-flow-sensitive-types-in-whiley/ | title=On Flow-Sensitive Types in Whiley | publisher=whiley.org | date=22 September 2010 | access-date=11 March 2016 | author=David J. Pearce | archive-date=11 March 2016 | archive-url=https://web.archive.org/web/20160311184700/http://whiley.org/2010/09/22/on-flow-sensitive-types-in-whiley/ | url-status=dead }}</ref><ref>{{cite web | url=http://whiley.org/guide/typing/flow-typing/ | title=Whiley - Flow Typing | publisher=whiley.org | date=8 April 2012 | access-date=11 March 2016 | author=David J. Pearce | archive-date=11 March 2016 | archive-url=https://web.archive.org/web/20160311184703/http://whiley.org/guide/typing/flow-typing/ | url-status=dead }}</ref>
▲
There are also a few languages that don't have [[Tagged union|union types]] but do have [[nullable types]], that have a limited form of this feature that only applies to nullable types, such as [[C Sharp (programming language)|C#]],<ref>{{cite web |title=Design with nullable reference types |url=https://docs.microsoft.com/en-us/dotnet/csharp/tutorials/nullable-reference-types#create-respondents-and-get-answers-to-the-survey |website=docs.microsoft.com |language=en-us}}</ref> [[Kotlin (programming language)|Kotlin]],<ref>{{cite web | url=https://kotlinlang.org/docs/reference/null-safety.html | title=Null Safety | publisher=kotlinlang.org | access-date=11 March 2016}}</ref><ref>{{cite web | url=https://kotlinlang.org/docs/reference/typecasts.html | title=Type Checks and Casts | publisher=kotlinlang.org | access-date=11 March 2016}}</ref> and Lobster.<ref>{{cite web |title=The Lobster Type System |url=http://aardappel.github.io/lobster/type_checker.html#the-trouble-with-nil |website=aardappel.github.io}}</ref>
==Alternatives==
[[Pattern matching]] reaches the same goals as flow-sensitive typing, namely reducing [[verbosity]] 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]] because all the cases can be enumerated and statically checked by the compiler.
See this example mock for Java:<ref>{{cite web |title=JEP 441: Pattern Matching for switch| url=https://openjdk.org/jeps/441|website=openjdk.org |language=en-us |date=19 September 2023 |access-date=14 November 2023 |author=Gavin Bierman and Brian Goetz}}</ref>
<syntaxhighlight lang="java">
int eval(Node n) {
return switch(n) {
// try to type cast "Node" into "IntNode", and create the variable "i" of type "int".
// If that works, then return the value of "i"
case IntNode(int i) -> i;
// try to type cast "Node" into "NegNode", and create the variable "n" of type "Node".
// If that works, then return the negation of evaluating the "n" node
case NegNode(Node n) -> -eval(n);
// try to type cast "Node" into "AddNode", and create the variables "left" and "right" of type "Node".
// If that works, then return the addition of evaluating the "left" and "right" nodes
case AddNode(Node left, Node right) -> eval(left) + eval(right);
// try to type cast "Node" into "MulNode", and create the variables "left" and "right" of type "Node".
// If that works, then return the multiplication of evaluating the "left" and "right" nodes
case MulNode(Node left, Node right) -> eval(left) * eval(right);
// no "default" because the compiler knows all the possible cases have been enumerated
};
}
</syntaxhighlight>
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==
<references />
| |||