What is the purpose of algebraic data types without a constructor?

Question

In Haskell you can define a algebraic data type without a constructor:

data Henk

But what is the purpose of a type (or kind?) that doesn't have a constructor?

Answer 1

Type-level machinery often requires types to exist but never constructs values of such types.

E.g., phantom types:

module Example (Unchecked, Checked, Stuff()) where

data Unchecked
data Checked
data Stuff c = S Int String Double

check :: Stuff Unchecked -> Maybe (Stuff Checked)
check (S i s d) = if i>43 && ...
                  then Just (S i s d)
                  else Nothing

readFile :: Filepath -> IO (Stuff Unchecked)
readFile f = ...

workWithChecked :: Stuff Checked -> Int -> String
workWithChecked stuff i = ...

workWithAny :: Stuff any -> Int -> Stuff any
workWithAny stuff i = ...

As long as the S constructor is not exported by the module, the user of this library can not forge the "checked" status on the Stuff data type.

Above, the workWithChecked function does not have to sanitize the input every time it is called. The user must have already done it, since it has to provide a value in the "checked" type -- and this means the user had to call the check function beforehand. This is an efficient and robust design: we do not repeat the same check over and over at every call, and yet we do not allow the user to pass unchecked data.

Note how the values of types Checked,Unchecked are immaterial -- we never use those.

As others mentioned in comments, there are many other uses of empty types than phantom types. For instance, some GADTs involve empty types. E.g.

data Z
data S n
data Vec n a where
  Nil  :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

Above we use empty types to record length information in types.

Further, types with no constructors are needed to achieve some theoretical properties: if we look for an a such that Either a T is isomorphic to T, we want a to be empty. In type theory, an empty type is commonly used as a type equivalent of a logically "false" proposition.