A level type mechanism often requires types, but never creates values of such types.
For example, 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 isd) = if i>43 && ... then Just (S isd) 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 = ...
Unless the S constructor is exported by the module, the user of this library cannot fake the "checked" status in the Stuff data type.
Above, the workWithChecked function workWithChecked not sanitize an input signal every time it is called. The user had to do this, since he had to specify a value in the "checked" type, and this means that the user had to call the check function in advance. This is an efficient and reliable design: we do not repeat the same check again and again with every call, and yet we do not allow the user to transmit unverified data.
Please note that the values of the Checked , Unchecked types are Unchecked significant - we never use them.
As mentioned in the comments, there are many other uses for empty types than phantom types. For example, some GADT include empty types. For example.
data Z data S n data Vec na where Nil :: Vec Z a Cons :: a -> Vec na -> Vec (S n) a
Above, we use empty types to record length information in types.
In addition, to achieve some theoretical properties, types without constructors are needed: if we look for a so that Either a T is isomorphic to T , we want a be empty. In type theory, an empty type is usually used as the equivalent of a type of logically "false" sentence.