Skip to content

Commit 5120740

Browse files
authored
Clarify and test gradual function application (#15173)
* Implement gradual function domains and tighten function application Add fun_domain/1 to compute function domains for static, dynamic, and mixed function types, including explicit :badfun and {:badarity, ...} outcomes when domain extraction is not well-defined. Refine gradual function application internals by separating static and dynamic normalization paths, documenting behavior for purely dynamic and mixed cases, and clarifying domain/compatibility handling. Expand descr tests with gradual-application edge cases and a dedicated fun_domain test suite covering static, dynamic, mixed, and arity-error scenarios. * Refactor function application and domain handling * Remove fun_domain, recover coverage via fun_apply tests fun_domain was only used in tests; its behavior is fully observable through fun_apply (wrong-domain arg → :badarg, right-domain → :ok). Removed it and converted the domain tests to fun_apply assertions, adding a few previously uncovered cases along the way: pure non-fun badfun, union-arg-type enforcement, 2-arity, mixed-arity badarity for both static and dynamic unions, and the mixed static+dynamic gradual domain case. * Remove dead helpers introduced alongside fun_domain fun_single_arity, fun_single_arity_pair, fun_non_empty_arities_of, and fun_non_empty_arities are now unreachable. Also revert dynamic_fun_top? to the simpler map == %{} check — the semantic emptiness scan added in the refactor was only needed to handle the same edge cases fun_domain was handling. * Move mixed-arity badarity check to static side of fun_normalize_both fun_normalize itself stays simple (no arity cross-check). The check for other non-empty arities now lives in fun_normalize_both via fun_other_non_empty_arities/2, and only fires for the static component. This means: - union(fun/1, fun/2) applied with 1 arg → {:badarity, [1, 2]} (static: we know one branch will always fail at runtime) - union(dynamic_fun/1, dynamic_fun/2) applied with 1 arg → {:ok, dynamic(integer())} (dynamic: picks matching-arity arrows, wraps in dynamic() to reflect that the other branch may fail) * Add tests for mixed-arity union behavior Static union: badarity regardless of which arity is called with, with the called arity listed first followed by the others. Dynamic union: picks the matching-arity arrows and wraps in dynamic(), gives badarity only when no arity matches at all, and falls back to dynamic() when the arg is outside the domain but dynamically compatible.
1 parent 78a5151 commit 5120740

2 files changed

Lines changed: 197 additions & 13 deletions

File tree

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

Lines changed: 120 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1360,15 +1360,16 @@ defmodule Module.Types.Descr do
13601360
13611361
## Function application formula for dynamic types
13621362
1363-
τ◦τ′ = (lower_bound(τ) ◦ upper_bound(τ′)) (dynamic(upper_bound(τ) ◦ lower_bound(τ′)))
1363+
τ◦τ′ = (lower_bound(τ) ◦ upper_bound(τ′)) or (dynamic(upper_bound(τ) ◦ upper_bound(τ′)))
13641364
13651365
Where:
13661366
13671367
- τ is a dynamic function type
13681368
- τ′ are the arguments
13691369
- ◦ is function application
13701370
1371-
For more details, see Definition 6.15 in https://vlanvin.fr/papers/thesis.pdf
1371+
For more details, see Section 13.2 of
1372+
https://gldubc.github.io/assets/duboc-phd-thesis-typing-elixir.pdf
13721373
13731374
## Examples
13741375
@@ -1411,6 +1412,19 @@ defmodule Module.Types.Descr do
14111412
defp dynamic_fun_top?(%{fun: {:negation, map}}), do: map == %{}
14121413
defp dynamic_fun_top?(_), do: false
14131414

1415+
# Gradual function application algorithm.
1416+
#
1417+
# 1. Domain check against the extended gradual domain (see fun_normalize_both/3):
1418+
# - If the argument is a subtype of the domain, proceed to application.
1419+
# - Otherwise, in gradual mode, check compatibility (see below). If
1420+
# compatible, the application may succeed at runtime but we have no
1421+
# static information about the result, so we return dynamic().
1422+
# - Otherwise, error.
1423+
# 2. Compute the application result in three cases:
1424+
# - Fully static: apply static arrows to the arguments directly.
1425+
# - Purely dynamic function (no static arrows): wrap the result of
1426+
# applying dynamic arrows to upper-bounded arguments in dynamic().
1427+
# - Mixed: union the static result with the dynamic-wrapped dynamic result.
14141428
defp fun_apply_with_strategy(fun_static, fun_dynamic, arguments) do
14151429
args_domain = args_to_domain(arguments)
14161430
static? = fun_dynamic == nil and Enum.all?(arguments, fn arg -> not gradual?(arg) end)
@@ -1422,6 +1436,18 @@ defmodule Module.Types.Descr do
14221436
Enum.any?(arguments, &empty?/1) ->
14231437
{:badarg, domain_to_flat_args(domain, arity)}
14241438

1439+
# The domain here is the extended gradual domain computed by
1440+
# fun_normalize_both/3. If the argument does not satisfy it, we
1441+
# check compatibility before rejecting.
1442+
#
1443+
# Compatibility has two cases to avoid a degenerate situation.
1444+
# If the argument is purely dynamic (e.g. dynamic() and bool()),
1445+
# its static part (lower bound) is none(). We do not want
1446+
# none() <= domain to trivially succeed, because that would mean
1447+
# "a diverging argument is accepted by any function", which is true but
1448+
# useless. So when the static part is empty, we instead check
1449+
# that the upper bound overlaps with the domain. When the static
1450+
# part is non-empty, we check it is a subtype of the domain.
14251451
not subtype?(args_domain, domain) ->
14261452
if static? or not compatible?(args_domain, domain),
14271453
do: {:badarg, domain_to_flat_args(domain, arity)},
@@ -1431,12 +1457,27 @@ defmodule Module.Types.Descr do
14311457
{:ok, fun_apply_static(arguments, static_arrows)}
14321458

14331459
static_arrows == [] ->
1434-
# TODO: We need to validate this within the theory
1460+
# Purely dynamic function (e.g. dynamic() and (integer() -> integer())).
1461+
# There are no static arrows, so the general mixed formula simplifies:
1462+
# applying none() to anything yields none(), so the static branch
1463+
# vanishes and only the dynamic branch remains.
1464+
# The result is wrapped in dynamic(), so it is safe regardless of argument precision.
1465+
# If the upper-bounded arguments escape the domain, fun_apply_static returns term(),
1466+
# and dynamic(term()) = dynamic(), which brings back to the compatible case.
14351467
arguments = Enum.map(arguments, &upper_bound/1)
14361468
{:ok, dynamic(fun_apply_static(arguments, dynamic_arrows))}
14371469

14381470
true ->
1439-
# For dynamic cases, combine static and dynamic results
1471+
# Mixed case: union of the static and dynamic results.
1472+
# static_arrows (lower materialization) contain only arrows that are
1473+
# guaranteed to exist at runtime. Static guarantees about the result
1474+
# come from these alone.
1475+
# dynamic_arrows (upper materialization) include dynamically uncertain
1476+
# arrows, so their result is wrapped in dynamic().
1477+
# We use upper_bound on the arguments for both branches. This is sound
1478+
# because the dynamic branch wraps its result in dynamic().
1479+
# It is more strict and informative than using lower_bound in the static part,
1480+
# as it amounts to assuming the worst case of using the statically present arrows.
14401481
arguments = Enum.map(arguments, &upper_bound/1)
14411482

14421483
{:ok,
@@ -1448,22 +1489,57 @@ defmodule Module.Types.Descr do
14481489
end
14491490
end
14501491

1492+
# Normalizes a gradual function type into static and dynamic arrow
1493+
# components, and computes the extended gradual domain.
1494+
#
1495+
# The extended gradual domain is:
1496+
# dom(upper_bound and fun_top) or dynamic(dom(lower_bound))
1497+
#
1498+
# fun_normalize/3 implicitly performs the "and fun_top" projection
1499+
# because it only looks at the :fun component, so any non-function
1500+
# parts of the type are automatically discarded.
1501+
#
1502+
# Fallback cases:
1503+
#
1504+
# - Static normalization succeeds but dynamic fails (e.g. the dynamic
1505+
# part has no arrows at the given arity): we discard the dynamic
1506+
# arrows and use the static arrows for both branches, degenerating
1507+
# to the fully static case. This is sound because ignoring unusable
1508+
# dynamic information cannot produce incorrect static results.
1509+
#
1510+
# - Static normalization fails (:badfun): only the dynamic arrows
1511+
# contribute. The domain becomes dom(upper_bound) or dynamic(),
1512+
# reflecting that the lower bound has no function type at this arity.
1513+
# The application proceeds as purely dynamic (static_arrows = []).
14511514
defp fun_normalize_both(fun_static, fun_dynamic, arity) do
14521515
case fun_normalize(fun_static, arity) do
1453-
{:ok, static_domain, static_arrows} when fun_dynamic == nil ->
1454-
{:ok, static_domain, static_arrows, static_arrows}
1516+
{:ok, static_domain, static_arrows} ->
1517+
# A static function with arrows at other arities is a mixed-arity union:
1518+
# we cannot safely apply it because at runtime the value may have a
1519+
# different arity than the one being called with.
1520+
case fun_other_non_empty_arities(fun_static, arity) do
1521+
[] when fun_dynamic == nil ->
1522+
{:ok, static_domain, static_arrows, static_arrows}
14551523

1456-
{:ok, static_domain, static_arrows} when fun_dynamic != nil ->
1457-
case fun_normalize(fun_dynamic, arity) do
1458-
{:ok, dynamic_domain, dynamic_arrows} ->
1459-
domain = union(dynamic_domain, dynamic(static_domain))
1460-
{:ok, domain, static_arrows, dynamic_arrows}
1524+
[] ->
1525+
case fun_normalize(fun_dynamic, arity) do
1526+
{:ok, dynamic_domain, dynamic_arrows} ->
1527+
domain = union(dynamic_domain, dynamic(static_domain))
1528+
{:ok, domain, static_arrows, dynamic_arrows}
14611529

1462-
_ ->
1463-
{:ok, static_domain, static_arrows, static_arrows}
1530+
_ ->
1531+
# Dynamic normalization failed: fall back to static-only.
1532+
{:ok, static_domain, static_arrows, static_arrows}
1533+
end
1534+
1535+
other ->
1536+
{:badarity, [arity | other]}
14641537
end
14651538

14661539
:badfun ->
1540+
# No static arrows: dynamic-only path. Mixed-arity in the dynamic
1541+
# component is fine — we pick the matching-arity arrows and the
1542+
# result is wrapped in dynamic(), reflecting the uncertainty.
14671543
case fun_normalize(fun_dynamic, arity) do
14681544
{:ok, dynamic_domain, dynamic_arrows} ->
14691545
{:ok, union(dynamic_domain, dynamic()), [], dynamic_arrows}
@@ -1477,6 +1553,20 @@ defmodule Module.Types.Descr do
14771553
end
14781554
end
14791555

1556+
defp fun_other_non_empty_arities(%{fun: {:union, bdds}}, arity) do
1557+
case :maps.take(arity, bdds) do
1558+
{_bdd, rest} ->
1559+
for {a, b} <- rest,
1560+
not Enum.all?(bdd_to_dnf(b), fn {pos, neg} -> fun_line_empty?(pos, neg) end),
1561+
do: a
1562+
1563+
:error ->
1564+
[]
1565+
end
1566+
end
1567+
1568+
defp fun_other_non_empty_arities(_, _), do: []
1569+
14801570
# Transforms a binary decision diagram (BDD) into the canonical `domain-arrows` pair:
14811571
#
14821572
# 1. **domain**: The union of all domains from positive functions in the BDD
@@ -1522,6 +1612,13 @@ defmodule Module.Types.Descr do
15221612

15231613
defp fun_normalize(%{}, _arity), do: :badfun
15241614

1615+
# Applies a static function type to arguments by reducing over the
1616+
# function's DNF clauses. Each clause is an intersection of arrows,
1617+
# processed by aux_apply/4 with rets_reached initialized to term().
1618+
#
1619+
# When the arguments are within the domain, this is the standard
1620+
# application operator. When the arguments escape the domain, the
1621+
# result is term() (see aux_apply/4).
15251622
defp fun_apply_static(arguments, arrows) do
15261623
type_args = args_to_domain(arguments)
15271624

@@ -1554,8 +1651,18 @@ defmodule Module.Types.Descr do
15541651
# - input: The input type being applied to the function
15551652
# - rets_reached: The intersection of return types reached so far
15561653
# - arrow_intersections: The list of function arrows to process
1654+
#
1655+
# Domain escape: if the input is not covered by the union of all the
1656+
# arrow domains in the clause, the result is term(). This is because
1657+
# rets_reached starts at term() and is only refined (intersected) when
1658+
# an arrow's domain covers the input, which is check by dom_subtract.
1659+
# Along a path where no arrow covers the input, rets_reached stays
1660+
# term() and gets unioned into the result at the base case. Since
1661+
# term() is maximal, the overall result for that clause is term().
15571662

15581663
# For more details, see Definitions 2.20 or 6.11 in https://vlanvin.fr/papers/thesis.pdf
1664+
# For the escape case, see Section 13.2 of
1665+
# https://gldubc.github.io/assets/duboc-phd-thesis-typing-elixir.pdf
15591666
defp aux_apply(result, _input, rets_reached, []) do
15601667
if subtype?(rets_reached, result), do: result, else: union(result, rets_reached)
15611668
end

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

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1095,7 +1095,10 @@ defmodule Module.Types.DescrTest do
10951095

10961096
test "non funs" do
10971097
assert fun_apply(term(), [integer()]) == :badfun
1098+
assert fun_apply(integer(), [integer()]) == :badfun
10981099
assert fun_apply(union(integer(), none_fun(1)), [integer()]) == :badfun
1100+
assert fun_apply(union(integer(), fun([integer()], atom())), [integer()]) == :badfun
1101+
assert fun_apply(union(integer(), dynamic()), [integer()]) == :badfun
10991102
end
11001103

11011104
test "static" do
@@ -1108,6 +1111,19 @@ defmodule Module.Types.DescrTest do
11081111
assert fun_apply(fun([integer()], atom()), [float()]) == {:badarg, [integer()]}
11091112
assert fun_apply(fun([integer()], atom()), [term()]) == {:badarg, [integer()]}
11101113

1114+
# Union argument type: domain is int | float
1115+
assert fun_apply(fun([union(integer(), float())], atom()), [integer()]) == {:ok, atom()}
1116+
assert fun_apply(fun([union(integer(), float())], atom()), [float()]) == {:ok, atom()}
1117+
1118+
assert fun_apply(fun([union(integer(), float())], atom()), [atom()]) ==
1119+
{:badarg, [union(integer(), float())]}
1120+
1121+
# 2-arity function
1122+
assert fun_apply(fun([integer(), atom()], binary()), [integer(), atom()]) == {:ok, binary()}
1123+
1124+
assert fun_apply(fun([integer(), atom()], binary()), [boolean(), atom()]) ==
1125+
{:badarg, [integer(), atom()]}
1126+
11111127
# Return types
11121128
assert fun_apply(fun([integer()], none()), [integer()]) == {:ok, none()}
11131129
assert fun_apply(fun([integer()], term()), [integer()]) == {:ok, term()}
@@ -1126,6 +1142,11 @@ defmodule Module.Types.DescrTest do
11261142
assert fun_apply(fun([integer()], integer()), [term(), term()]) == {:badarity, [1]}
11271143
assert fun_apply(fun([integer(), atom()], boolean()), [integer()]) == {:badarity, [2]}
11281144

1145+
# Union of two different arities: always badarity regardless of which arity is called
1146+
fun_mixed = union(fun([integer()], integer()), fun([integer(), atom()], boolean()))
1147+
assert fun_apply(fun_mixed, [integer()]) == {:badarity, [1, 2]}
1148+
assert fun_apply(fun_mixed, [integer(), atom()]) == {:badarity, [2, 1]}
1149+
11291150
# Function intersection tests (no overlap)
11301151
fun0 = intersection(fun([integer()], atom()), fun([float()], binary()))
11311152
assert fun_apply(fun0, [integer()]) == {:ok, atom()}
@@ -1209,6 +1230,20 @@ defmodule Module.Types.DescrTest do
12091230
assert fun_apply(dynamic_fun([integer(), atom()], boolean()), [integer()]) ==
12101231
{:badarity, [2]}
12111232

1233+
# Union of two dynamic functions with different arities: the call may succeed,
1234+
# so we pick the matching-arity arrows and wrap in dynamic().
1235+
fun_dyn_mixed =
1236+
union(dynamic_fun([integer()], integer()), dynamic_fun([integer(), atom()], boolean()))
1237+
1238+
# picks arity-1 arrows → dynamic(integer())
1239+
assert fun_apply(fun_dyn_mixed, [integer()]) == {:ok, dynamic(integer())}
1240+
# picks arity-2 arrows → dynamic(boolean())
1241+
assert fun_apply(fun_dyn_mixed, [integer(), atom()]) == {:ok, dynamic(boolean())}
1242+
# no matching arity → badarity (no dynamic escape here)
1243+
assert fun_apply(fun_dyn_mixed, [integer(), atom(), float()]) == {:badarity, [1, 2]}
1244+
# arg outside arity-1 domain but dynamic-compatible → dynamic()
1245+
assert fun_apply(fun_dyn_mixed, [atom()]) == {:ok, dynamic()}
1246+
12121247
# Function intersection tests
12131248
fun0 = intersection(dynamic_fun([integer()], atom()), dynamic_fun([float()], binary()))
12141249
assert fun_apply(fun0, [integer()]) == {:ok, dynamic(atom())}
@@ -1252,6 +1287,23 @@ defmodule Module.Types.DescrTest do
12521287
)
12531288

12541289
assert fun_apply(fun3, [atom([:ok])]) == {:ok, dynamic(none())}
1290+
1291+
# Testing the special case of uplifiting both the function and argument
1292+
# when the function is purely dynamic
1293+
fun4 =
1294+
intersection(
1295+
dynamic_fun([integer()], integer()),
1296+
dynamic_fun([boolean()], boolean())
1297+
)
1298+
1299+
# dynamic(int->int and bool->bool) applied to dynamic(int)
1300+
assert fun_apply(fun4, [dynamic(integer())]) == {:ok, dynamic(integer())}
1301+
1302+
# float escapes the domain so the result is dynamic()
1303+
arg = dynamic(union(integer(), float()))
1304+
assert fun_apply(fun4, [arg]) == {:ok, dynamic()}
1305+
1306+
assert fun_apply(dynamic(), [integer()]) == {:ok, dynamic()}
12551307
end
12561308

12571309
test "static and dynamic" do
@@ -1279,6 +1331,14 @@ defmodule Module.Types.DescrTest do
12791331
assert fun_args |> fun_apply([atom()]) == {:ok, dynamic()}
12801332
assert fun_args |> fun_apply([integer()]) == {:badarg, [dynamic(atom())]}
12811333

1334+
# ((bool->bool) or dyn(int->int))
1335+
# booleans work, but not integers
1336+
fun_mixed_gdom = union(fun([boolean()], boolean()), dynamic_fun([integer()], integer()))
1337+
assert fun_apply(fun_mixed_gdom, [boolean()]) == {:ok, dynamic()}
1338+
assert fun_apply(fun_mixed_gdom, [dynamic(boolean())]) == {:ok, union(dynamic(), boolean())}
1339+
assert fun_apply(fun_mixed_gdom, [integer()]) == {:badarg, [dynamic(boolean())]}
1340+
assert fun_apply(fun_mixed_gdom, [dynamic(integer())]) == {:badarg, [dynamic(boolean())]}
1341+
12821342
# Badfun
12831343
assert union(
12841344
fun([atom()], integer()),
@@ -1293,6 +1353,23 @@ defmodule Module.Types.DescrTest do
12931353
dynamic_fun([integer()], binary())
12941354
)
12951355
|> fun_apply([integer()]) == {:ok, dynamic(binary())}
1356+
1357+
# Applying (dynamic or int) -> bool to (dynamic and float).
1358+
# The domain is
1359+
# gdom((dynamic or int) -> bool) = dom(int -> bool) or dynamic and dom(term -> bool)
1360+
# = int or dynamic and term = int or dynamic
1361+
1362+
# The domain check dynamic and float <= int or dynamic succeeds.
1363+
# The static application (term -> bool) o float = bool is well-defined.
1364+
# The dynamic application (int -> bool) o float is not well-defined (float not <: int),
1365+
# but since it is dynamic it returns term wrapped in dynamic, which is dynamic.
1366+
# Result: bool or dynamic.
1367+
fun_type = fun([union(dynamic(), integer())], boolean())
1368+
arg = dynamic(float())
1369+
1370+
# Application yields bool or dynamic
1371+
assert {:ok, result} = fun_apply(fun_type, [arg])
1372+
assert equal?(union(boolean(), dynamic()), result)
12961373
end
12971374
end
12981375

0 commit comments

Comments
 (0)