3 ms·
Kotlin also has this type, it's called "Nothing". https://kotlinlang.org/api/core/kotlin-stdlib/kotlin/-nothing/ https://kotlinlang.org/api/core/kotlin-stdlib/
by kuschku 1y ago
Kotlin also has this type, it's called "Nothing".
https://kotlinlang.org/api/core/kotlin-stdlib/kotlin/-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.
- nialv7 1y agoI 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/Prelude.html#False.elim https://leanprover-community.github.io/mathlib4_docs/Init/Pr...