Skip to content

Commit ce2210c

Browse files
authored
Add compatibility relation for gradual typechecking (#13407)
1 parent 5c2e3cf commit ce2210c

File tree

3 files changed

+58
-3
lines changed

3 files changed

+58
-3
lines changed

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

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -291,6 +291,38 @@ defmodule Module.Types.Descr do
291291
"""
292292
def equal?(left, right), do: subtype?(left, right) and subtype?(right, left)
293293

294+
@doc """
295+
Check if two types have a non-empty intersection.
296+
"""
297+
def intersect?(left, right), do: not empty?(intersection(left, right))
298+
299+
@doc """
300+
Checks if a type is a compatible subtype of another.
301+
302+
If `input_type` has a static part (i.e., values that are known to appear and
303+
need to be handled), then to be compatible it should be a subtype of the
304+
the dynamic part of `expected_type` (that is, the largest allowed type at
305+
runtime).
306+
307+
If `input_type` is a dynamic type, then we check that the two can intersect
308+
at runtime, i.e. it is possible to get valid inputs at runtime.
309+
310+
The function is used, in gradual mode, to type an operator that expects a given
311+
type. For instance, `+` expects `integer() or float()` inputs. Compatible inputs
312+
include `dynamic()`, `integer()`, but also `dynamic() and (integer() or atom())`.
313+
Incompatible subtypes include `integer() or list()`, `dynamic() and atom()`.
314+
"""
315+
def compatible?(input_type, expected_type) do
316+
{input_dynamic, input_static} = Map.pop(input_type, :dynamic, input_type)
317+
expected_dynamic = Map.get(expected_type, :dynamic, expected_type)
318+
319+
if not empty?(input_static) do
320+
subtype_static(input_static, expected_dynamic)
321+
else
322+
intersect?(input_dynamic, expected_dynamic)
323+
end
324+
end
325+
294326
## Bitmaps
295327

296328
defp bitmap_union(v1, v2), do: v1 ||| v2

lib/elixir/lib/module/types/of.ex

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -114,9 +114,7 @@ defmodule Module.Types.Of do
114114
# will already have checked the type, so we skip the check here
115115
# as an optimization.
116116
# TODO: properly handle dynamic. Do we need materialization?
117-
if actual_type == dynamic() or
118-
(kind == :pattern and is_var(left)) or
119-
empty?(difference(actual_type, expected_type)) do
117+
if (kind == :pattern and is_var(left)) or compatible?(actual_type, expected_type) do
120118
{:ok, context}
121119
else
122120
hints = if meta[:inferred_bitstring_spec], do: [:inferred_bitstring_spec], else: []

lib/elixir/test/elixir/module/types/descr_test.exs

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -147,6 +147,31 @@ defmodule Module.Types.DescrTest do
147147
end
148148
end
149149

150+
describe "compatible" do
151+
test "intersection" do
152+
assert compatible?(integer(), intersection(dynamic(), integer()))
153+
refute compatible?(intersection(dynamic(), integer()), atom())
154+
refute compatible?(atom(), intersection(dynamic(), integer()))
155+
refute compatible?(atom(), intersection(dynamic(), atom([:foo, :bar])))
156+
assert compatible?(intersection(dynamic(), atom()), atom([:foo, :bar]))
157+
assert compatible?(atom([:foo, :bar]), intersection(dynamic(), atom()))
158+
end
159+
160+
test "static" do
161+
refute compatible?(atom(), atom([:foo, :bar]))
162+
refute compatible?(union(integer(), atom()), integer())
163+
refute compatible?(none(), integer())
164+
refute compatible?(union(atom(), dynamic()), integer())
165+
end
166+
167+
test "dynamic" do
168+
assert compatible?(dynamic(), term())
169+
assert compatible?(term(), dynamic())
170+
assert compatible?(dynamic(), integer())
171+
assert compatible?(integer(), dynamic())
172+
end
173+
end
174+
150175
describe "to_quoted" do
151176
test "bitmap" do
152177
assert union(integer(), union(float(), binary())) |> to_quoted_string() ==

0 commit comments

Comments
 (0)