Why is the unit type's type and value the same?

Learn
1

This is more of a curiosity after creating a bare-minimum Elm app.
…

type alias Model =
    ()


initialModel : Model
initialModel =
    ()

...

The type of the unit type is () and its value is also (). I don’t recall if that’s true for any other type as other types generally have human readable names.

2

It’s empty tuple and uses same syntax as other tuples:

Types: (Int, Int) - (Int) - ()
Values: (1, 2) - (1) - ()

EDIT: Actually I’m not sure whether Elm supports single-value tuples.

1 Like
3

Ah, well there you have it. The unit type is not actually a separate type. It’s a tuple with no values. Makes sense now.

4

There is also the type {} which has only the value {}

1 Like
5

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!

6

This topic was automatically closed 10 days after the last reply. New replies are no longer allowed.