This is far beyond the realm of Elm, but the property you describe—that there is only a single value of type
(), which is
()—is called a singleton. This is a building block in a broader concept called dependent types, which are types that are dependent on a values. There are a few advanced languages that support dependent types.
The Idris language, for example, allows you to define a
Vector type in terms of a fixed-length
List. You can then write functions like append, which add two
Vector values together, but the type signature guarantees that the length of the return vector is the sum of the lengths of the two input vectors.
-- append in the Idris language
append : Vect n a -> Vect m a -> Vect (n + m) a
append vec1 vec2 =
-- adds vec1 and vec2 together
Pretty cool stuff!