What is the significance of algebraic datatypes with zero constructors?

Question

This passage, which unfortunately lacks references, about the development of ADTs in Haskell, from A History of Haskell: Being Lazy With Class, section 5.1:

In general, an algebraic type specifies a sum of one or more alternatives, where each alternative is a product of zero or more fields. It might have been useful to permit a sum of zero alternatives, which would be a completely empty type, but at the time the value of such a type was not appreciated.

leaves me wondering, how would such an ADT be useful?

Answer 1

Theoretically: the Curry-Howard isomorphism gives us an interpretation of this type as the "false" proposition. "false" is useful as a proposition on its own; but is also useful for constructing the "not" combinator (as type Not a = a -> False) and other similar constructions.

Pragmatically: this type can be used to prevent certain branches of parameterized data types from coming into existence. For example, I've used this in a library for parsing various game trees something like this:

data RuleSet a            = Known !a | Unknown String
data GoRuleChoices        = Japanese | Chinese
data LinesOfActionChoices -- there are none in the spec!
type GoRuleSet            = RuleSet GoRuleChoices
type LinesOfActionRuleSet = RuleSet LinesOfActionChoices

The impact of this is that, when parsing a Lines of Action game tree, if there's a ruleset specified, we know its constructor will be Unknown, and can leave other branches off during pattern matches, etc.

Answer 2

Among corresponding to logical false (as stated in another answer), they are often used to create additional type constraints in combination with GADTs. For example:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyDataDecls #-}

import Data.List (groupBy)

data Zero
data Succ n

data Vec n a where
    Nil  ::                 Vec Zero a
    Cons :: a -> Vec n a -> Vec (Succ n) a

vhead :: Vec (Succ n) a -> a
vhead (Cons v _) = v

vtail :: Vec (Succ n) a -> Vec n a
vtail (Cons _ v) = v

Here we have two such data types with no constructor. Their meaning here is just to represent natural numbers: Zero, Succ Zero, Succ (Succ Zero) etc. They are used as phantom types in Vec data type so that we can encode the length of a vector in its type. Then, we can write type-safe functions such as vhead/vtail that can be applied only to non-empty vectors.

See also [Haskell] Fixed-length vectors in Haskell, Part 1: Using GADTs where the example is elaborated in detail.