Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
133 changes: 120 additions & 13 deletions lib/elixir/lib/module/types/descr.ex
Original file line number Diff line number Diff line change
Expand Up @@ -1294,15 +1294,16 @@ defmodule Module.Types.Descr do

## Function application formula for dynamic types

τ◦τ′ = (lower_bound(τ) ◦ upper_bound(τ′)) (dynamic(upper_bound(τ) ◦ lower_bound(τ′)))
τ◦τ′ = (lower_bound(τ) ◦ upper_bound(τ′)) or (dynamic(upper_bound(τ) ◦ upper_bound(τ′)))

Where:

- τ is a dynamic function type
- τ′ are the arguments
- ◦ is function application

For more details, see Definition 6.15 in https://vlanvin.fr/papers/thesis.pdf
For more details, see Section 13.2 of
https://gldubc.github.io/assets/duboc-phd-thesis-typing-elixir.pdf

## Examples

Expand Down Expand Up @@ -1345,6 +1346,19 @@ defmodule Module.Types.Descr do
defp dynamic_fun_top?(%{fun: {:negation, map}}), do: map == %{}
defp dynamic_fun_top?(_), do: false

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

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

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

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

{:ok,
Expand All @@ -1382,22 +1423,57 @@ defmodule Module.Types.Descr do
end
end

# Normalizes a gradual function type into static and dynamic arrow
# components, and computes the extended gradual domain.
#
# The extended gradual domain is:
# dom(upper_bound and fun_top) or dynamic(dom(lower_bound))
#
# fun_normalize/3 implicitly performs the "and fun_top" projection
# because it only looks at the :fun component, so any non-function
# parts of the type are automatically discarded.
#
# Fallback cases:
#
# - Static normalization succeeds but dynamic fails (e.g. the dynamic
# part has no arrows at the given arity): we discard the dynamic
# arrows and use the static arrows for both branches, degenerating
# to the fully static case. This is sound because ignoring unusable
# dynamic information cannot produce incorrect static results.
#
# - Static normalization fails (:badfun): only the dynamic arrows
# contribute. The domain becomes dom(upper_bound) or dynamic(),
# reflecting that the lower bound has no function type at this arity.
# The application proceeds as purely dynamic (static_arrows = []).
defp fun_normalize_both(fun_static, fun_dynamic, arity) do
case fun_normalize(fun_static, arity) do
{:ok, static_domain, static_arrows} when fun_dynamic == nil ->
{:ok, static_domain, static_arrows, static_arrows}
{:ok, static_domain, static_arrows} ->
# A static function with arrows at other arities is a mixed-arity union:
# we cannot safely apply it because at runtime the value may have a
# different arity than the one being called with.
case fun_other_non_empty_arities(fun_static, arity) do
[] when fun_dynamic == nil ->
{:ok, static_domain, static_arrows, static_arrows}

{:ok, static_domain, static_arrows} when fun_dynamic != nil ->
case fun_normalize(fun_dynamic, arity) do
{:ok, dynamic_domain, dynamic_arrows} ->
domain = union(dynamic_domain, dynamic(static_domain))
{:ok, domain, static_arrows, dynamic_arrows}
[] ->
case fun_normalize(fun_dynamic, arity) do
{:ok, dynamic_domain, dynamic_arrows} ->
domain = union(dynamic_domain, dynamic(static_domain))
{:ok, domain, static_arrows, dynamic_arrows}

_ ->
{:ok, static_domain, static_arrows, static_arrows}
_ ->
# Dynamic normalization failed: fall back to static-only.
{:ok, static_domain, static_arrows, static_arrows}
end

other ->
{:badarity, [arity | other]}
end

:badfun ->
# No static arrows: dynamic-only path. Mixed-arity in the dynamic
# component is fine — we pick the matching-arity arrows and the
# result is wrapped in dynamic(), reflecting the uncertainty.
case fun_normalize(fun_dynamic, arity) do
{:ok, dynamic_domain, dynamic_arrows} ->
{:ok, union(dynamic_domain, dynamic()), [], dynamic_arrows}
Expand All @@ -1411,6 +1487,20 @@ defmodule Module.Types.Descr do
end
end

defp fun_other_non_empty_arities(%{fun: {:union, bdds}}, arity) do
case :maps.take(arity, bdds) do
{_bdd, rest} ->
for {a, b} <- rest,
not Enum.all?(bdd_to_dnf(b), fn {pos, neg} -> fun_line_empty?(pos, neg) end),
do: a

:error ->
[]
end
end

defp fun_other_non_empty_arities(_, _), do: []

# Transforms a binary decision diagram (BDD) into the canonical `domain-arrows` pair:
#
# 1. **domain**: The union of all domains from positive functions in the BDD
Expand Down Expand Up @@ -1456,6 +1546,13 @@ defmodule Module.Types.Descr do

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

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

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

# For more details, see Definitions 2.20 or 6.11 in https://vlanvin.fr/papers/thesis.pdf
# For the escape case, see Section 13.2 of
# https://gldubc.github.io/assets/duboc-phd-thesis-typing-elixir.pdf
defp aux_apply(result, _input, rets_reached, []) do
if subtype?(rets_reached, result), do: result, else: union(result, rets_reached)
end
Expand Down
77 changes: 77 additions & 0 deletions lib/elixir/test/elixir/module/types/descr_test.exs
Original file line number Diff line number Diff line change
Expand Up @@ -1057,7 +1057,10 @@ defmodule Module.Types.DescrTest do

test "non funs" do
assert fun_apply(term(), [integer()]) == :badfun
assert fun_apply(integer(), [integer()]) == :badfun
assert fun_apply(union(integer(), none_fun(1)), [integer()]) == :badfun
assert fun_apply(union(integer(), fun([integer()], atom())), [integer()]) == :badfun
assert fun_apply(union(integer(), dynamic()), [integer()]) == :badfun
end

test "static" do
Expand All @@ -1070,6 +1073,19 @@ defmodule Module.Types.DescrTest do
assert fun_apply(fun([integer()], atom()), [float()]) == {:badarg, [integer()]}
assert fun_apply(fun([integer()], atom()), [term()]) == {:badarg, [integer()]}

# Union argument type: domain is int | float
assert fun_apply(fun([union(integer(), float())], atom()), [integer()]) == {:ok, atom()}
assert fun_apply(fun([union(integer(), float())], atom()), [float()]) == {:ok, atom()}

assert fun_apply(fun([union(integer(), float())], atom()), [atom()]) ==
{:badarg, [union(integer(), float())]}

# 2-arity function
assert fun_apply(fun([integer(), atom()], binary()), [integer(), atom()]) == {:ok, binary()}

assert fun_apply(fun([integer(), atom()], binary()), [boolean(), atom()]) ==
{:badarg, [integer(), atom()]}

# Return types
assert fun_apply(fun([integer()], none()), [integer()]) == {:ok, none()}
assert fun_apply(fun([integer()], term()), [integer()]) == {:ok, term()}
Expand All @@ -1088,6 +1104,11 @@ defmodule Module.Types.DescrTest do
assert fun_apply(fun([integer()], integer()), [term(), term()]) == {:badarity, [1]}
assert fun_apply(fun([integer(), atom()], boolean()), [integer()]) == {:badarity, [2]}

# Union of two different arities: always badarity regardless of which arity is called
fun_mixed = union(fun([integer()], integer()), fun([integer(), atom()], boolean()))
assert fun_apply(fun_mixed, [integer()]) == {:badarity, [1, 2]}
assert fun_apply(fun_mixed, [integer(), atom()]) == {:badarity, [2, 1]}

# Function intersection tests (no overlap)
fun0 = intersection(fun([integer()], atom()), fun([float()], binary()))
assert fun_apply(fun0, [integer()]) == {:ok, atom()}
Expand Down Expand Up @@ -1171,6 +1192,20 @@ defmodule Module.Types.DescrTest do
assert fun_apply(dynamic_fun([integer(), atom()], boolean()), [integer()]) ==
{:badarity, [2]}

# Union of two dynamic functions with different arities: the call may succeed,
# so we pick the matching-arity arrows and wrap in dynamic().
fun_dyn_mixed =
union(dynamic_fun([integer()], integer()), dynamic_fun([integer(), atom()], boolean()))

# picks arity-1 arrows → dynamic(integer())
assert fun_apply(fun_dyn_mixed, [integer()]) == {:ok, dynamic(integer())}
# picks arity-2 arrows → dynamic(boolean())
assert fun_apply(fun_dyn_mixed, [integer(), atom()]) == {:ok, dynamic(boolean())}
# no matching arity → badarity (no dynamic escape here)
assert fun_apply(fun_dyn_mixed, [integer(), atom(), float()]) == {:badarity, [1, 2]}
# arg outside arity-1 domain but dynamic-compatible → dynamic()
assert fun_apply(fun_dyn_mixed, [atom()]) == {:ok, dynamic()}

# Function intersection tests
fun0 = intersection(dynamic_fun([integer()], atom()), dynamic_fun([float()], binary()))
assert fun_apply(fun0, [integer()]) == {:ok, dynamic(atom())}
Expand Down Expand Up @@ -1214,6 +1249,23 @@ defmodule Module.Types.DescrTest do
)

assert fun_apply(fun3, [atom([:ok])]) == {:ok, dynamic(none())}

# Testing the special case of uplifiting both the function and argument
# when the function is purely dynamic
fun4 =
intersection(
dynamic_fun([integer()], integer()),
dynamic_fun([boolean()], boolean())
)

# dynamic(int->int and bool->bool) applied to dynamic(int)
assert fun_apply(fun4, [dynamic(integer())]) == {:ok, dynamic(integer())}

# float escapes the domain so the result is dynamic()
arg = dynamic(union(integer(), float()))
assert fun_apply(fun4, [arg]) == {:ok, dynamic()}

assert fun_apply(dynamic(), [integer()]) == {:ok, dynamic()}
end

test "static and dynamic" do
Expand Down Expand Up @@ -1241,6 +1293,14 @@ defmodule Module.Types.DescrTest do
assert fun_args |> fun_apply([atom()]) == {:ok, dynamic()}
assert fun_args |> fun_apply([integer()]) == {:badarg, [dynamic(atom())]}

# ((bool->bool) or dyn(int->int))
# booleans work, but not integers
fun_mixed_gdom = union(fun([boolean()], boolean()), dynamic_fun([integer()], integer()))
assert fun_apply(fun_mixed_gdom, [boolean()]) == {:ok, dynamic()}
assert fun_apply(fun_mixed_gdom, [dynamic(boolean())]) == {:ok, union(dynamic(), boolean())}
assert fun_apply(fun_mixed_gdom, [integer()]) == {:badarg, [dynamic(boolean())]}
assert fun_apply(fun_mixed_gdom, [dynamic(integer())]) == {:badarg, [dynamic(boolean())]}

# Badfun
assert union(
fun([atom()], integer()),
Expand All @@ -1255,6 +1315,23 @@ defmodule Module.Types.DescrTest do
dynamic_fun([integer()], binary())
)
|> fun_apply([integer()]) == {:ok, dynamic(binary())}

# Applying (dynamic or int) -> bool to (dynamic and float).
# The domain is
# gdom((dynamic or int) -> bool) = dom(int -> bool) or dynamic and dom(term -> bool)
# = int or dynamic and term = int or dynamic

# The domain check dynamic and float <= int or dynamic succeeds.
# The static application (term -> bool) o float = bool is well-defined.
# The dynamic application (int -> bool) o float is not well-defined (float not <: int),
# but since it is dynamic it returns term wrapped in dynamic, which is dynamic.
# Result: bool or dynamic.
fun_type = fun([union(dynamic(), integer())], boolean())
arg = dynamic(float())

# Application yields bool or dynamic
assert {:ok, result} = fun_apply(fun_type, [arg])
assert equal?(union(boolean(), dynamic()), result)
end
end

Expand Down