## The Etymology of Lifting_{[source]}

xml

`<glacius:metadata>` | |

` <title>The Etymology of Lifting</title>` | |

` <description>What "lifting" means in the context of computer programming</description>` | |

` <category>Legacy blog posts</category>` | |

` <category>Programming</category>` | |

` <category>Math</category>` | |

`</glacius:metadata>` | |

`<glacius:macro name="legacy blargh banner">` | |

` <properties>` | |

` <originalUrl>https://tmont.com/blargh/2011/11/the-eymology-of-lifting</originalUrl>` | |

` <originalDate>2011-11-02T08:47:50.000Z</originalDate>` | |

` </properties>` | |

`</glacius:macro>` | |

`<p>` | |

` "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. | |

`</p>` | |

`<p>` | |

` 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 <code>object foo = null;</code> and not` | |

` get a compiler error. It also means you can do things like <code>foo.ToString()</code>` | |

` and get an ever familiar <code>NullReferenceException</code>.` | |

`</p>` | |

`<p>` | |

` This is because reference types in C♯ are nullable by default. But not all types are this way. Value types` | |

` like <code class="sunlight-highlight-csharp">int</code> are never null, and have a default value that is retrievable` | |

` with the <tt>default</tt> operator: <code class="sunlight-highlight-csharp">var zero = default(int);</code>` | |

`</p>` | |

`<p>` | |

The expected behavior becomes less clear when you use nullable value types like | |

` <code>int?</code>. By using nullable types, you can assign a null value to` | |

` a value type without a compiler error: <code>int? nullableInt = null;</code>` | |

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

`</p>` | |

`<glacius:code lang="csharp"><![CDATA[int? nullableInt = null;` | |

int nonNullableInt = 2; | |

int result = nullableInt + nonNullableInt; // what happens? | |

`int? result = nullableInt + nonNullableInt; // what about here?]]></glacius:code>` | |

`<p>` | |

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 <code>result</code> 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. | |

`</p>` | |

`<h2>Let's get mathematical</h2>` | |

`<p> ` | |

Lifting comes from the prestigious and panty-dropping field of | |

` <a href="https://en.wikipedia.org/wiki/Algebraic_topology"><strong>topology</strong></a>, which has to do ` | |

with "structured space", which is basically a catch-all term in mathematics. You can hunt down the exact | |

definition later. | |

`</p>` | |

`<p> ` | |

In algebraic topology, there's a thing called a | |

` <a href="https://en.wikipedia.org/wiki/Homotopy_theory"><strong>homotopy</strong></a>. 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 <a href="https://en.wikipedia.org/wiki/Poincar%C3%A9_conjecture">Poincaré` | |

` Conjecture</a>. So they've served a purpose at some point.` | |

`</p>` | |

`<p> ` | |

` So where does lifting come in? Well, if you have a homotopy on a space <strong>X</strong> to another space` | |

` <strong>B</strong> and a mapping ` | |

` function <strong>δ</strong> from another topological space <strong>E</strong> to <strong>B</strong>,` | |

` then <strong>δ</strong> has the <em>homotopic lifting property</em> on <strong>X</strong> if it` | |

satisifies some other conditions. | |

`</p>` | |

`<p>` | |

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 <em>lifting</em>.` | |

`</p>` | |

`<p>` | |

` So. The <strong>δ</strong> function above is a map bridging two different spaces. Instead of` | |

spaces, we'll call them sets (since that's actually what | |

` <a href="https://en.wikipedia.org/wiki/Topological_space#Definitions">they are</a>). Say <strong>E</strong>` | |

` is the set of integers <code>{ 1, 2, 3, 4 }</code>, and <strong>B</strong> is the set of integers` | |

` <code>{ 2, 4, 6, 8 }</code>. In this trivial case, <strong>δ</strong> could be <glacius:latex>f(x) = 2x</glacius:latex>.` | |

` It should be pretty obvious to see that <strong>δ</strong> will map each element in <strong>E</strong>` | |

` to an element in <strong>B</strong>.` | |

`</p>` | |

`<p>` | |

` Now, to say that <strong>δ</strong> has the <em>lifting property</em> is where it starts to get` | |

interesting. Well, more interesting. Whatever. | |

`</p>` | |

`<p>` | |

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 <strong>δ</strong> has the <em>lifting property</em> on a` | |

` space <strong>X</strong> (which, remember, contains a homotopy from <strong>X</strong> to <strong>B</strong>), then` | |

` there exists another function <strong>g</strong> that maps <strong>X</strong> to <strong>E</strong>.` | |

`</p>` | |

`<p>` | |

` So, continuing with our trivial example, say <strong>X</strong> is <code>{ 5, 6, 7, 8 }</code>. Then` | |

` we could have <glacius:latex>g(x) = x - 4</glacius:latex>. ` | |

` This would map all of the elements in <strong>X</strong> to an element in <strong>E</strong>` | |

` (which was <code>{ 1, 2, 3, 4 }</code>, as was defined above).` | |

`</p>` | |

`<p>` | |

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 <strong>not</strong> a valid mathematical` | |

` notion. This ain't Wolfram|Alpha. For example, <strong>X</strong> must be defined on the continuous` | |

` closed interval <glacius:latex>[0, 1]</glacius:latex>, and there must also exist a map from ` | |

` <glacius:latex>X \times {0}</glacius:latex> to <strong>E</strong>.` | |

But we won't get into that. | |

`</p>` | |

`<p>` | |

` So what is happening is that the homotopy from <strong>X</strong> to <strong>B</strong> is "lifted" to ` | |

` <strong>E</strong> by <strong>g</strong>. What this (approximately) means in layman's terms is that` | |

` the homotopy from <strong>X</strong> to <strong>B</strong> can also take place from <strong>X</strong>` | |

` to <strong>E</strong>. And what THAT means is a function that can transformed from <strong>X</strong>` | |

` to <strong>B</strong> (the definition of homotopy) can also be transfromed from <strong>X</strong>` | |

` to <strong>E</strong>.` | |

`</p>` | |

`<h2>Lifting in C♯</h2>` | |

`<p>` | |

` So how does all of this relate to C♯ and nullable types? Well, to be able to conveniently perform` | |

` addition, C♯ "lifts" the <code>+</code> operator on <code>int</code>` | |

` to <code>int?</code>. 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 <strong>δ</strong> mapping` | |

function that lifts addition to the nullable integers. | |

`</p>` | |

`<p>` | |

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

`</p>` | |

`<p>` | |

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

`</p>` | |