@@ -1290,25 +1290,22 @@ defmodule Module.Types.Descr do
12901290 type_args = args_to_domain ( arguments )
12911291
12921292 # Optimization: short-circuits when inner loop is none() or outer loop is term()
1293- result =
1294- if maybe_empty? and empty? ( type_args ) do
1295- Enum . reduce_while ( arrows , none ( ) , fn intersection_of_arrows , acc ->
1296- Enum . reduce_while ( intersection_of_arrows , term ( ) , fn
1297- { _dom , _ret } , acc when acc == @ none -> { :halt , acc }
1298- { _dom , ret } , acc -> { :cont , intersection ( acc , ret ) }
1299- end )
1300- |> case do
1301- :term -> { :halt , :term }
1302- inner -> { :cont , union ( inner , acc ) }
1303- end
1293+ if maybe_empty? and empty? ( type_args ) do
1294+ Enum . reduce_while ( arrows , none ( ) , fn intersection_of_arrows , acc ->
1295+ Enum . reduce_while ( intersection_of_arrows , term ( ) , fn
1296+ { _dom , _ret } , acc when acc == @ none -> { :halt , acc }
1297+ { _dom , ret } , acc -> { :cont , intersection ( acc , ret ) }
13041298 end )
1305- else
1306- Enum . reduce ( arrows , none ( ) , fn intersection_of_arrows , acc ->
1307- aux_apply ( acc , type_args , term ( ) , intersection_of_arrows )
1308- end )
1309- end
1310-
1311- result
1299+ |> case do
1300+ :term -> { :halt , :term }
1301+ inner -> { :cont , union ( inner , acc ) }
1302+ end
1303+ end )
1304+ else
1305+ Enum . reduce ( arrows , none ( ) , fn intersection_of_arrows , acc ->
1306+ aux_apply ( acc , type_args , term ( ) , intersection_of_arrows )
1307+ end )
1308+ end
13121309 end
13131310
13141311 # Helper function for function application that handles the application of
@@ -1465,34 +1462,33 @@ defmodule Module.Types.Descr do
14651462 # Returns true if the intersection of the positives is a subtype of (t1,...,tn)->(not t).
14661463 #
14671464 # See [Castagna and Lanvin (2024)](https://arxiv.org/abs/2408.14345), Theorem 4.2.
1468- defp all_non_empty_domains? ( positives ) do
1469- Enum . all? ( positives , fn { args , _ret } -> not empty? ( args_to_domain ( args ) ) end )
1470- end
1471-
14721465 defp phi_starter ( arguments , return , positives ) do
1473- ### SPECIAL CASE: all the positives (intersection) functions have non-empty arguments
1474- # In that case, checking subtyping of it with a single arrow is simply checking that the union
1475- # of the domains of the positives is a supertype of the domain of the arrow
1476- # and that applying the input type of the arrow to the intersection gives sth that
1477- # is a subtype of the return type of the arrow
1478- if all_non_empty_domains? ( positives ) and all_non_empty_domains? ( [ { arguments , return } ] ) do
1466+ # Optimization: When all positive functions have non-empty domains,
1467+ # we can simplify the phi function check to a direct subtyping test.
1468+ # This avoids the expensive recursive phi computation by checking only that applying the
1469+ # input to the positive intersection yields a subtype of the return
1470+ if all_non_empty_domains? ( [ { arguments , return } | positives ] ) do
14791471 fun_apply_static ( arguments , [ positives ] , false )
14801472 |> subtype? ( return )
14811473 else
14821474 n = length ( arguments )
1483- # Arity mismatch: if there is one positive function with a different arity,
1484- # then it cannot be a subtype of the (arguments->type) functions.
1475+ # Arity mismatch: functions with different arities cannot be subtypes
1476+ # of the target function type (arguments -> return)
14851477 if Enum . any? ( positives , fn { args , _ret } -> length ( args ) != n end ) do
14861478 false
14871479 else
1488- # Initialize memoization cache
1480+ # Initialize memoization cache for the recursive phi computation
14891481 Process . put ( :phi_cache , % { } )
14901482 arguments = Enum . map ( arguments , & { false , & 1 } )
14911483 phi ( arguments , { false , negation ( return ) } , positives )
14921484 end
14931485 end
14941486 end
14951487
1488+ defp all_non_empty_domains? ( positives ) do
1489+ Enum . all? ( positives , fn { args , _ret } -> not empty? ( args_to_domain ( args ) ) end )
1490+ end
1491+
14961492 defp phi ( args , { b , t } , [ ] ) do
14971493 Enum . any? ( args , fn { bool , typ } -> bool and empty? ( typ ) end ) or ( b and empty? ( t ) )
14981494 end
@@ -3798,6 +3794,4 @@ defmodule Module.Types.Descr do
37983794 defp non_empty_map_or ( [ head | tail ] , fun ) do
37993795 Enum . reduce ( tail , fun . ( head ) , & { :or , [ ] , [ & 2 , fun . ( & 1 ) ] } )
38003796 end
3801-
3802- # Performance tracking helpers for aux_apply
38033797end
0 commit comments