data Void where Void :: { absurd :: forall a. a } -> Void ^ I just defined a type with no inhabitants [1] along with the ability to use a value of it to pr

data Void where Void :: { absurd :: forall a. a } -> Void ^ I just defined a type with no inhabitants [1] along with the ability to use a value of it to prove anything. And it leans on the type system features & ergonomics Go & Rust don't even get close to having. This is a pedantic example in a way, but this type is actually very useful in practice! And defining the type almost reads like English (or at least math English.) Haskell is just a different world. You program with type variables of different shapes and sizes and relationships like it's nothing and it Just Works. Go's new generics & Rust's are crufty in comparison. Both due to syntax and semantics. [1] modulo bottom..I know, I know :)