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.

Answer 3

There is no way to construct a "real" value of a no-constructor type (where by "real" I mean a terminating computation; Haskell has undefined :: a, error :: String -> a and the possibility of writing nonterminating programs like mwahaha = mwahaha, which to be simplistic I'll call "fake" values).

One example of how this can be useful is versions 0.5 and later of the conduit library. The basic type in the library is Pipe l i o u m r; with different parameters for these types, a Pipe can serve either as a source (which produces output without consuming any input), a sink (consumes input without producing any output), or a conduit (consumes input and produces output). The i and o type parameters to Pipe are the types of its input and output, respectively.

So one of the ways the conduit library enforces the notion that sources consume no input and sinks produce no output by using the Void type from Data.Void as the input type for sources and output type for sinks. Again, there is no terminating way to construct a value of such a type, so a program that attempts to consume output from a sink will not terminate (which as a reminder, in Haskell this can mean "raise an error" and not necessarily "loop forever").

Answer 4

Types with no constructors are called phantom types. See the page in the Haskell wiki.