Improve pretty printing of types and fix list tail

lib/elixir/lib/module/types/apply.ex

@@ -218,7 +218,11 @@ defmodule Module.Types.Apply do
         {:erlang, :trunc, [{[union(integer(), float())], integer()}]},
 
         # TODO: Replace term()/dynamic() by parametric types
-        {:erlang, :++, [{[list(term()), term()], dynamic(list(term(), term()))}]},
+        {:erlang, :++,
+         [
+           {[empty_list(), term()], dynamic(term())},
+           {[non_empty_list(term()), term()], dynamic(non_empty_list(term(), term()))}
+         ]},
         {:erlang, :--, [{[list(term()), list(term())], dynamic(list(term()))}]},
         {:erlang, :andalso, [{[boolean(), term()], dynamic()}]},
         {:erlang, :delete_element, [{[integer(), open_tuple([])], dynamic(open_tuple([]))}]},

lib/elixir/lib/module/types/descr.ex

@@ -40,6 +40,7 @@ defmodule Module.Types.Descr do
   }
   @empty_list %{bitmap: @bit_empty_list}
   @not_non_empty_list Map.delete(@term, :list)
+  @not_list Map.replace!(@not_non_empty_list, :bitmap, @bit_top - @bit_empty_list)
 
   @empty_intersection [0, @none]
   @empty_difference [0, []]
@@ -69,7 +70,7 @@ defmodule Module.Types.Descr do
   def integer(), do: %{bitmap: @bit_integer}
   def float(), do: %{bitmap: @bit_float}
   def fun(), do: %{bitmap: @bit_fun}
-  def list(type, tail \\ @empty_list), do: list_descr(type, tail, true)
+  def list(type), do: list_descr(type, @empty_list, true)
   def non_empty_list(type, tail \\ @empty_list), do: list_descr(type, tail, false)
   def open_map(), do: %{map: @map_top}
   def open_map(pairs), do: map_descr(:open, pairs)
@@ -391,11 +392,7 @@ defmodule Module.Types.Descr do
         case descr do
           %{list: list, bitmap: bitmap} when (bitmap &&& @bit_empty_list) != 0 ->
             descr = descr |> Map.delete(:list) |> Map.replace!(:bitmap, bitmap - @bit_empty_list)
-
-            case list_to_quoted(list, :list, opts) do
-              [] -> {[{:empty_list, [], []}], descr}
-              unions -> {unions, descr}
-            end
+            {list_to_quoted(list, true, opts), descr}
 
           %{} ->
             {[], descr}
@@ -418,7 +415,7 @@ defmodule Module.Types.Descr do
   defp to_quoted(:bitmap, val, _opts), do: bitmap_to_quoted(val)
   defp to_quoted(:dynamic, descr, opts), do: dynamic_to_quoted(descr, opts)
   defp to_quoted(:map, dnf, opts), do: map_to_quoted(dnf, opts)
-  defp to_quoted(:list, dnf, opts), do: list_to_quoted(dnf, :non_empty_list, opts)
+  defp to_quoted(:list, dnf, opts), do: list_to_quoted(dnf, false, opts)
   defp to_quoted(:tuple, dnf, opts), do: tuple_to_quoted(dnf, opts)
 
   @doc """
@@ -841,13 +838,17 @@ defmodule Module.Types.Descr do
 
   ## List
 
-  # Represents both list and improper list simultaneously using a pair {list_type, last_type}.
+  # Represents both list and improper list simultaneously using a pair
+  # `{list_type, last_type}`.
   #
-  # For proper lists, the last_type is empty_list().
-  # In general, list(term(), term()) is interpreted as {term(), term()}
-  # and not non_empty_list(term(), term()).
+  # We compute if it is a proper or improper list based if the last_type
+  # is an empty_list() or a list(). In particular, the last_type is not
+  # pruned to remove the empty_list() or list(), and therefore it may
+  # contain the list itself. This is ok because operations like `tl`
+  # effectively return the list itself plus the union of the tail (and
+  # if the tail includes the list itself, they are equivalent).
   #
-  # Note: A type being none() is handled separately.
+  # none() types can be given and, while stored, it means the list type is empty.
   defp list_descr(list_type, last_type, empty?) do
     {list_dynamic?, list_type} = list_pop_dynamic(list_type)
     {last_dynamic?, last_type} = list_pop_dynamic(last_type)
@@ -861,6 +862,10 @@ defmodule Module.Types.Descr do
             list_new(list_type, last_type)
 
           {dnf, last_type} ->
+            # It is safe to discard the negations for the tail because
+            # `list(term()) and not list(integer())` means a list
+            # of all terms except lists where all of them are integer,
+            # which means the head is still a term().
             {list_type, last_type} =
               Enum.reduce(dnf, {list_type, last_type}, fn {head, tail, _}, {acc_head, acc_tail} ->
                 {union(head, acc_head), union(tail, acc_tail)}
@@ -1051,55 +1056,77 @@ defmodule Module.Types.Descr do
 
   defp list_tl_static(:term), do: :term
 
-  defp list_tl_static(descr) do
-    case descr do
-      %{list: dnf} ->
-        Enum.reduce(dnf, %{list: dnf, bitmap: @bit_empty_list}, fn {_, last, _}, acc ->
-          union(last, acc)
-        end)
+  defp list_tl_static(%{list: dnf} = descr) do
+    initial =
+      case descr do
+        %{bitmap: bitmap} when (bitmap &&& @bit_empty_list) != 0 ->
+          %{list: dnf, bitmap: @bit_empty_list}
 
-      %{bitmap: bitmap} when (bitmap &&& @bit_empty_list) != 0 ->
-        empty_list()
+        %{} ->
+          %{list: dnf}
+      end
 
-      %{} ->
-        none()
-    end
+    Enum.reduce(dnf, initial, fn {_, last, _}, acc ->
+      union(last, acc)
+    end)
   end
 
-  defp list_to_quoted(dnf, name, opts) do
+  defp list_tl_static(%{}), do: none()
+
+  defp list_improper_static?(:term), do: false
+  defp list_improper_static?(%{bitmap: bitmap}) when (bitmap &&& @bit_empty_list) != 0, do: false
+  defp list_improper_static?(term), do: equal?(term, @not_list)
+
+  defp list_to_quoted(dnf, empty?, opts) do
     dnf = list_normalize(dnf)
 
-    for {list_type, last_type, negs} <- dnf, reduce: [] do
-      acc ->
-        arguments =
-          if subtype?(last_type, @empty_list) do
-            [to_quoted(list_type, opts)]
+    {unions, list_rendered?} =
+      Enum.reduce(dnf, {[], false}, fn {list_type, last_type, negs}, {acc, list_rendered?} ->
+        {name, arguments, list_rendered?} =
+          cond do
+            list_type == term() and list_improper_static?(last_type) ->
+              {:improper_list, [], list_rendered?}
+
+            subtype?(last_type, @empty_list) ->
+              name = if empty?, do: :list, else: :non_empty_list
+              {name, [to_quoted(list_type, opts)], empty?}
+
+            true ->
+              args = [to_quoted(list_type, opts), to_quoted(last_type, opts)]
+              {:non_empty_list, args, list_rendered?}
+          end
+
+        acc =
+          if negs == [] do
+            [{name, [], arguments} | acc]
           else
-            [to_quoted(list_type, opts), to_quoted(last_type, opts)]
+            negs
+            |> Enum.map(fn {ty, lst} ->
+              args =
+                if subtype?(lst, @empty_list) do
+                  [to_quoted(ty, opts)]
+                else
+                  [to_quoted(ty, opts), to_quoted(lst, opts)]
+                end
+
+              {name, [], args}
+            end)
+            |> Enum.reduce(&{:or, [], [&2, &1]})
+            |> Kernel.then(
+              &[
+                {:and, [], [{name, [], arguments}, {:not, [], [&1]}]}
+                | acc
+              ]
+            )
           end
 
-        if negs == [] do
-          [{name, [], arguments} | acc]
-        else
-          negs
-          |> Enum.map(fn {ty, lst} ->
-            args =
-              if subtype?(lst, @empty_list) do
-                [to_quoted(ty, opts)]
-              else
-                [to_quoted(ty, opts), to_quoted(lst, opts)]
-              end
-
-            {name, [], args}
-          end)
-          |> Enum.reduce(&{:or, [], [&2, &1]})
-          |> Kernel.then(
-            &[
-              {:and, [], [{name, [], arguments}, {:not, [], [&1]}]}
-              | acc
-            ]
-          )
-        end
+        {acc, list_rendered?}
+      end)
+
+    if empty? and not list_rendered? do
+      [{:empty_list, [], []} | unions]
+    else
+      unions
     end
   end
 
@@ -1858,6 +1885,10 @@ defmodule Module.Types.Descr do
     {:empty_map, [], []}
   end
 
+  def map_literal_to_quoted({:open, fields}, _opts) when map_size(fields) == 0 do
+    {:map, [], []}
+  end
+
   def map_literal_to_quoted({:open, %{__struct__: @not_atom_or_optional} = fields}, _opts)
       when map_size(fields) == 1 do
     {:non_struct_map, [], []}

lib/elixir/pages/references/gradual-set-theoretic-types.md

@@ -30,7 +30,7 @@ Intersections will find the elements in common between the operands. For example
 
 ## The syntax of data types
 
-In this section we will cover the syntax of all data types.
+In this section we will cover the syntax of all data types. At the moment, developers will interact with those types mostly through compiler warnings and diagnostics.
 
 ### Indivisible types
 
@@ -56,18 +56,26 @@ You can also specify the type of the list element as argument. For example, `lis
 
 Internally, Elixir represents the type `list(a)` as the union two distinct types, `empty_list()` and `not_empty_list(a)`. In other words, `list(integer())` is equivalent to `empty_list() or non_empty_list(integer())`.
 
-Elixir also supports improper lists, where the last element is not an empty list, via `non_empty_list(elem_type, tail_type)`. For example, the value `[1, 2 | 3]` would have the type `non_empty_list(integer(), integer())`.
+#### Improper lists
+
+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.
+
+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())`.
+
+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())`.
 
 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:
 
     list() == empty_list() or non_empty_list(term())
-    improper_list() == non_empty_list(term(), term() and not empty_list())
+    improper_list() == non_empty_list(term(), term() and not list())
 
 ### Maps
 
 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.
 
-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. Structs are closed maps with the `__struct__` key pointing to the struct name.
+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.
+
+Structs are closed maps with the `__struct__` key pointing to the struct name.
 
 ### Functions
 
@@ -105,7 +113,7 @@ def negate(x) when is_integer(x), do: -x
 def negate(x) when is_boolean(x), do: not x
 ```
 
-Elixir type checks it as if the function had the type `(dynamic() -> dynamic())`. Then, based on patterns and guards, we can refine the value of the variable `x` to be `dynamic() and integer()` and `dynamic() and boolean()` for each clause respectively. We say `dynamic()` is a gradual type, which leads us to *gradual set-theoretic types*.
+Elixir type checks it as if the function had the type `(dynamic() -> dynamic())`. Then, based on patterns and guards, we can refine the value of the variable `x` to be `dynamic() and integer()` and `dynamic() and boolean()` for each clause respectively. We say `dynamic()` is a gradual type, which leads us to _gradual set-theoretic types_.
 
 The simplest way to reason about `dynamic()` in Elixir is that it is a range of types. If you have a type `atom() or integer()`, the underlying code needs to work with both `atom() or integer()`. For example, if you call `Integer.to_string(var)`, and `var` has type `atom() or integer()`, the type system will emit a warning, because `Integer.to_string/1` does not accept atoms.
 
@@ -131,7 +139,7 @@ Inferring type signatures comes with a series of trade-offs:
 
 On the other hand, type inference offers the benefit of enabling type checking for functions and codebases without requiring the user to add type annotations. To balance these trade-offs, Elixir has a two-steps system, where we first perform module-local inference on functions without type signatures, and then we type check all modules. Module-local inference means the types of the arguments, return values, and all variables are computed considering all of the function calls to the same module and to Elixir's standard library. Any call to a function in another module is conservatively assumed to return `dynamic()` during inference.
 
-Type inference in Elixir is best-effort: it doesn't guarantee it will find all possible type incompatibilities, only that it may find bugs where all combinations of a type *will* fail, even in the absence of explicit type annotations. It is meant to be an efficient routine that brings developers some benefits of static typing without requiring any effort from them.
+Type inference in Elixir is best-effort: it doesn't guarantee it will find all possible type incompatibilities, only that it may find bugs where all combinations of a type _will_ fail, even in the absence of explicit type annotations. It is meant to be an efficient routine that brings developers some benefits of static typing without requiring any effort from them.
 
 In the long term, Elixir developers who want typing guarantees must explicitly add type signatures to their functions (see "Roadmap"). Any function with an explicit type signature will be typed checked against the user-provided annotations, as in other statically typed languages, without performing type inference. In summary, type checking will rely on type signatures and only fallback to inferred types when no signature is available.