Similarities and differences between Unit and Bottom types?

Question

I came across this recent Reddit thread, Thoughts on Botton vs Unit Types, but I don't understand what the similarities and differences are in regards to when you are creating a programming language.

If you are creating a programming language, why do you need both a Bottom and a Unit type (as defined in the thread).

For the sake of this discussion, let's call the bottom type a type that has no members. NIL in Common Lisp, Nothing in Scala, never in TypeScript, Never in Swift. This type can be used to indicate the return type of a function that never returns (a function that only throws an exception, for example).

Let's call the unit type a type that has a single member. NULL and NIL in Common Lisp (the symbol NIL not to be confused with the type NIL), () and () in Haskel, Unit and () in Scala, Void and () in Swift.

What exactly are the differences between the two as well?

In my PL, I currently just have a void type, which is meant to mean "nothing" or "empty" or "null" I would think, but this throws into question what I am doing. It seems I need to add another type, but not sure how it fits in. Because then in Rust you have the None type, I don't see why I couldn't just make that the void type as well. That sort of stuff. What are the similarities and differences, and why do you need both?

Answer 1

Jörg W Mittag gives an excellent answer. But I think it does miss the heart of the question. The quote says "For the sake of this discussion, let's call the bottom type a type that has no members." So while Jorg is right that the "the defining feature of a bottom type is not that it has no members" and that "it is perfectly possible for a bottom type to have members", we should also consider that it is perfectly possible for a bottom type to have no members.

Why would a type with no members be useful and why can't we just use the unit type for the same thing?

Unit and None

So let's consider a language that has a type Unit with one member unit and a type None with no members. I'll assume that unit is not a member of "ordinary" types like Int. While we are at it, let's assume that the only members of Int are integers.

A case for Unit

If we declare a function

fun foo() : T is .... end 

where T is a type, that usually means that if a call returns, it returns a value that is a member of type T. Or to put it another way

Any call to foo either returns a member of T or doesn't return

If T is Unit, that means that any call to foo will return (if it returns) a member of Unit, i.e. unit. Since the value returned is entirely predictable, there is no point writing say

val x : Unit = foo() 

since the value of x is a forgone conclusion. We might as well just write

foo()

Unit is playing the role that void plays in C or Java. The only difference is that we are treating Unit as a type, whereas in C and Java void is not really a type.

So what about None, why not use that instead of Unit for our analog of void?

Consider

fun bar() : None is ... end 

From our understanding of what this means, we see that

Any call to bar either returns a member of None or doesn't return

But since None has no members, this is equivalent to

No call to bar returns.

That doesn't sound like void. None is not a suitable analog for void, but Unit is.

Three cases for None

Is there any point to having None?

Here are three arguments for having a None type. But note that these arguments don't really rest on None having no members, but rather that it is a subtype of all other types in the language, i.e. that it is a bottom type.

None as a return type

A function that returns None sounds pretty useless. But it isn't completely useless. Suppose I have a function that always throws an exception, then I can write

fun unreachable() : None is
    throw new AssertionError("Unreacble code reached")
end

This can be useful for defensive programming. E.g.

fun partial(a : Int) : Int is
    if a > 0
        return 1 
    else if a < 0
        return -1
    else
        return unreachable()
    end
end

This should type-check since None is a subtype of Int.

What if we had used used Unit for the return type of unreachable? The subroutine above would not type check. Since Unit is not a subtype of Int). So we'd have to rewrite the else part as, for example

 unreachable()
 return 42

which looks rather arbitrary.

Here is a more compelling example. Here we have a generic function

fun assertWithResult<T>( b : Bool, v : T, m : String := "Assertion failed" ) : T is
    if b
        return v
    else
        return (throw new AssertionError( m ) )
    end
 end 

For this to typecheck, we need for throw new AssertionError( m ) to have the bottom type. If we rewrite the code as

else
    throw new AssertionError( m )
end

The language implementation will (I'd hope) complain about the missing return. We can't rewrite it as

else
    throw new AssertionError( m )
    return ...
end

since there is nothing we can write in the place of .... null is not the answer because I'm supposing null is not a member of Int, for example. unit has the same problem. I'll consider the case where there is a null value that's in every type later.

None as the type of something that isn't there.

Suppose our language has lists. (These are lists of values, as in Haskell -- not lists of locations as in Python.)

A reasonable rule for list catenation is that the type of xs ++ ys is List[T|U] where the type of xs is List[T], the type of ys is List[U] and T|U is the smallest type that contains the union of the members of T and U.

What is the type of the empty list constant []. If it is List[Unit], then [1,2,3] ++ [] will have type List[Int|Unit], which is probably not what you want. But if the type of the empty list constant is List[None] we have List[Int|None] which is List[Int].

Intersection types

Let's introduce multiple inheritance into our language. Given two interfaces I and J we can write I&J for the combination of both. I.e. the members or I&J are exactly the members of I intersected with the members of J. Why not allow intersection types for any two types? Now what is Int&Unit? Again None comes to the rescue.

Error without Unit or None

In Haskell, there is bottom type that has one member, which represents an error value. This error value is also a member of all other types.

The arguments above don't require that the bottom type have no members, just that it is a bottom type. (This is the point Jörg made.)

Imagine a language where we have a bottom type Error that contains one value, call it err that represents an error; and where err is a member of all types. err is the value of expressions that have errors, e.g., the value of 1/0 might be err and the value of 1/0 = 1/0 would also be err. (In the literature err is often written $\bot$ and called "bottom", but I'm going to avoid that terminology so that the term bottom isn't used with two technical meanings.) It follows that None is not a type in this language. (Int and Unit are also ruled out, but let's define a new type Int? that contains only integers and err.) We'll say that a function that does not return a value implicitly returns err. For example

fun incr( x : in out Int?) : Error is x := x+1 end 

is a reasonable function. (The implementation won't complain about a missing return, because return err is implicit.) It always returns err but, if we don't use the value, this is not an issue.

Now consider

fun baz() : Int?
    var y : Int? := 0
    if <<Something>>
        return 1
    else
        return incr(z)
end fun

This will type-check since Error is a subtype of Int?. Personally, I'd rather that it not type-check. I'd rather find out about the error before run time. So even if my bottom type contains an error value, I'd still like to have a unit type (Unit?) that additionally contains a non-error value. My personal feelings aside, this is a possible language design.

We can do without None by making the value of throw be err.

In short, whether or not you have an error value that is a member of every type or not, is largely orthogonal to the other issues such as whether you want unit and Unit. But it makes a difference to whether your bottom type is empty or not.

Is Error better than None?

One argument for all types having an error value holds for languages with lazyness. Suppose we have a type Int*Int that consist of pairs of Integers. In a lazy language (i, a[i]) (where i is an integer variable and a is a list of integers) must have a value, even if i is an out of bounds index. That's because first( (i, a[i] ) would have no error at compile or run time. But no pair of integers makes sense if i is out of bounds. The solution is to have Int? instead of Int. (You could have both, but the type of a[i] or any integer expression that might contain an error should be Int?, not Int.

A very pragmatic reason to have an error value is for uninitialized locations in an imperative language. Again you could have both Int? and Int, but locations of type Int would have to be initialized to integer. This is sort of the approach Java takes. Locations of type int are initialized to 0 by default. But location of type Integer are initialized to null by default. Granted, null is not the same as err since null is a first class value.

There are theoretical reasons for all type having to be inhibited by an error value. For example in Dana Scott's domain theory all types have a bottom value and this is important for showing that all well-typed functions have a meaning.

Null without Unit or None

Finally, we might consider a design where every type (except None and Error) has some particular non-error value, call it "null". Think of Java with the primitive types int, bool, double, etc. expunged. Now we can have a type Null that contains only null. (Or, if all inhabited types should have an err value, we can have a type Null? that contains only null and err.) I don't think there is much of a case for a Unit (or Unit? type containing both unit and null. Do we still need None? I think none of my arguments above for None are strong in this case. We can ditch the None type and then Null (or Error if you have err as value and Error as type) will be the bottom type and also the stand in for void.

Appendix

Summary of types mentioned above

• None no members, subtype of everything
• Error contains only err.
• Null contains only null.
• Null? contains only null and err.
• Unit contains only unit.
• Unit? contains only unit and err.
• Int contains only integers.
• Int? contains only integers and err.
• List[None] contains only the empty list.
• List[Int] contains only lists all of whose members are integers. Supertype of List[None].
• T | U the smallest type that contains all members of T and all members of U.
• T & U a type containing only values that are members of both T and U.

Answer 2

I think you are conflating several different issues, in addition to conflating concepts from mathematical type theory with concepts from practical, "real-world" programming language design.

In practical programming language design, the defining feature of a bottom type is not that it has no members. The defining feature of a bottom type is that it is a subtype of every (other) type, i.e. that it sits at the "bottom" of the type hierarchy. (The opposite is a top type.)

A unit type is a type which has only a single member.

It is perfectly possible for a bottom type to have members. For example, in Scala, Null is the bottom type for all reference types (i.e. it is the bottom type for the half of the type hierarchy which branches off of AnyRef) but it has a single member, null. (Which, technically, also makes it a unit type.)

In mathematical type theory, because of the fact that a unit type has only a single member, the unit type and the unit value convey no information. As a result, also, all unit types and unit values are isomorphic, so there is only the unit type and the unit value.

But this is not necessarily true for practical programming language design. There may be legitimate reasons to want to distinguish between different unit types or to have multiple bottom types for different parts of the type hierarchy, or to have bottom types have a member.

From a programming language perspective, there are good reasons to want to distinguish between a subroutine which does not return a useful value and a subroutine which does not return at all. I.e. a subroutine which prints something and a subroutine which runs into an infinite loop are very much not the same thing, and thus it makes sense for them to have different types.

Some programming languages don't care about one or both of those. E.g. Pascal does not concern itself with subroutines that do not return. It does, however, distinguish between subroutines which return a useful value and subroutines that don't. In Pascal, this is not handled via different return types but rather by having two different kinds of subroutines: FUNCTIONs return a value, PROCEDUREs don't.

Some programming languages have a special type annotation which is not actually a type itself which designates a subroutine as not returning a useful value. E.g. in Java, void is not a type, but a special keyword denoting the absence of a useful return type.

Many of these programming languages also have the distinction between expressions and statements where expressions evaluate to a value and have a type, and statements only have side-effects and don't have a type.

Some programming languages, like Scala, only have expressions, and only have subroutines which evaluate to a value. However, Scala is still an impure, partial programming language, so you can have expressions and subroutines which don't evaluate to a useful value and ones that don't terminate.

In Scala, all of these need to have a type, and IFF they return, they also need to return something. They can't just return nothing like in C or Java.

For something which returns no useful value, it makes sense that this value is the unit value and the type is the unit type. In general, there is no need to have multiple "no useful values" and there is no need to have multiple "no useful types". So, the unit type and the unit value are a sensible choice for that reason alone, regardless of the connection between programming and logic. But of course, there are good reasons based on the Curry-Howard-Isomorphism, Girard-Reynolds-Isomorphism, etc. as well why that should be the case.

Likewise, for something which never returns, it makes sense to use a type that has no members. This makes it clear that the method never returns, since if it were to return, it would need to return a value, which it can't, because there is no value of that type.

It also makes sense for this type to be the subtype of every other type: if the subroutine never returns, then I obviously use its return value everywhere where a value of any type is expected, because I know this value will never actually be consumed since the computation will never progress any further. Since I can pass this value that can never exist anywhere for any type, this means that the value must be a member of every type, and one of the ways to achieve this is to make its type the subtype of every type.

As to your question

why do you need both?

Clearly, the answer is "You don't", since there are successful programming languages like C, C++, Java, C#, which don't have both unit types and bottom types, and even successful programming languages like ECMAScript, PHP, Python, Perl, Ruby, Lua, and many others which don't even have types at all.

IFF you even care at all about subroutines which don't return and/or subroutines which return no useful value, AND IFF you want to distinguish between the two, AND IFF you want to use the type system for that distinction (as opposed to, say, two different kinds of subroutines like Pascal does), THEN you will typically end up with something which looks like a bottom type, something which looks like a unit type, and something which looks like a unit value.

But if you don't care about any of that, then you don't need both or even either.