<p>As far as I know, for many decades, in mainstream programming languages, there were only two options to handle null-like optionality:</p>
<ol>
<li><p>Pointer or reference types are always nullable (the famous &quot;billion-dollar mistake&quot;). The programmer needs to remember to check for null wherever needed, or else the program does bad things at runtime. The compiler doesn't detect mistakes, though linters can often help.</p>
</li>
<li><p>There are separate &quot;optional&quot; or &quot;maybe&quot; wrapper types, so the programmer can't accidentally use a nullable value where a non-null value is required. This solves the problem of #1, but it means that the programmer has to introduce a new variable, with a different name, for the unwrapped value, even though it represents the same thing. (There can also be a runtime cost, if this is not compiled down to a pointer.)</p>
</li>
</ol>
<p>In the 2010s (I think?), a new way appeared, which I love.</p>
<ol start="3">
<li>Pointer or reference types are <em>usually</em> nullable, but the compiler requires a null-check where needed; it can do this because it's smart enough to detect that <code>x</code> is not null inside <code>if (x != null) { ... }</code>. This gives the safety guarantees of #2, without the downsides that I mentioned above. No downsides (that I know of).</li>
</ol>
<p>Kotlin calls that a &quot;smart cast&quot; (it works with downcasts in addition to null-checking). Swift has something similar too, requiring only adding a <code>let</code> keyword.</p>
<p>This miraculous third way, which we will hopefully enjoy in every future language... This application of flow-sensitive typing to improve the ergonomics of safe null-checking... Which language did it come from?</p>

<history><type-inference><nullability>
What language was the first to treat null checks as smart casts to non-nullable types?
CC BY-SA 4.0
2023-11-11T23:05:13.873Z
A Maybe/Option type goes a long way beyond just forcing you to write checking code; it gives you additional facilities for working with and propogating the "null" case, in the form of Monads or Streams. It also often goes alongside lots of shorthand syntax for doing so which is at least as easy to read as your "modern way", which doesn't seem particularly "miraculous" to me.
IMSoP
CC BY-SA 4.0
2023-11-11T23:27:58.223Z
[Related](https://langdev.stackexchange.com/q/360/45) (cc: @IMSoP)
Seggan
CC BY-SA 4.0
2023-11-12T01:09:30.300Z
@IMSoP You seem to have understood my question as a criticism of tagged option types? It is not that, since #2 and #3 are compatible. But it is a praise of what you called a "convenience" improvement. Maybe it is not literally miraculous :) but I don't want to program in an inconvenient language when convenient ones exist.
Eldritch Conundrum
CC BY-SA 4.0
2023-11-12T01:20:05.053Z
@EldritchConundrum Convenience is very much subjective. I find `if x != null` to be horribly ugly and not terribly convenient. I think IMSoP's point is that such a design does not allow for a different set of conveniences that Option/Result types provide. But also note that `if x != null` in the way you describe is identical to `if let Some(x) == x` in ex. Rust: and from other questions, it sounds like Swift's implementation, at least, may be syntactic sugar for it.
apropos
CC BY-SA 4.0
2023-11-12T01:38:52.313Z
"such a design does not allow for a different set of conveniences that Option/Result types provide" Why not? They are compatible. As to the more verbose variants that require adding an explicit `let`, they're good too, as long as a second name doesn't need to be introduced.
Eldritch Conundrum
CC BY-SA 4.0
2023-11-12T01:45:15.787Z
@EldritchConundrum You can reuse the same name in Haskell: `do { x <- x; Just (x + 1) }` (Note that, inside `do` notation, this is not introducing a recursive binding). This shadows the original `x`
David Young
CC BY-SA 4.0
2023-11-12T02:04:13.507Z
For completeness, [here](https://play.haskell.org/saved/jqzjoLSJ) is a full, runnable example of what I mean using an browser-based Haskell compiler.
David Young
CC BY-SA 4.0
2023-11-12T02:05:03.240Z
@DavidYoung Interesting! `x <- x` isn't the most readable null check for everyone, but it seems to accomplish something similar to flow checking, albeit with the additional constraints of being only able to return None when x is None, and generally having to be in a Maybe-returning do.
Eldritch Conundrum
CC BY-SA 4.0
2023-11-12T02:27:49.753Z
@EldritchConundrum You can effectively do a bit more with some other things, like `sequenceA`. That function will "commute" certain pairs of functors. For example, `sequenceA` will turn a `Maybe (IO ())` value into a `IO (Maybe ())` value (specifically, the outermost functor of the input has to be `Traversable` and the innermost functor has to be `Applicative`). [Here is an example of that](https://play.haskell.org/saved/AQ6rfAM5). You can also straightfowardly combine `theBody` and `example` into one function. I just separated them for clarity.
David Young
CC BY-SA 4.0
2023-11-12T02:36:28.223Z
(Also, note that, similar to the other example, the `x` in `pure (print x)` is an `Int`, not a `Maybe Int`).
David Young
CC BY-SA 4.0
2023-11-12T02:45:41.350Z
@DavidYoung Of course you can always add more code and accomplish anything, but that's getting further away from the minimality of having `if x is not null, print(x)` safely do what you mean.
Eldritch Conundrum
CC BY-SA 4.0
2023-11-12T04:07:22.530Z
The way you've presented it suggests that this feature is a completely new approach to the problem, whereas I am suggesting that it's just one feature among many that can make working with nullable or Option types more convenient. There's a whole range of scenarios and programming styles where it wouldn't make any difference, and if writing an if statement around a block was the *only* way the language offered to handle nulls, it would be significantly *less* convenient than other languages.
IMSoP
CC BY-SA 4.0
2023-11-12T08:02:01.927Z
I think that a latent issue underlying several comments above is that you characterize "the functional way" as obsolete, which is naturally going to annoy people and prompt them to argue with you about that. I think you can avoid such responses by trimming your question to focus only on the pattern you're actually asking about; or if you find it too hard to describe it without describing the alternatives to it, then you can at least try to avoid editorializing.
ruakh
CC BY-SA 4.0
2023-11-12T09:21:06.457Z
I see... Maybe the heart of the issue is that it is an improvement much more useful in non-functional languages (where `if` is the most idiomatic way to check null) than in functional languages (which have more varied ways). My question doesn't highlight the difference, maybe it should. I could also restrict the question to non-functional languages, just for clarity? However, I think that flow typing is also an improvement in functional languages. I'd like to know if it's not!
Eldritch Conundrum
CC BY-SA 4.0
2023-11-12T10:07:11.233Z
I agree with ruakh's comment, but want to stress that it doesn't fully address mine, which is that *this isn't a third way of handling nulls*. You can have a procedural or OO language that strictly checks for nulls at compile time, but doesn't use this, offering instead operators like null coalesce (var ?? default) and null chaining (var?->member)
IMSoP
CC BY-SA 4.0
2023-11-12T12:46:20.157Z
@IMSoP You seem to claim that the presence of null coalesce and null chaining operators in an OO/procedural language replace entirely the need for general case direct null-checking. My years of experience in such languages tell me that's not true! Even after using these operators everywhere you can, you are still left with direct null checks, and it is a relief when you can have flow typing for these and avoid new identifier proliferation. (I'm starting to wonder if we should talk about this in chat)
Eldritch Conundrum
CC BY-SA 4.0
2023-11-12T15:43:50.697Z
@EldritchConundrum No, I'm saying the opposite: that flow-based type inference doesn't replace null coalesce and chaining operators, so picking any one of them and calling it "the modern way" doesn't really make sense. It's an interesting feature, but as both question and answer mention, it's really an advance in static type checking that happens to be useful for nullable types.
IMSoP
CC BY-SA 4.0
2023-11-12T16:15:36.847Z
@IMSoP Null coalescing and chaining handle only specific cases. (Respectively: when you have a default value, and when you want to do nothing in the null case.) My question is about approaches to *general* null-checking, for *any* kind of behavior. This makes null coalescing and chaining not relevant here.
Eldritch Conundrum
CC BY-SA 4.0
2023-11-12T16:16:59.493Z
I called it the "modern" way because humanity had to wait until the 2010s to finally get both advantages ("The safety guarantees of #2, combined with the no-clutter ergonomics of #1") together, whereas the two other ways have existed since long ago in the 20th century.
Eldritch Conundrum
CC BY-SA 4.0
2023-11-12T16:28:21.967Z
@EldritchConundrum Flow-based type inference *also* only handles specific cases, that's my whole point. I'm not clear if you just don't agree, or still haven't understood what I'm trying to say.
IMSoP
CC BY-SA 4.0
2023-11-12T16:48:34.917Z
I do not see how it only handles specific cases.
Eldritch Conundrum
CC BY-SA 4.0
2023-11-12T17:39:21.387Z
As far as I can tell, your option (3) is an advance in compiler technology, not a new language feature.  Are you talking about something more than flow analysis there?  What do you suppose a compiler will do with the knowledge that `x` cannot be null that improves the detection of or reduces the impact of programmer error?
John Bollinger
CC BY-SA 4.0
2023-11-12T19:43:34.333Z
If you're providing a default value, the extra code to run is in the null case, not the non-null case, so inference doesn't make anything shorter, but a coalesce operator does. If you're propogating an error through several calls, type inference doesn't save you from having multiple nested or sequential if statements, but a shortcutting operator, monad, or stream map, does. I'm sure there are other scenarios, where other features improve the code.
IMSoP
CC BY-SA 4.0
2023-11-12T21:53:30.053Z
@JohnBollinger The language feature is type refinement within the scope, so part of the static typing. Variable `x` which earlier had type `string | null`, and thus couldn't have any properties of the string type accessed, has type `string` alone within the true scope of the if, so what the compiler will do is allow the programmer to access properties of the reference instead of rejecting it. This **is** a semantic language feature, not a compiler technology feature.
Michael Homer
CC BY-SA 4.0
2023-11-12T22:06:33.020Z
Ok, @MichaelHomer.  That seems a lot more specific to a certain kind of type system than the question prose suggested to me.
John Bollinger
CC BY-SA 4.0
2023-11-13T01:38:17.590Z
@EldritchConundrum I'm not fully convinced this is such a big difference from what's already available in a language like Haskell. Consider `letJust` in [this example](https://play.haskell.org/saved/7AvEYFdD). This seems to more or less capture what you're looking for (and you can use it inside any value with a type that's an `Applicative` and also therefore any `Monad`). Now, it's not built into the language, and the syntax could look nicer. But all it would take is a *very* small macro to make a *very* slight change to the syntax to be close to what you're talking about
David Young
CC BY-SA 4.0
2023-11-13T01:50:25.707Z
@EldritchConundrum In fact, a generalized version of that function already exists in the standard library under the name [`for_`](https://hackage.haskell.org/package/base-4.19.0.0/docs/Data-Foldable.html#v:for_). It's generalized because not only can the "effect" be any `Applicative`, but instead of only working with `Maybe` it works with any `Foldable` (like lists, for instance)! There's a joke in the Haskell community that "everything is `traverse`". Well, `for_` is just a version of `traverse` that ignores the result of the effectful computation and its arguments flipped =)
David Young
CC BY-SA 4.0
2023-11-13T01:55:55.253Z
Also, that generalization really shows that it's actually essentially the same thing as a `foreach` loop (this is what `for_` does when you use it with a list). But instead of iterating over a list, you are "iterating" over an optional
David Young
CC BY-SA 4.0
2023-11-13T12:58:42.803Z
@DavidYoung there are plenty of ways to avoid having to introduce a new name when doing this in Haskell, but the one you're suggesting with `x <- x` is not among the ones I'd consider, in fact it's rather horrible IMO. Certainly not something to use for something as simple as your example, which can simply be written `fmap (+1) x`.
leftaroundabout
CC BY-SA 4.0
2023-11-13T15:25:38.137Z
@leftaroundabout I agree that it’s not very nice. Which way would you suggest that fits all of the requirements in replacing the general `if (x != Nothing)` form in question here? I realize that there are more idiomatic alternative ways to do that it certain particular situations, but I just wanted a straightforward way to show why I don’t think that `if` form is a major change from what is already in the language. An assumption of the question, as I understand it, seems to be that such an `if` was a groundbreaking improvement over what languages like Haskell have.
David Young
CC BY-SA 4.0
2023-11-13T20:03:33.750Z
I did not limit the question to null pointers in OO/procedural languages, because flow-sensitive typing could be useful in functional languages too. Simultaneously, I recognize that in Haskell it would only represents a minor improvement, for multiple reasons. It is now clear to me that the characterization as "modern", seemingly in opposition to "functional", was too much for many sensibilities, and that my praises should have been more narrowly targeted.
Eldritch Conundrum
CC BY-SA 4.0
2023-11-24T12:39:13.863Z
This doesn't sound to me like a new design so much as a compiler optimization.
Karl Knechtel
CC BY-SA 4.0
2023-11-24T13:28:16.353Z
@KarlKnechtel See Michael Homer's comment above
Eldritch Conundrum
CC BY-SA 4.0
2023-12-03T18:18:14.440Z
Swift if let doesn’t require a new variable name.
gnasher729
<p>I don't think this design is as new as you're expecting, though practical languages designed from the beginning with this purpose in mind are more recent. For example, in 2002's <a href="https://web.eecs.umich.edu/%7Ebchandra/courses/papers/Fahndrich_NonNull.pdf" rel="noreferrer">Declaring and Checking Non-null Types in an Object-Oriented Language</a> by Manuel Fähndrich &amp; K. Rustan M. Leino, non-null annotations for languages in the Java and C# mold are proposed, and the implementation already uses flow-sensitive inference to handle local variables of reference types:</p>
<blockquote>
<p>Instead, our checker infers the nullity and rawness type information using a simple flow-sensitive method-local (intra-procedural) data-flow analysis. <strong>The analysis is smart enough to refine the annotations in branches of tests against null</strong>. Programmers can thus use ordinary tests against null to refine a type from <span class="math-container">$T^+$</span> to <span class="math-container">$T^-$</span>.</p>
</blockquote>
<p><span class="math-container">$T^+$</span> is their notation for a nullable type, and their system operates on top of C#. A number of linting tools for C(-like languages) did similar things before that. Static checkers for Java also did the same thing. It's arguable whether external checkers constitute language features, but from a certain point of view they do define a language.</p>
<hr />
<p>On the language level, I believe <strong><a href="https://en.wikipedia.org/wiki/Whiley_(programming_language)" rel="noreferrer">Whiley</a> in 2009-2010 first introduced this refinement syntax and semantics</strong> as a language element.</p>
<p>Whiley is directly built around flow-sensitive typing, and this specific refinement is explicitly identified in <a href="https://ecs.wgtn.ac.nz/foswiki/pub/Main/TechnicalReportSeries/ECSTR10-23.pdf" rel="noreferrer">its earliest technical report</a> in 2010:</p>
<blockquote>
<pre><code>int f(LL link):
    if link != null:¹
        link.dt = [1]²
        return 0³
</code></pre>
<p>The typing environments determined for this function are:</p>
<ul>
<li>Γ¹ = {link ↦ μX.({int dt, X nxt} ∨ null)}</li>
<li>Γ² = {link ↦ {int dt, μX.({int dt, X nxt} ∨ null) nxt}}</li>
<li>Γ³ = {link ↦ {[int] dt, μX.({int dt, X nxt} ∨ null) nxt}</li>
</ul>
<p>Here, the null test removes the possibility of link being null in the true branch. Then, the assignment
updates the type of field dt from int to [int].</p>
</blockquote>
<p>The superscripts in the code are part of the typesetting, not the language, to identify the corresponding environments below.</p>
<p>Other examples also appear with tests in both directions:</p>
<blockquote>
<pre><code>int sum(LinkedList l):
    if l is null:
        return 0
    else:
        return l.data + sum(l.next)
</code></pre>
</blockquote>
<p>and</p>
<blockquote>
<pre><code>[string] split(string str, char c):
    idx = indexOf(str,c)
    // idx has type null|int
    if idx is int:
        // idx now has type int
        below = str[0..idx]
        above = str[idx..]
        return [below,above]
    else:
        // idx now has type null
        return [str] // no occurrence
</code></pre>
</blockquote>
<p>This is the first instance I know of of a practical language designed for this sort of construction with <code>null</code>, and introduced some of the vocabulary around it. Whiley uses flow-sensitive typing heavily for all types, not only for nullability, so this is just an (important) special case of the general case, rather than the driving force. Much of the formal work on this sort of concrete flow-sensitive typing is from Pearce.</p>
<hr />
<p>On the more-functional side of things, &quot;occurrence typing&quot; was introduced by Tobin-Hochstadt &amp; Felleisen for <a href="https://doi.org/10.1145/1328438.1328486" rel="noreferrer">Typed Scheme</a> in 2008. It refines variable types based on predicate tests, and these predicates could include checking for <code>nil</code>, though Lisp <code>nil</code> is not quite the same thing as an object-oriented null pointer. You might or might not want to count this. Flow-sensitive and occurrence typing are broadly the same thing discovered independently. The follow-on Typed Racket also <a href="https://docs.racket-lang.org/ts-guide/occurrence-typing.html" rel="noreferrer">includes general occurrence typing</a> based on predicates. Test predicates can sometimes be quite complex, beyond superficial type tests, and can cause some non-local propagation as well. This may be beyond the scope of what you're thinking of and of course the syntactic construction is quite different.</p>
<p>Ceylon (2011) is an object-oriented system with a design hewing closer to Java, but with flow-sensitive typing and a separate branch of the type hierarchy for nulls. It used more specialised dedicated test operators. Kotlin draws from the same well.</p>
<hr />
<p>I would say that the contrasts and trade-offs made in all of these options are not as stark as the question makes out. In particular, explicit (tagged) option types can be <em>useful</em> beyond merely requiring more boilerplate, allowing for option-chaining, monoidal or monadic operations, and static transformations. It's useful to have generalised mapping, collapsing or railway-style failure handling, and distinguished labels for data, and the design question is more about whether that's <em>more</em> useful than the <em>other</em> things you enable without them.</p>
<p>In fact, tagged option types aren't even incompatible with flow-sensitive type refinement if you want to design the language that way! These are ergonomic and semantic tradeoffs, and none of them are so miraculous.</p>

CC BY-SA 4.0
2023-11-11T23:34:30.180Z
2023-11-12T00:05:30.793Z
2023-11-12T00:05:30.793Z
Michael Homer
CC BY-SA 4.0
2023-11-11T23:49:16.897Z
I think this point is a really important challenge to the way the question is framed: "tagged option types aren't even incompatible with flow-sensitive type refinement". In other words, this isn't a third way between null pointers and ADTs, it's a convenience feature which can be added to either of them. Indeed, the question accidentally confirms this, mentioning Swift, where the convenience feature is on top of an Option type.
IMSoP
CC BY-SA 4.0
2023-11-12T01:17:32.160Z
@Michael Homer I wouldn't count linters, direct language support is vastly superior. Whiley and Ceylon definitely count. Occurrence typing may count if it was applied to nullability in practice? My question doesn't ask about the origins of flow typing itself, but about applying flow typing to (null/none/nothing)-checking. And of course it is compatible with tagged option types, that are useful on their own. I'm curious about the tradeoffs you mention. Are there any downsides to flow typing for null/none/nothing?
Eldritch Conundrum
CC BY-SA 4.0
2023-11-12T01:41:41.500Z
@EldritchConundrum The distinction between a checker/linter (Fähndrich & Leino) and a static type system applied to an untyped language (Typed Scheme) is pretty narrow, so it's conceivable the line got crossed somewhere. While nil-checking is an obvious application, I'm not sure there's any documented *claim* about it for Typed Scheme preceding Whiley; typical patterns of programming in Lisp probably don't make it very interesting. Whiley is likely the source for what you're looking for.
Michael Homer
# What language was the first to treat null checks as smart casts to non-nullable types?
Posted by: username_0 on 2023-11-11
As far as I know, for many decades, in mainstream programming languages, there were only two options to handle null-like optionality:

1. Pointer or reference types are always nullable (the famous "billion-dollar mistake"). The programmer needs to remember to check for null wherever needed, or else the program does bad things at runtime. The compiler doesn't detect mistakes, though linters can often help.
2. There are separate "optional" or "maybe" wrapper types, so the programmer can't accidentally use a nullable value where a non-null value is required. This solves the problem of #1, but it means that the programmer has to introduce a new variable, with a different name, for the unwrapped value, even though it represents the same thing. (There can also be a runtime cost, if this is not compiled down to a pointer.)

In the 2010s (I think?), a new way appeared, which I love.

3. Pointer or reference types are *usually* nullable, but the compiler requires a null-check where needed; it can do this because it's smart enough to detect that `x` is not null inside `if (x != null) { ... }`. This gives the safety guarantees of #2, without the downsides that I mentioned above. No downsides (that I know of).

Kotlin calls that a "smart cast" (it works with downcasts in addition to null-checking). Swift has something similar too, requiring only adding a `let` keyword.

This miraculous third way, which we will hopefully enjoy in every future language... This application of flow-sensitive typing to improve the ergonomics of safe null-checking... Which language did it come from?
**Tags:** history type-inference nullability
> **Comments:**
> **username_1**: A Maybe/Option type goes a long way beyond just forcing you to write checking code; it gives you additional facilities for working with and propogating the "null" case, in the form of Monads or Streams. It also often goes alongside lots of shorthand syntax for doing so which is at least as easy to read as your "modern way", which doesn't seem particularly "miraculous" to me.  
> **username_2**: [Related](https://langdev.stackexchange.com/q/360/45) (cc: @IMSoP)  
> **username_0**: @IMSoP You seem to have understood my question as a criticism of tagged option types? It is not that, since #2 and #3 are compatible. But it is a praise of what you called a "convenience" improvement. Maybe it is not literally miraculous :) but I don't want to program in an inconvenient language when convenient ones exist.  
> **username_3**: @EldritchConundrum Convenience is very much subjective. I find `if x != null` to be horribly ugly and not terribly convenient. I think IMSoP's point is that such a design does not allow for a different set of conveniences that Option/Result types provide. But also note that `if x != null` in the way you describe is identical to `if let Some(x) == x` in ex. Rust: and from other questions, it sounds like Swift's implementation, at least, may be syntactic sugar for it.  
> **username_0**: "such a design does not allow for a different set of conveniences that Option/Result types provide" Why not? They are compatible. As to the more verbose variants that require adding an explicit `let`, they're good too, as long as a second name doesn't need to be introduced.  
> **username_4**: @EldritchConundrum You can reuse the same name in Haskell: `do { x <- x; Just (x + 1) }` (Note that, inside `do` notation, this is not introducing a recursive binding). This shadows the original `x`  
> **username_4**: For completeness, [here](https://play.haskell.org/saved/jqzjoLSJ) is a full, runnable example of what I mean using an browser-based Haskell compiler.  
> **username_0**: @DavidYoung Interesting! `x <- x` isn't the most readable null check for everyone, but it seems to accomplish something similar to flow checking, albeit with the additional constraints of being only able to return None when x is None, and generally having to be in a Maybe-returning do.  
> **username_4**: @EldritchConundrum You can effectively do a bit more with some other things, like `sequenceA`. That function will "commute" certain pairs of functors. For example, `sequenceA` will turn a `Maybe (IO ())` value into a `IO (Maybe ())` value (specifically, the outermost functor of the input has to be `Traversable` and the innermost functor has to be `Applicative`). [Here is an example of that](https://play.haskell.org/saved/AQ6rfAM5). You can also straightfowardly combine `theBody` and `example` into one function. I just separated them for clarity.  
> **username_4**: (Also, note that, similar to the other example, the `x` in `pure (print x)` is an `Int`, not a `Maybe Int`).  
> **username_0**: @DavidYoung Of course you can always add more code and accomplish anything, but that's getting further away from the minimality of having `if x is not null, print(x)` safely do what you mean.  
> **username_1**: The way you've presented it suggests that this feature is a completely new approach to the problem, whereas I am suggesting that it's just one feature among many that can make working with nullable or Option types more convenient. There's a whole range of scenarios and programming styles where it wouldn't make any difference, and if writing an if statement around a block was the *only* way the language offered to handle nulls, it would be significantly *less* convenient than other languages.  
> **username_5**: I think that a latent issue underlying several comments above is that you characterize "the functional way" as obsolete, which is naturally going to annoy people and prompt them to argue with you about that. I think you can avoid such responses by trimming your question to focus only on the pattern you're actually asking about; or if you find it too hard to describe it without describing the alternatives to it, then you can at least try to avoid editorializing.  
> **username_0**: I see... Maybe the heart of the issue is that it is an improvement much more useful in non-functional languages (where `if` is the most idiomatic way to check null) than in functional languages (which have more varied ways). My question doesn't highlight the difference, maybe it should. I could also restrict the question to non-functional languages, just for clarity? However, I think that flow typing is also an improvement in functional languages. I'd like to know if it's not!  
> **username_1**: I agree with ruakh's comment, but want to stress that it doesn't fully address mine, which is that *this isn't a third way of handling nulls*. You can have a procedural or OO language that strictly checks for nulls at compile time, but doesn't use this, offering instead operators like null coalesce (var ?? default) and null chaining (var?->member)  
> **username_0**: @IMSoP You seem to claim that the presence of null coalesce and null chaining operators in an OO/procedural language replace entirely the need for general case direct null-checking. My years of experience in such languages tell me that's not true! Even after using these operators everywhere you can, you are still left with direct null checks, and it is a relief when you can have flow typing for these and avoid new identifier proliferation. (I'm starting to wonder if we should talk about this in chat)  
> **username_1**: @EldritchConundrum No, I'm saying the opposite: that flow-based type inference doesn't replace null coalesce and chaining operators, so picking any one of them and calling it "the modern way" doesn't really make sense. It's an interesting feature, but as both question and answer mention, it's really an advance in static type checking that happens to be useful for nullable types.  
> **username_0**: @IMSoP Null coalescing and chaining handle only specific cases. (Respectively: when you have a default value, and when you want to do nothing in the null case.) My question is about approaches to *general* null-checking, for *any* kind of behavior. This makes null coalescing and chaining not relevant here.  
> **username_0**: I called it the "modern" way because humanity had to wait until the 2010s to finally get both advantages ("The safety guarantees of #2, combined with the no-clutter ergonomics of #1") together, whereas the two other ways have existed since long ago in the 20th century.  
> **username_1**: @EldritchConundrum Flow-based type inference *also* only handles specific cases, that's my whole point. I'm not clear if you just don't agree, or still haven't understood what I'm trying to say.  
> **username_0**: I do not see how it only handles specific cases.  
> **username_6**: As far as I can tell, your option (3) is an advance in compiler technology, not a new language feature.  Are you talking about something more than flow analysis there?  What do you suppose a compiler will do with the knowledge that `x` cannot be null that improves the detection of or reduces the impact of programmer error?  
> **username_1**: If you're providing a default value, the extra code to run is in the null case, not the non-null case, so inference doesn't make anything shorter, but a coalesce operator does. If you're propogating an error through several calls, type inference doesn't save you from having multiple nested or sequential if statements, but a shortcutting operator, monad, or stream map, does. I'm sure there are other scenarios, where other features improve the code.  
> **username_7**: @JohnBollinger The language feature is type refinement within the scope, so part of the static typing. Variable `x` which earlier had type `string | null`, and thus couldn't have any properties of the string type accessed, has type `string` alone within the true scope of the if, so what the compiler will do is allow the programmer to access properties of the reference instead of rejecting it. This **is** a semantic language feature, not a compiler technology feature.  
> **username_6**: Ok, @MichaelHomer.  That seems a lot more specific to a certain kind of type system than the question prose suggested to me.  
> **username_4**: @EldritchConundrum I'm not fully convinced this is such a big difference from what's already available in a language like Haskell. Consider `letJust` in [this example](https://play.haskell.org/saved/7AvEYFdD). This seems to more or less capture what you're looking for (and you can use it inside any value with a type that's an `Applicative` and also therefore any `Monad`). Now, it's not built into the language, and the syntax could look nicer. But all it would take is a *very* small macro to make a *very* slight change to the syntax to be close to what you're talking about  
> **username_4**: @EldritchConundrum In fact, a generalized version of that function already exists in the standard library under the name [`for_`](https://hackage.haskell.org/package/base-4.19.0.0/docs/Data-Foldable.html#v:for_). It's generalized because not only can the "effect" be any `Applicative`, but instead of only working with `Maybe` it works with any `Foldable` (like lists, for instance)! There's a joke in the Haskell community that "everything is `traverse`". Well, `for_` is just a version of `traverse` that ignores the result of the effectful computation and its arguments flipped =)  
> **username_4**: Also, that generalization really shows that it's actually essentially the same thing as a `foreach` loop (this is what `for_` does when you use it with a list). But instead of iterating over a list, you are "iterating" over an optional  
> **username_8**: @DavidYoung there are plenty of ways to avoid having to introduce a new name when doing this in Haskell, but the one you're suggesting with `x <- x` is not among the ones I'd consider, in fact it's rather horrible IMO. Certainly not something to use for something as simple as your example, which can simply be written `fmap (+1) x`.  
> **username_4**: @leftaroundabout I agree that it’s not very nice. Which way would you suggest that fits all of the requirements in replacing the general `if (x != Nothing)` form in question here? I realize that there are more idiomatic alternative ways to do that it certain particular situations, but I just wanted a straightforward way to show why I don’t think that `if` form is a major change from what is already in the language. An assumption of the question, as I understand it, seems to be that such an `if` was a groundbreaking improvement over what languages like Haskell have.  
> **username_0**: I did not limit the question to null pointers in OO/procedural languages, because flow-sensitive typing could be useful in functional languages too. Simultaneously, I recognize that in Haskell it would only represents a minor improvement, for multiple reasons. It is now clear to me that the characterization as "modern", seemingly in opposition to "functional", was too much for many sensibilities, and that my praises should have been more narrowly targeted.  
> **username_9**: This doesn't sound to me like a new design so much as a compiler optimization.  
> **username_0**: @KarlKnechtel See Michael Homer's comment above  
> **username_10**: Swift if let doesn’t require a new variable name.  
---
## 1 answers
### Answer by username_7 on 2023-11-11. Score: 22 | Accepted answer
I don't think this design is as new as you're expecting, though practical languages designed from the beginning with this purpose in mind are more recent. For example, in 2002's Declaring and Checking Non-null Types in an Object-Oriented Language by Manuel Fähndrich & K. Rustan M. Leino, non-null annotations for languages in the Java and C# mold are proposed, and the implementation already uses flow-sensitive inference to handle local variables of reference types:

Instead, our checker infers the nullity and rawness type information using a simple flow-sensitive method-local (intra-procedural) data-flow analysis. The analysis is smart enough to refine the annotations in branches of tests against null. Programmers can thus use ordinary tests against null to refine a type from $T^+$ to $T^-$.

$T^+$ is their notation for a nullable type, and their system operates on top of C#. A number of linting tools for C(-like languages) did similar things before that. Static checkers for Java also did the same thing. It's arguable whether external checkers constitute language features, but from a certain point of view they do define a language.

On the language level, I believe Whiley in 2009-2010 first introduced this refinement syntax and semantics as a language element.
Whiley is directly built around flow-sensitive typing, and this specific refinement is explicitly identified in its earliest technical report in 2010:

int f(LL link):
    if link != null:¹
        link.dt = [1]²
        return 0³

The typing environments determined for this function are:

Γ¹ = {link ↦ μX.({int dt, X nxt} ∨ null)}
Γ² = {link ↦ {int dt, μX.({int dt, X nxt} ∨ null) nxt}}
Γ³ = {link ↦ {[int] dt, μX.({int dt, X nxt} ∨ null) nxt}

Here, the null test removes the possibility of link being null in the true branch. Then, the assignment
updates the type of field dt from int to [int].

The superscripts in the code are part of the typesetting, not the language, to identify the corresponding environments below.
Other examples also appear with tests in both directions:

int sum(LinkedList l):
    if l is null:
        return 0
    else:
        return l.data + sum(l.next)


and

[string] split(string str, char c):
    idx = indexOf(str,c)
    // idx has type null|int
    if idx is int:
        // idx now has type int
        below = str[0..idx]
        above = str[idx..]
        return [below,above]
    else:
        // idx now has type null
        return [str] // no occurrence


This is the first instance I know of of a practical language designed for this sort of construction with null, and introduced some of the vocabulary around it. Whiley uses flow-sensitive typing heavily for all types, not only for nullability, so this is just an (important) special case of the general case, rather than the driving force. Much of the formal work on this sort of concrete flow-sensitive typing is from Pearce.

On the more-functional side of things, "occurrence typing" was introduced by Tobin-Hochstadt & Felleisen for Typed Scheme in 2008. It refines variable types based on predicate tests, and these predicates could include checking for nil, though Lisp nil is not quite the same thing as an object-oriented null pointer. You might or might not want to count this. Flow-sensitive and occurrence typing are broadly the same thing discovered independently. The follow-on Typed Racket also includes general occurrence typing based on predicates. Test predicates can sometimes be quite complex, beyond superficial type tests, and can cause some non-local propagation as well. This may be beyond the scope of what you're thinking of and of course the syntactic construction is quite different.
Ceylon (2011) is an object-oriented system with a design hewing closer to Java, but with flow-sensitive typing and a separate branch of the type hierarchy for nulls. It used more specialised dedicated test operators. Kotlin draws from the same well.

I would say that the contrasts and trade-offs made in all of these options are not as stark as the question makes out. In particular, explicit (tagged) option types can be useful beyond merely requiring more boilerplate, allowing for option-chaining, monoidal or monadic operations, and static transformations. It's useful to have generalised mapping, collapsing or railway-style failure handling, and distinguished labels for data, and the design question is more about whether that's more useful than the other things you enable without them.
In fact, tagged option types aren't even incompatible with flow-sensitive type refinement if you want to design the language that way! These are ergonomic and semantic tradeoffs, and none of them are so miraculous.
> **Comments:**
> **username_1** (2023-11-11): I think this point is a really important challenge to the way the question is framed: "tagged option types aren't even incompatible with flow-sensitive type refinement". In other words, this isn't a third way between null pointers and ADTs, it's a convenience feature which can be added to either of them. Indeed, the question accidentally confirms this, mentioning Swift, where the convenience feature is on top of an Option type.  
> **username_0** (2023-11-12): @Michael Homer I wouldn't count linters, direct language support is vastly superior. Whiley and Ceylon definitely count. Occurrence typing may count if it was applied to nullability in practice? My question doesn't ask about the origins of flow typing itself, but about applying flow typing to (null/none/nothing)-checking. And of course it is compatible with tagged option types, that are useful on their own. I'm curious about the tradeoffs you mention. Are there any downsides to flow typing for null/none/nothing?  
> **username_7** (2023-11-12): @EldritchConundrum The distinction between a checker/linter (Fähndrich & Leino) and a static type system applied to an untyped language (Typed Scheme) is pretty narrow, so it's conceivable the line got crossed somewhere. While nil-checking is an obvious application, I'm not sure there's any documented *claim* about it for Typed Scheme preceding Whiley; typical patterns of programming in Lisp probably don't make it very interesting. Whiley is likely the source for what you're looking for.  
---
