One of the remarkable property of ML languages is algebraic data types and then type systems. Look here<p>type Bottom = private Bottom of Bottom<p>Modeling any kind of data is intuitive and simple. This is why ML languages (F#, oCamel etc.) shines in industries where you've complex data like Finance.
Reading any F# code is like reading a novel. It starts with modeling of data and small functions. Then these small functions and data evolves into bigger features. File by file you keep moving upwards.
For example if you are writing a Json parser in F#, you start with Modeling Json data first. And here it is<p>type JsonValue =
| String of string
| Number of decimal
| Float of float
| Record of properties:(string * JsonValue)[]
| Array of elements:JsonValue[]
| Boolean of bool
| Null<p>Then everything starts from here.
Bottom types get difficult in presence of statically dispatched type classes / traits. Even though the bottom type doesn't have values, because it is an existing type you can still define traits on it. You could plausibly define any existing trait on it, or none at all, because it's logically consistent the either way: because the values don't exist, you can't actually call the trait methods so any trivial implementation (such as method that panics / throws and exception when called) will do. You won't get logical contradiction because you can't call it.<p>But then you get the difficulty of, which actual traits should that type implement? That's a hard decision to make, and it's the reason why Rust doesn't yet have a first class bottom type.
Swift has Never, which is the return type of functions that don't terminate, such as fatalError().<p><a href="https://developer.apple.com/documentation/swift/never" rel="nofollow">https://developer.apple.com/documentation/swift/never</a><p>It's currently not implemented as a bottom type in the sense that it's not the subtype of all types (discussed in <a href="https://nshipster.com/never/" rel="nofollow">https://nshipster.com/never/</a>).
Interestingly, if you read the article [0] linked in the reddit post referred to in this blog post, the author points out that the Haskell version of the bottom type has a problem - you can construct an inhabitant. Pulling out the relevant section of code:<p><pre><code> fix :: (a -> a) -> a -- defined in Data.Function
fix f = let x = f x in x -- least fixed point of f
false :: Void
false = fix (id :: Void -> Void)
</code></pre>
Since you can find an inhabitant of Void, you can therefore create an inhabitant of any type, so you can prove any proposition:<p><pre><code> inhabitant :: a
inhabitant = fix id
</code></pre>
I don't know if this is only really a problem if you were trying to use Haskell as a theorem prover. It might be the case that in practice, you're unlikely to run into this inconsistency. I think [1] provides a bit more discussion regarding this.<p>[0]: <a href="https://gciruelos.com/propositions-as-types.html" rel="nofollow">https://gciruelos.com/propositions-as-types.html</a>
[1]: <a href="https://frenchy64.github.io/2018/04/07/unsoundness-in-untyped-types.html" rel="nofollow">https://frenchy64.github.io/2018/04/07/unsoundness-in-untype...</a><p>EDIT: Just found this [2] which describes the above problem in type theory language.<p>[2]: <a href="https://en.wikipedia.org/wiki/System_U#Girard's_paradox" rel="nofollow">https://en.wikipedia.org/wiki/System_U#Girard's_paradox</a>
Rust actually has a type like this in addition to a bottom type (which is !). It is the Infallible type which is an enum type (a sum type) with no variants and is thus not constructible. It's purpose is to indicate that an operation always succeeds when that operation returns a Result type. But defining it that way, the compiler can use this information to remove error checks. While it doesn't implement every trait automatically, I found it to be pretty easy to implement every trait I cared about since the it just had to typecheck and not do anything useful.
Some discussion about a rejected suggestion for a bottom type and a local hack:<p><pre><code> type Bottom = private Bottom of Bottom
</code></pre>
which unfortunately<p>> [...] subtype of all types. My bottom type does not have this property.