Void与absurd的工作机制及类型签名有效性问询

Let's break down your questions one by one, starting with the source code you shared:

Source code for Void states:

newtype Void = Void Void

instance showVoid :: Show Void where
  show = absurd

absurd :: forall a. Void -> a
absurd a = spin a where
  spin (Void b) = spin b

1. Why is absurd :: forall a. Void -> a a valid type signature? #

This boils down to core type theory, specifically the idea of the empty type (which Void represents).

In PureScript's type system, Void has no valid "real" inhabitants—you can't create a Void value without using unsafe tricks like unsafeCoerce. The type Void -> a describes a function that takes a value from an empty set and returns any type a. Logically, this is "vacuously true" (via the Curry-Howard correspondence, this maps to the idea that a contradiction can imply any proposition).

The compiler accepts this signature because it adheres to the type system's rules:

• The function takes a Void parameter, which is a valid, well-defined type.
• Claiming to return any type a is allowed because there's no scenario where the function would actually need to produce an a (since no valid Void input exists to trigger the function's body).

The infinite recursive implementation is just one way to write such a function—type checking only verifies that the implementation matches the signature, not whether it terminates.

2. Does the compiler allow this because it recognizes the function won't terminate? #

Nope, that's not the reason.

PureScript's type system doesn't check for termination by default. Non-terminating functions (like loop = loop) can have any type, but absurd's validity doesn't come from its non-termination.

Instead, its validity is rooted in the nature of Void itself. Even if you could write a terminating absurd (which you can't, since there's no way to process a Void value), the type signature would still be valid because there are no inputs to handle.

3. Can absurd = unsafeCoerce achieve the same effect? #

Kind of, but with huge caveats:

• Behavior with fake Void values: If you use unsafeCoerce to create a fake Void (e.g., unsafeCoerce "lol" :: Void), the original absurd will enter an infinite loop (it keeps unpacking the recursive Void constructor forever). The unsafeCoerce version, however, will directly cast the underlying value to type a—this might work if the memory layout of the fake Void matches a, but it's extremely unsafe and can lead to crashes, undefined behavior, or garbage results (like casting a string to an Int).
• Safety: The standard absurd is 100% safe in normal use because there's no way to get a valid Void value. unsafeCoerce bypasses the type system entirely, bringing all the risks of unsafe operations.
• Semantics: The standard absurd aligns with the logical meaning of Void (no inhabitants, so any output is valid). The unsafeCoerce version is a hack that ignores the semantic intent of absurd—it's a type cheat, not a logically sound implementation.

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