The Etymology of Lifting

Contents hide

This article was originally published in my blog (affectionately referred to as blargh) on . The original blog no longer exists as I've migrated everything to this wiki.

The original URL of this post was at Hopefully that link redirects back to this page.

"Lifting" is an esoteric term that is used by a few languages (C♯, most notably) to describe a feature usually associated with nullable types. It's used colloquially to signify that a member (or operator) is "lifted" from another object automatically by the compiler.

What this actually means is best illustrated with an example. C♯'s reference types are nullable by default. This means you can do things like object foo = null; and not get a compiler error. It also means you can do things like foo.ToString() and get an ever familiar NullReferenceException.

This is because reference types in C♯ are nullable by default. But not all types are this way. Value types like int are never null, and have a default value that is retrievable with the default operator: var zero = default(int);

The expected behavior becomes less clear when you use nullable value types like int?. By using nullable types, you can assign a null value to a value type without a compiler error: int? nullableInt = null; For example, what happens in the following code? Is it a compiler error, a runtime error, or is it valid code that will run without exception?

int? nullableInt = null;
int nonNullableInt = 2;
int result = nullableInt + nonNullableInt; // what happens?
int? result = nullableInt + nonNullableInt; // what about here?

The answer I'll leave as an exercise to the reader, as it's mostly irrelevant to what I want to talk about. That is, the subject of this post is not the peculiarities of the C♯ language specification and the validity (or lack thereof) of nullable reference types. Both subjects have been hotly debated by people far more qualified than I. Rather, the subject of this post is what "lifting" means in the context of a programming language. I gave the example above to illustrate potential ambiguities when performing operations on nullable types. The actual value of result is insignificant, but the ways in which the compiler determines how to perform addition between a potentially null value and a non-null value are a good lead-in to lifting.

Let's get mathematical

Lifting comes from the prestigious and panty-dropping field of topology, which has to do with "structured space", which is basically a catch-all term in mathematics. You can hunt down the exact definition later.

In algebraic topology, there's a thing called a homotopy. Two functions in two different topological spaces are homotopic if one can be transformed into the other. What that actually means is not really relevant, but homotopic functions (and in particular homotopies in more than two dimensions) played a role in proving the Poincaré Conjecture. So they've served a purpose at some point.

So where does lifting come in? Well, if you have a homotopy on a space X to another space B and a mapping function δ from another topological space E to B, then δ has the homotopic lifting property on X if it satisifies some other conditions.

Obviously, that makes no sense, and nor should it, unless you happen to be a grad student studying algebraic topology. The exact meaning isn't important, but a general inkling of what it represents will aid in understanding why programming languages borrowed the term lifting.

So. The δ function above is a map bridging two different spaces. Instead of spaces, we'll call them sets (since that's actually what they are). Say E is the set of integers { 1, 2, 3, 4 }, and B is the set of integers { 2, 4, 6, 8 }. In this trivial case, δ could be f(x)=2xf(x) = 2x. It should be pretty obvious to see that δ will map each element in E to an element in B.

Now, to say that δ has the lifting property is where it starts to get interesting. Well, more interesting. Whatever.

Anyway, to say a function has the lifting property requires a bit of verification. Specifically, it requires several conditions to be true, all of which I'm not going to discuss. You can read about them on wikipedia if you want. The important thing is that if δ has the lifting property on a space X (which, remember, contains a homotopy from X to B), then there exists another function g that maps X to E.

So, continuing with our trivial example, say X is { 5, 6, 7, 8 }. Then we could have g(x)=x4g(x) = x - 4. This would map all of the elements in X to an element in E (which was { 1, 2, 3, 4 }, as was defined above).

Now, bear in mind that this is all completely contrived and dumbed down for the sake of illustrating the concept of lifting in programming languages. This is not a valid mathematical notion. This ain't Wolfram|Alpha. For example, X must be defined on the continuous closed interval [0,1][0, 1], and there must also exist a map from X×0X \times {0} to E. But we won't get into that.

So what is happening is that the homotopy from X to B is "lifted" to E by g. What this (approximately) means in layman's terms is that the homotopy from X to B can also take place from X to E. And what THAT means is a function that can transformed from X to B (the definition of homotopy) can also be transfromed from X to E.

Lifting in C♯

So how does all of this relate to C♯ and nullable types? Well, to be able to conveniently perform addition, C♯ "lifts" the + operator on int to int?. If you think of the set of operators on integers a topological space, and the set of operators on nullable integers another topological space, the magic that happens that allows addition between nullable integers would be the δ mapping function that lifts addition to the nullable integers.

I think that might be the worst of analogy of all time. I don't think taking something simple and rewording it be more complex is an actual literary technique. It's possible that I just invented it. But I digress.

Using the term "lifting" is a bit of a misnomer, as it has concrete meaning in other fields (namely algebraic topology). "Lifting" in C♯ is a bastardized form of "lifting" that ignores many of the essential properties of homotopy theory (like the fact that it only applies to continuous functions). But honestly, it doesn't really matter. The visualization of literally (well, figuratively) "lifting" an operator from one object and applying it to another object is pretty apt. But sometimes it's good to understand WHY these things are done this way.