Scala and Haskell are there and I think they inspired this in Kotlin and Rust. In Haskell it's "bottom" and in Scala it's "Nothing".

In Scala no one uses "return" (mostly because we don't care about performance in the same way), but if you do, the way it is internally implemented is by throwing exceptions, so in a sense it suffers from the same problems as Rust.

It's actually very important to have that type in a language that uses immutable collections. Imagine this pseudocode:

    // List() creates an immutable list
    let emptyList = List() 
    let listWithAnInteger = emptyList.add(42)
    let listWithAString = emptyList.add("foo")

This works in Scala. But how can the compiler know that `emptyList.add(42)` is allowed? After all, you can only add things to a list where the added element matches the type of the other elements right?

The reason this works is because the type of emptyList will be List<Nothing> and since Nothing a subtype of every other type, the type of listWithAnInteger will become List<Integer>. You can annotate these types explicitly if you want.

Every language without such a bottom type has a failed type-system in my opinion. (looking at you Golang and many others)

? This works fine in a type system without an explicit bottom type. In Haskell or ML or whatever `emptyList` would be given a polymorphic type, `List a` or `'a list`.

There's issues around doing this with mutable collections (i.e. the value restriction) but that's not what you're referring to...

> In Haskell or ML or whatever `emptyList` would be given a polymorphic type, `List a` or `'a list`.

That alone would not work. Think about it: `List a` means "A list that contains values of type `a` and `a` can be any type whatsoever". Now imagine you combine that list with a list of integers. That obviously cannot work, since `(++) :: [a] -> [a] -> [a]` as you see, the types must align.

The way Haskell fixes that is (apparently) by doing something called `Let-generalisation` (https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/let_...)

To me that feels like hacky way to exactly resolve the problem that I described, and if you turn it off then that code would stop working and fail to compile as expected.

You are misreading the quantification, a value l of type List a means that for all type a, the element of the list has type a. In other words, this is an universal quantification whereas your interpretation is an existential quantification.

This is obviously only possible if the list itself has no elements, and indeed a simple proof is that the statement above is valid for the empty type: all elements of a list of type List a have type empty (among other types). Thus there are no elements in this list.

And both Haskell or OCaml can prove it:

     type empty = | (* this is defining a never type *)
     type polymorphic_list = { l: 'a. 'a list } 
     (* OCaml require to explicit construct polymorphic type *)

     let polymorphic_lists_are_empty ({l} : polymorphic_list ) =
     match (l:empty list) with
     | [] -> () (* this is the empty list *)
     | _ -> . 
     (* this clause requires to the OCaml typechecker to prove that the remaining cases are unreachable *)

> this is an universal quantification whereas your interpretation is an existential quantification

Indeed, I stand corrected. Interesting! I'll look into that a bit more, thank you.

Kotlin also has this type, it's called "Nothing".

https://kotlinlang.org/api/core/kotlin-stdlib/kotlin/-nothin...

As you can never get a value of type nothing, it can coerce into anything, just like rust's ! or () or typescripts never.

I recently realized (by playing with Lean) that coercing of "!" is because of the principle of explosion [1]. Basically propositions are types in Lean, and proofs are instances of those types. A proposition that is false doesn't have any instances, so they are like "!". Principle of explosion says ∀ P, False -> P, which is exactly the type signature for "!" coercing.

[1]: https://leanprover-community.github.io/mathlib4_docs/Init/Pr...