This one feature has popped up under different names in several recent type systems like TypeScript, Flow, Hack, Kotlin (and in a limited way, C#):
(terms that conflict with established terminology)
“Type refinement” is the term used by Facebook’s Flow and Hack. It doesn’t appear to be in use outside of Facebook. ‘Refinement’ is a good description of what’s happening, but it sounds exactly like “refinement types”, an established term since 1991 referring to a completely different possible type system feature. Refinement types are invariably in the top 3 search results for “type refinement”, so this is very confusing. (The leading implementation today is Liquid Haskell, very cool stuff, check it out.)
“Flow-sensitive typing” is probably used by the most languages, but they’re generally pretty obscure: Whiley, Groovy, Ceylon, Lobster. (Google’s Kotlin uses the term in its spec, but not in its user-facing documentation.) The problem is that “flow-sensitive” vs “path-sensitive” is established terminology in static analysis, and this feature should properly be called “path-sensitive” rather than “flow-sensitive”. (Technically, a path-sensitive analysis is usually also flow-sensitive, but calling an analysis flow-sensitive usually suggests that it’s path-insensitive, whereas this typing feature is definitely path-sensitive.)
(When Whiley originated this term, the author actually used the term “flow-sensitive” correctly, as do Groovy and Lobster, and Facebook correctly describes Flow as “path-sensitive” in their OOPSLA’17 paper. Unfortunately, the term appears to have morphed when it spread to Ceylon and Kotlin.)
(the term I think we should all use instead)
“Type narrowing” is the term used by TypeScript (and PHPStan). I think this is just as clear as ‘type refinement’, while avoiding confusion with ‘refinement types’. There is also some existing academic and industry usage of ‘narrowing’ in the sense of downcasting in Java (and Visual Basic), an extension of C++ usage for numeric types (e.g. narrowing an int64 to an int32).
(I could also live with these)
“Occurrence typing” is the term used by Typed Racket. Its predecessor Typed Scheme appears to be the first implementation of this feature. I don’t think this term is as clear as ‘type narrowing’ or ‘type refinement’, but I guess it’s clearer than ‘smart casting’ or ‘flow typing’. (It also might go beyond merely path-sensitive type narrowing?)
“Flow typing” is often used interchangeably with ‘flow-sensitive typing’, by the same languages, so I worry it’s confusing for the same reason. But I suppose it could be viewed as expressing dependence on control flow more generally, and I could buy an argument that it’s somewhat established usage.
“Smart casting” is the term used by Google’s Kotlin. It’s not very descriptive, it sounds like a “smart TV” feature (most search results are for this), and no one else uses it that I know of.
Those are okay, but not as clear as “type narrowing”, right? In any case, can we all just pick one?
(C# does not use any specific term for this feature, and has a very limited version that only supports narrowing a nullable type to a non-nullable type. Swift and Zig also both have a feature for extracting a non-nullable type from a nullable type that is superficially similar, but is actually path- and flow-insensitive and based on Haskell/ML-style pattern matching.)
