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!