14
$\begingroup$

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.

  1. 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?

$\endgroup$
34
  • 4
    $\begingroup$ 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. $\endgroup$
    – IMSoP
    Nov 11, 2023 at 23:05
  • 5
    $\begingroup$ 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. $\endgroup$
    – ruakh
    Nov 12, 2023 at 8:02
  • 2
    $\begingroup$ 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! $\endgroup$ Nov 12, 2023 at 9:21
  • 2
    $\begingroup$ 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? $\endgroup$ Nov 12, 2023 at 17:39
  • 2
    $\begingroup$ @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. $\endgroup$
    – Michael Homer
    Nov 12, 2023 at 21:53

1 Answer 1

20
$\begingroup$

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.

$\endgroup$
3
  • 3
    $\begingroup$ 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. $\endgroup$
    – IMSoP
    Nov 11, 2023 at 23:49
  • $\begingroup$ @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? $\endgroup$ Nov 12, 2023 at 1:17
  • 3
    $\begingroup$ @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. $\endgroup$
    – Michael Homer
    Nov 12, 2023 at 1:41

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .