You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: lib/elixir/pages/references/gradual-set-theoretic-types.md
+58-14Lines changed: 58 additions & 14 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -17,21 +17,38 @@ The current milestone aims to infer types from existing programs and use them fo
17
17
18
18
## A gentle introduction
19
19
20
-
Types in Elixir are written using the type named followed by parentheses, such as `integer()` or `list(integer())`. The basic types in the language are: `atom()`, `binary()`, `integer()`, `float()`, `function()`, `list()` (and `improper_list()`), `map()`, `pid()`, `port()`, `reference()`, and `tuple()`.
20
+
Types in Elixir are written using the type named followed by parentheses, such as `integer()` or `list(integer())`.
21
21
22
-
Many of the types above can also be written more precisely. We will discuss their syntax in detail later, but here are some examples:
22
+
The basic types are:
23
+
24
+
```elixir
25
+
atom()
26
+
binary()
27
+
empty_list()
28
+
integer()
29
+
float()
30
+
function()
31
+
map()
32
+
non_empty_list(elem_type, tail_type)
33
+
pid()
34
+
port()
35
+
reference()
36
+
tuple()
37
+
```
38
+
39
+
Many of the types above can also be written more precisely. We will discuss their syntax in the next sections, but here are two examples:
23
40
24
41
* While `atom()` represents all atoms, the atom `:ok` can also be represented in the type system as `:ok`
25
42
26
43
* While `tuple()` represents all tuples, you can specify the type of a two-element tuple where the first element is the atom `:ok` and the second is an integer as `{:ok, integer()}`
27
44
28
-
* While `function()` represents all functions, you can specify a function that receives an integer and returns a boolean as `(integer() -> boolean())`
29
-
30
45
There are also three special types: `none()` (represents an empty set), `term()` (represents all types), `dynamic()` (represents a range of the given types).
31
46
32
47
Given the types are set-theoretic, we can compose them using unions (`or`), intersections (`and`), and negations (`not`). For example, to say a function returns either atoms or integers, one could write: `atom() or integer()`.
33
48
34
-
Intersections will find the elements in common between the operands. For example, `atom() and integer()`, which in this case it becomes the empty set `none()`. You can combine intersections and negations to perform difference, for example, to say that a function expects all atoms, except `nil` (which is an atom), you could write: `atom() and not nil`.
49
+
Intersections will find the elements in common between the operands. For example, `atom() and integer()`, which in this case is the empty set `none()`. You can combine intersections and negations to perform difference, for example, to say that a function expects all atoms, except `nil` (which is an atom), you could write: `atom() and not nil`.
50
+
51
+
You can find a complete reference in the [set-theoretic types cheatsheet](../cheatsheets/types-cheat.cheatmd).
35
52
36
53
## The syntax of data types
37
54
@@ -63,24 +80,51 @@ Internally, Elixir represents the type `list(a)` as the union two distinct types
63
80
64
81
#### Improper lists
65
82
66
-
You can represent all _improper_ lists as `improper_list()`. Most times, however, an `improper_list` is built by passing a second argument to `non_empty_list`, which represents the type of the tail.
83
+
While most developers will simply use `list(a)`, the type system can express all different representations of lists in Elixirby passing a second argument to `non_empty_list`, which represents the type of the tail.
67
84
68
85
A proper list is one where the tail is the empty list itself. The type `non_empty_list(integer())` is equivalent to `non_empty_list(integer(), empty_list())`.
69
86
70
87
If the `tail_type` is anything but a list, then we have an improper list. For example, the value `[1, 2 | 3]` would have the type `non_empty_list(integer(), integer())`.
71
88
72
-
While most developers will simply use `list(a)`, the type system can express all different representations of lists in Elixir. At the end of the day, `list()` and `improper_list()` are translations to the following constructs:
73
-
74
-
list() == empty_list() or non_empty_list(term())
75
-
improper_list() == non_empty_list(term(), term() and not list())
89
+
If you pass a list type as the tail, then the list type is merged into the element type. For example, `non_empty_list(integer(), list(binary()))` is the same as `non_empty_list(integer() or binary(), empty_list())`.
76
90
77
91
### Maps
78
92
79
-
You can represent all maps as `map()`. Maps may also be written using their literal syntax, such as `%{name: binary(), age: integer()}`, which outlines a map with exactly two keys, `:name` and `:age`, and values of type `binary()` and `integer()` respectively.
93
+
You can represent all maps as `map()`.
94
+
95
+
Maps may also be written using their literal syntax, such as `%{name: binary(), age: integer()}`, which outlines a map with exactly two keys, `:name` and `:age`, and values of type `binary()` and `integer()` respectively.
96
+
97
+
A key may be marked as optional using the `if_set/1` operation on its value type. For example, `%{name: binary(), age: if_set(integer())}` is a map that certainly has the `:name` key but it may have the `:age` key (and if it has such key, its value type is `integer()`).
98
+
99
+
We say the maps above are "closed": they only support the keys explicitly defined. We can also mark a map as "open", by including `...` as its first element.
100
+
101
+
For example, the type `%{..., name: binary(), age: integer()}` means the keys `:name` and `:age` must exist, with their respective types, but any other key may also be present. In other words, `map()` is the same as `%{...}`. For the empty map, you may write `%{}`, although we recommend using `empty_map()` for clarity.
102
+
103
+
#### Domain types
80
104
81
-
We say the map above is a "closed" map: it only supports the two keys explicitly defined. We can also mark a map as "open", by including `...` as its last element. For example, the type `%{name: binary(), age: integer(), ...}` means the keys `:name` and `:age` must exist, with their respective types, but any other key may also be present. In other words, `map()` is the same as `%{...}`. For the empty map, you may write `%{}`, although we recommend using `empty_map()` for clarity.
105
+
In the examples above, all map keys were atoms, but we can also use other types as map keys. For example:
106
+
107
+
```elixir
108
+
# Closed map
109
+
%{binary() oratom() =>integer()}
110
+
111
+
# Open map
112
+
%{..., binary() oratom() =>integer()}
113
+
```
114
+
115
+
Currently, the type system only tracks the top of each individial type as the domain keys. For example, if you say:
Structs are closed maps with the `__struct__` key pointing to the struct name.
127
+
Furthermore, it is important to note that domain keys are, by definition, optional. Whenever you have a `%{integer() => integer()}`and you try to fetch a key, we must assume the key may not exist (after all, it is not possible to store all integers as map keys as they are infinite).
84
128
85
129
### Functions
86
130
@@ -158,4 +202,4 @@ The third milestone is to introduce set-theoretic type signatures for functions.
158
202
159
203
## Acknowledgements
160
204
161
-
The type system was made possible thanks to a partnership between [CNRS](https://www.cnrs.fr/) and [Remote](https://remote.com/). The research was partially supported by [Supabase](https://supabase.com/) and [Fresha](https://www.fresha.com/). The development work is sponsored by [Fresha](https://www.fresha.com/), [Starfish*](https://starfish.team/), and [Dashbit](https://dashbit.co/).
205
+
The type system was made possible thanks to a partnership between [CNRS](https://www.cnrs.fr/) and [Remote](https://remote.com/). The development work is currently sponsored by [Fresha](https://www.fresha.com/), and [Tidewave](https://tidewave.ai/).
0 commit comments