Haskell中Empty类型与Void类型的区别是什么？

Awesome question—this gets into some really interesting overlaps between Haskell's type system and category theory, plus the messy reality of bottom values. Let's unpack it all clearly.

First: Clarifying "Empty" vs. Void #

First off, Haskell's standard library doesn't have a built-in Empty type. When people talk about an "Empty type" here, they almost always mean a user-defined algebraic data type with no constructors, like this:

data Empty  -- No constructors, so no way to create a valid value (except bottom)

Void, on the other hand, is a standard type from Data.Void in the base library, defined exactly the same way (data Void), but with extra tooling and semantic weight baked in.

Core Differences Between Empty (custom) and Void #

1. Standard Library Support & Tooling #

• Void comes with out-of-the-box utilities that make it practical to use. The biggest one is absurd :: Void -> a—this is the key function that formalizes Void's role as an initial object (more on that in a sec). It also has pre-defined instances for common typeclasses like Show, Eq, Ord, and even Exception, making it useful for error handling and impossible-case signaling.
• A custom Empty type has none of this. You'd have to manually write your own version of absurd (like emptyAbsurd :: Empty -> a; emptyAbsurd x = case x of {}) and implement every typeclass you need from scratch. No built-in optimizations or ecosystem support here.

2. Status as Hask's Initial Object #

In category theory terms, an initial object in the Hask category is a type where exactly one function exists from it to every other type in the category.

• For Void, absurd is that unique function. Since there are no valid (non-bottom) values of type Void, absurd never actually needs to produce a value of type a—it's a proof that such a function must exist, even if it's never executed. GHC even recognizes absurd as a special case and optimizes it away where possible.
• A custom Empty type can act as an initial object too—you can write that emptyAbsurd function I mentioned, which is just as valid. But Void is the de facto standard implementation in Haskell. It's the type everyone recognizes as meaning "this can never happen", whereas a custom Empty is just a random empty ADT with no shared semantic meaning.

The Bottom Problem: Theory vs. Haskell's Reality #

You're right that Haskell's inclusion of bottom (⊥)—the non-terminating/error value present in every type—muddies the pure category theory picture.

• In ideal category theory, an uninhabited type has no values. But in Haskell, every type (including Void and custom Empty) includes ⊥. So you can write undefined :: Void or undefined :: Empty—both are valid.
• That said, Void is still designed to handle this edge case properly. absurd undefined just evaluates to undefined, which is the expected behavior: if you have a bottom value of type Void, propagating that bottom to the result type is the only sensible thing to do. A custom emptyAbsurd would do the same, but Void's design explicitly accounts for this reality, whereas a custom Empty is just a bare-bones empty type.

Another tiny but practical detail: GHC represents Void as a 0-byte type, which makes sense since there are no valid values to store. A custom Empty type will get the same treatment, but Void is the official, documented way to get this behavior.

Quick Recap #

• Use Void for "impossible state" signaling—it's standard, has great tooling, and carries clear semantic meaning.
• A custom Empty type is just a bare empty ADT with no built-in support; only use it if you have a very specific custom use case.
• Both act as initial objects in Hask when ignoring bottom, but Void is the accepted standard implementation.
• Bottom exists in both types, but Void is designed to handle it gracefully as part of its standard API.

内容的提问来源于stack exchange，提问作者user5158149