Skip to content

Commit

Permalink
Use dynamic(type) on pretty printing
Browse files Browse the repository at this point in the history
  • Loading branch information
josevalim committed May 5, 2024
1 parent 18ba88c commit 0043b1e
Show file tree
Hide file tree
Showing 5 changed files with 41 additions and 39 deletions.
18 changes: 10 additions & 8 deletions lib/elixir/lib/module/types/descr.ex
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,9 @@ defmodule Module.Types.Descr do

## Set operations

def term_type?(@term), do: true
def term_type?(descr), do: subtype_static(@term, Map.delete(descr, :dynamic))

def gradual?(descr), do: is_map_key(descr, :dynamic)

@doc """
Expand Down Expand Up @@ -212,14 +214,14 @@ defmodule Module.Types.Descr do
@doc """
Converts a descr to its quoted representation.
"""
def to_quoted(@term) do
{:term, [], []}
end

def to_quoted(%{} = descr) do
case Enum.flat_map(descr, fn {key, value} -> to_quoted(key, value) end) do
[] -> {:none, [], []}
unions -> unions |> Enum.sort() |> Enum.reduce(&{:or, [], [&2, &1]})
if term_type?(descr) do
{:term, [], []}
else
case Enum.flat_map(descr, fn {key, value} -> to_quoted(key, value) end) do
[] -> {:none, [], []}
unions -> unions |> Enum.sort() |> Enum.reduce(&{:or, [], [&2, &1]})
end
end
end

Expand Down Expand Up @@ -591,7 +593,7 @@ defmodule Module.Types.Descr do
cond do
term_type?(descr) -> [{:dynamic, [], []}]
single = indivisible_bitmap(descr) -> [single]
true -> [{:and, [], [{:dynamic, [], []}, to_quoted(descr)]}]
true -> [{:dynamic, [], [to_quoted(descr)]}]
end
end

Expand Down
6 changes: 3 additions & 3 deletions lib/elixir/pages/references/gradual-set-theoretic-types.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ This function also has the type `(boolean() -> boolean())`, because it receives

At this point, some may ask, why not a union? As a real-world example, take a t-shirt with green and yellow stripes. We can say the t-shirt belongs to the set of "t-shirts with green color". We can also say the t-shirt belongs to the set of "t-shirts with yellow color". Let's see the difference between unions and intersections:

* `(t_shirts_with_green() or t_shirts_with_yellow())` - contains t-shirts with either green or yellow, such as green, green and red, green and blue, yellow, yellow and red, etc.
* `(t_shirts_with_green() or t_shirts_with_yellow())` - contains t-shirts with either green or yellow, such as green, green and red, green and yellow, yellow, yellow and red, etc.

* `(t_shirts_with_green() and t_shirts_with_yellow())` - contains t-shirts with both green and yellow (and also other colors)

Expand All @@ -62,15 +62,15 @@ The simplest way to reason about `dynamic()` in Elixir is that it is a range of

However, by intersecting any type with `dynamic()`, we make the type gradual and therefore only a subset of the type needs to be valid. For instance, if you call `Integer.to_string(var)`, and `var` has type `dynamic() and (atom() or integer())`, the type system will not emit a warning, because `Integer.to_string/1` works with at least one of the types. This flexibility makes `dynamic()` excellent for typing existing code, because it will only emit warnings once it is certain the code will fail. For convenience, most programs will write `dynamic(atom() or integer())` instead of the intersection. They have the same behaviour.

Once Elixir introduces a type language into its API, Elixir programs will behave as a statically typed language, unless the `dynamic` type is used. This brings us to one last remark about dynamic types in Elixir: dyamic types are always at the root. For example, when you write a tuple of type `{:ok, dynamic()}`, Elixir will rewrite it to `dynamic({:ok, term()})`. While this has the downside that you cannot make part of a tuple/map/list gradual, only the whole tuple/map/list, it comes with the upside that dynamic is always explicitly at the root, making it harder to accidentally sneak `dynamic()` in a statically typed program.
Once Elixir introduces typed function signatures, typed Elixir programs will behave as a statically typed code, unless the `dynamic()` type is used. This brings us to one last remark about dynamic types in Elixir: dyamic types are always at the root. For example, when you write a tuple of type `{:ok, dynamic()}`, Elixir will rewrite it to `dynamic({:ok, term()})`. While this has the downside that you cannot make part of a tuple/map/list gradual, only the whole tuple/map/list, it comes with the upside that dynamic is always explicitly at the root, making it harder to accidentally sneak `dynamic()` in a statically typed program.

## Roadmap

The current milestone is to implement type inference and type checking of Elixir programs without changes to the Elixir language. At this stage, we want to collect feedback on the quality of error messages and performance, and therefore the type system has no user facing API.

If the results are satisfactory, the next milestone will include a mechanism for defining typed structs. Elixir programs frequently pattern match on structs, which reveals information about the struct fields, but it knows nothing about their respective types. By propagating types from structs and their fields throughout the program, we will increase the type system’s ability to find errors while further straining our type system implementation. Proposals including the required changes to the language surface will be sent to the community once we reach this stage.

The third milestone is to introduce the type annotations for functions. Once we conclude this stage, the existing typespecs system will be phased out of the language and moved into a separate library.
The third milestone is to introduce set-theoretic type signatures for functions. Unfortunately, the existing typespecs are not precise enough for set-theoretic types and they will be phased out of the language and moved into a separate library once this stage concludes.

## Acknowledgements

Expand Down
6 changes: 3 additions & 3 deletions lib/elixir/test/elixir/module/types/descr_test.exs
Original file line number Diff line number Diff line change
Expand Up @@ -374,15 +374,15 @@ defmodule Module.Types.DescrTest do
assert intersection(binary(), dynamic()) |> to_quoted_string() == "binary()"

assert intersection(union(binary(), pid()), dynamic()) |> to_quoted_string() ==
"dynamic() and (binary() or pid())"
"dynamic(binary() or pid())"

assert intersection(atom(), dynamic()) |> to_quoted_string() == "dynamic() and atom()"
assert intersection(atom(), dynamic()) |> to_quoted_string() == "dynamic(atom())"

assert union(atom([:foo, :bar]), dynamic()) |> to_quoted_string() ==
"dynamic() or (:bar or :foo)"

assert intersection(dynamic(), closed_map(a: integer())) |> to_quoted_string() ==
"dynamic() and %{a: integer()}"
"dynamic(%{a: integer()})"
end

test "map" do
Expand Down
48 changes: 24 additions & 24 deletions lib/elixir/test/elixir/module/types/expr_test.exs
Original file line number Diff line number Diff line change
Expand Up @@ -229,7 +229,7 @@ defmodule Module.Types.ExprTest do
expected type:
dynamic() and %Point{x: term(), y: term(), z: term()}
dynamic(%Point{x: term(), y: term(), z: term()})
but got type:
Expand Down Expand Up @@ -279,7 +279,7 @@ defmodule Module.Types.ExprTest do
the given type does not have the given key:
dynamic() and %Point{x: nil, y: nil, z: integer()}
dynamic(%Point{x: nil, y: nil, z: integer()})
typing violation found at:\
"""}
Expand All @@ -295,17 +295,16 @@ defmodule Module.Types.ExprTest do
where "x" was given the type:
# type: dynamic() and
%URI{
authority: term(),
fragment: term(),
host: term(),
path: term(),
port: term(),
query: term(),
scheme: term(),
userinfo: term()
}
# type: dynamic(%URI{
authority: term(),
fragment: term(),
host: term(),
path: term(),
port: term(),
query: term(),
scheme: term(),
userinfo: term()
})
# from: types_test.ex:LINE-2
x = %URI{}
Expand Down Expand Up @@ -369,7 +368,7 @@ defmodule Module.Types.ExprTest do
where "y" was given the type:
# type: dynamic() and %Point{x: term(), y: term(), z: term()}
# type: dynamic(%Point{x: term(), y: term(), z: term()})
# from: types_test.ex:LINE-2
y = %Point{}
Expand Down Expand Up @@ -421,16 +420,17 @@ defmodule Module.Types.ExprTest do
where "e" was given the type:
# type: dynamic() and
(%RuntimeError{__exception__: true, message: term()} or
%SyntaxError{
__exception__: true,
column: term(),
description: term(),
file: term(),
line: term(),
snippet: term()
})
# type: dynamic(
%RuntimeError{__exception__: true, message: term()} or
%SyntaxError{
__exception__: true,
column: term(),
description: term(),
file: term(),
line: term(),
snippet: term()
}
)
# from: types_test.ex:LINE-5
e in [SyntaxError, RuntimeError]
Expand Down
2 changes: 1 addition & 1 deletion lib/elixir/test/elixir/module/types/pattern_test.exs
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ defmodule Module.Types.PatternTest do
where "x" was given the type:
# type: dynamic() and %Point{x: term(), y: term(), z: term()}
# type: dynamic(%Point{x: term(), y: term(), z: term()})
# from: types_test.ex:LINE-2
x = %Point{}
Expand Down

0 comments on commit 0043b1e

Please sign in to comment.