Using optional callbacks in Rust

Thanks for the links. Looks like it's going to be interesting reading.

Starts to look like my problem here is that I don't have a CS degree. I know nothing of type theory, Curry-Howard correspondence etc. Or should I go back and get a maths degree?

For me it comes down to the point that Rust is likely not so impossible to understand. After all it's obvious that some functions never return. But the way Rust is described and often talked about here uses language that is totally alien coming as it does from the world of type theory and function programming. Which I'm guessing most working programmers have little exposure to.

So it seems. See my post above.

Problem is I have spent decades writing software, in all kind of languages, not studying type theory. I have worked in many companies, in different industries and countries, using a variety of languages. Never had I heard many of these terms used or discussed. Until I arrived here a couple of years ago.

I'm doing my best to catch up...

Still not clear to me. If a function never returns it feels like it has no return type, not that it does actually return a type that is always empty.

Perhaps I'm having the same problem with this as the generations back in the day who did not get the idea of zero as an actual numerical value rather than just as a symbol filling in the positional notation.

In the same way one might ask: why would I need a symbol for no number of things? One could ask: Why would I need a type for the absence of a type?

If you see what I mean...

No, I don’t think there’s any strict prerequisites at all. If you want more background on the terminology being used, external references that explain more are great; but otherwise, learning that “bottom type” means “empty type” and “diverges” means “never returns” is totally fine. I like the approach of not re-inventing new terminology for existing things. For example, I’ve learned functional programming (in particular Haskell) while in school with no formal background in mathematics or computer science, and it teaches you terms like Functor and Monad, or Monoid (or Semigroup, too, nowadays). These are all used practically for solving real programming problems, yet they keep their original names from their mathematical origin. This way, if you’re later in life coming across some bit of formal maths using these terms, you’re already having some intuition about them.


I’ve never seen an in-depth introduction of type theory in particular either. I do know some mathematical logic and also had a lecture including denotational semantics (that’s that thing that this section in the “Divergence” article is referring to).

I’ve had some interaction with theorem provers (e.g. Coq), hence some intuition about Curry-Howard correspondence.

Fun fact: The Curry-Howard correspondence connects the “bottom type” with the “⊥” meaning “false” in logic (e.g. one type in Coq that’s basically an empty enum that’s literally called “False” for that reason), and denotational semantics does connect the bottom type (somewhat) with the “bottom element” in order theory. (More precisely, it does connect the “bottom element” with diverging functions / expressions.) So all the “Mathematics” entries for “Bottom (disambiguation)”

Mathematics

  • Bottom, or falsum , a contradiction in logic and Boolean algebra
  • Bottom element, in lattice theory and related branches of mathematics
  • Bottom type, or empty type, in type theory
  • The symbol up tack (⊥), used to represent these concepts

are in a way connected.

2 Likes

If a function never returns, it has no return value, which means that the set of values it can possibly return is empty. A type is just a set of values about which you can prove interesting properties. So saying that the return type of f is ! is just saying that you can prove that f has the interesting property of never returning any value at all.

When seen this way ! is really no different than i32 or any other type, which is why it's treated in Rust as just another type rather than as a special annotation on a function (as in C11's noreturn).

3 Likes

I agree.

My problem is that in my world, having started programming in the late 1970's with ALGOL, and moving on through C, Pascal, C++, Ada, Coral, etc those things have never existed! No one around me did any Functional Programming and certainly did not use any of the FP languages. I wonder where did all this come from recently, or where has it been hiding?

So my idea of functions and types and all is what you get in the languages I mentioned above. Sweet and simple.

Having read around Functor, Monad , Monoid and the like I start to have a glimmer of understanding. Still have no clue what any of that has got to do with any programming problem I might have or how they might help.

It’s insanely useful for type-checking expressions, too. I’ve used the words “diverging functions / expressions” above, and a diverging expression also has the type !. You might want to read this post of mine:

1 Like

A function type is composed of argument type(s) and return type(s). You can't have "no return type" by definition. You can have an uninhabited type, which means that there's no value the function can ever return, because a value of its return type cannot be constructed, i.e. it will never return.

Why would I need a type for the absence of a type?

It's not the absence of a type, it's the absence of a value. And we need it because some functions do work like that. They panic, or they loop forever, for instance. And similarly, continue and break and return are control flow instructions that, when used as a value or expression, have the never type, which is how things like let x = if cond { value } else { return; } can at all compile. It would be hugely detrimental to the usability of the language if these expressions didn't consistently fit into the type system.

5 Likes

I get the idea. And it sounds perfectly reasonable of course.

But, looked at from the point of view of my former ignorance (prior to reading this thread) I think I can rationally claim that a function that never returns cannot possibly have a return type. There is no set of values it can possibly return because it never returns. That is to say, there isn't even set of values it returns, why even think about if that non-existent set is empty or not? That's crazy! :slight_smile:

Again, I get the idea and it's seems perfectly reasonable.

Except... In Rust I can have a function with no return type:

Contrast:

A function with a return type. Apparently an empty set, or bottom type or whatever:

fn f() -> ! {
    loop {
        //...
    }
}

A function with no return type. No empty set or bottom type to be seen:

fn f() {
    loop {
        //...
    }
}

Even C won't allow such a thing. Colour me confused at this point.

Empty sets are not crazy. Sorry, if you think they are, then you really need to brush up your basic maths, and I'm not going to try to convince you any more, because it's futile.

The syntactically "missing" return type means an implicit unit or () return type. It's a convenience feature of the language. Surface syntax is not everything, don't confuse it with semantics. The type checker still operates on the meaning, or representation, of the implicit unit return type.

2 Likes

No, no, I did not mean to say empty sets are crazy. Even if my school days were decades ago an empty set is as reasonable to me as an empty bucket of water.

What I was getting at is that there is no set. A somewhat different thing. Continuing the analogy there is no bucket. Which can be seen as kind of sort of true, if one has to wait an infinite amount of time to get the result there is no result. Not even an empty one.

I don't but you are likely right about the brushing up anyway.

Please, don't give up, this is interesting.

I was just thinking about that.

I thought we already had a symbol for the missing return type, the () as you say. Which I take to be an empty set. All well and good.

Today I have learned there are two different missing return types, there is the '!' as well. Which is also explained in this thread as an empty set.

Contrast all these functions that don't return anything:

fn f0() -> () {}

fn f1() -> ! {}. // Won't compile. 

fn f2() {}

fn f3() -> () {
    loop {}
}

fn f4() -> ! {
    loop {}
}

fn f5() {
    loop {}
}

Seems some empty sets are more empty than others.

Clearly I am still missing a subtle point.

() as a type is not an empty set. It is a singleton set, i.e. it has exactly one value: (). (It's an empty tuple, i.e. an empty product type, and the unit element of multiplication is 1, not 0.) If it were an empty set, then it would be a terrible default choice for an implicit return type – most functions don't diverge, so most of the time the just "fall off the end" syntactic convenience would result in a type error.

But there is a set. The type checker has to work with some return type. This is not a deep philosophical problem. It would be highly impractical to special case the never type by saying "this function has no return type" and then also special case all of the approximately 3 968 724 occurrences of handling function return types in the source code of the compiler. I claim that would be crazy. Representing a set of 0 types as an empty set is "only" done for consistency.

4 Likes

Your f3 (and f5, which is identical) compiles because ! can be coerced into any type, including (). (But not the other way round.)

3 Likes

You could say that. And there is even a sense in which you'd be right, but it isn't a useful thing to say in the context of proving interesting properties about your code.

The whole point of a type system is to get the compiler to prove interesting properties about your code so that you don't have to. Interesting properties like "this function can't be called without locking the mutex first" or "this entire program has no undefined behavior". To this end, it's useful to consider sets such as "the set of values that can be returned by this function". And sometimes, in the course of proving whatever particular properties you find interesting about this set of values, you might find that it's just empty. So it's useful to tell the compiler that fact. It's not useful to simply declare that the set doesn't exist, because that's not a meaningful statement in the logical language the compiler uses to try to prove things.

7 Likes

Ah ha.

It it is some kind of philosophical problem. I can see that the type checker has to work with some return type.

However, I don't. I know that function never returns. And hence there is no return or any type.

Anyway, likely we should wrap up this little side discussion. For the record, I don't think any of this is "crazy" it just a lot of technicality I have never had to think about much before and have to get to grips with.

I'll go and sleep on it.

Thanks all.

I think that enum declarations can be useful to get the number of elements in the set right.

Consider

enum TwoValues { First, Second }

The type TwoValues has two values, those are TwoValues::First and TwoValues::Second. Describing the set of all value of type TwoValues, that’s a 2-element set,

{TwoValues::First, TwoValues::Second}

Conveniently, the enum declaration itself already almost looks like this set: { First, Second }.


Next example, going lower:

enum OneValue { First }

well, that’s a type with a single value. Every instance of OnceValue will be OneValue::First, while the value of type TwoValues can be represented with 1 bit of data, a value of type OneValue needs 0 bits of data. Thus it’s a zero-sized type, still the set of values isn’t a 0-element set, but a 1-element set, namely the set

{OneValue::First}


Going lower:

enum ZeroValues { }

now that’s an enum without any values at all. You cannot construct a value of type ZeroValues. If a function promises “if I return, then I return a value of type ZeroValues”, then you know that that function will never return. Because values of type ZeroValues don’t exist. The set of all value of type ZeroValues exists: It’s the set

{ }

or sometimes written

so the “empty set”. The fact that no values of ZeroValues exists then corresponds to the fact that no elements of the empty set exist. The set itself exists, but elements of it don’t.


Comparing these enums with more canonical types from the Rust standard library, we’d have

the type TwoValues is like the type bool,
the value TwoValues::First corresponds to the value false,
the value TwoValues::Second corresponds to the value true,

the type OneValue is like the type ()
the value OneValue::First corresponds to the value the value (),

the type ZeroValues is like the type !

10 Likes

Reminder that you can just type ! into the search box in the std documentation: https://doc.rust-lang.org/nightly/std/?search=!

Which will give you a long page with plenty of examples.

2 Likes

Can't be said too often :sweat_smile:

Seriously though, it's quite useful what you can find out this way. Every keyword has its own page, too, for example. I'm also just noticing, that apparently ops::Not is missing an ! alias, it's not in those search results.

3 Likes

I've always found it super unintuitive that you can actually search for symbols such as ! or [] to find docs on them. I would never have guessed it on my own.

4 Likes

This would be amazing! Is there a specific RFC or something I could follow/thumbs-up to get notified for if/when this is added?

Heh, no, that's just my personal idea/vision. It's not really too important to discuss something like this until ! gets stabilized anyways, and it also makes the most sense if ! is actually made to implement all kinds of traits (like Fn(String)) – potentially implicitly / automatically. Having it implement traits like that is an idea I've seen somewhere else but I don't know where, and it feels like a highly nontrivial endeavor on its own, especially if the goal is to automatically have it implement certain traits.

1 Like