@@ -46,8 +46,8 @@ defmodule Module.Types.Descr do
4646  @ not_non_empty_list  Map . delete ( @ term ,  :list ) 
4747  @ not_list  Map . replace! ( @ not_non_empty_list ,  :bitmap ,  @ bit_top  -  @ bit_empty_list ) 
4848
49-   @ empty_intersection  [ 0 ,  @ none ,  [ ] ] 
50-   @ empty_difference  [ 0 ,  [ ] ] 
49+   @ empty_intersection  [ 0 ,  @ none ,  [ ] ,   :fun_bottom ] 
50+   @ empty_difference  [ 0 ,  [ ] ,   :fun_bottom ] 
5151
5252  defguard  is_descr ( descr )  when  is_map ( descr )  or  descr  ==  :term 
5353
@@ -135,16 +135,17 @@ defmodule Module.Types.Descr do
135135  @ doc  """ 
136136  Creates a function from overlapping function clauses. 
137137  """ 
138-   def  fun_from_overlapping_clauses ( args_clauses )  do 
138+   def  fun_from_inferred_clauses ( args_clauses )  do 
139139    domain_clauses  = 
140140      Enum . reduce ( args_clauses ,  [ ] ,  fn  { args ,  return } ,  acc  -> 
141-         pivot_overlapping_clause ( args_to_domain ( args ) ,  return ,  acc ) 
141+         domain  =  args  |>  Enum . map ( & upper_bound / 1 )  |>  args_to_domain ( ) 
142+         pivot_overlapping_clause ( domain ,  upper_bound ( return ) ,  acc ) 
142143      end ) 
143144
144145    funs  = 
145146      for  { domain ,  return }  <-  domain_clauses , 
146147          args  <-  domain_to_args ( domain ) , 
147-           do:  fun ( args ,  return ) 
148+           do:  fun ( args ,  dynamic ( return ) ) 
148149
149150    Enum . reduce ( funs ,  & intersection / 2 ) 
150151  end 
@@ -198,19 +199,19 @@ defmodule Module.Types.Descr do
198199  def  domain_to_args ( descr )  do 
199200    case  :maps . take ( :dynamic ,  descr )  do 
200201      :error  -> 
201-         tuple_elim_negations_static ( descr ,  & Function . identity / 1 ) 
202+         unwrap_domain_tuple ( descr ,  fn   { :closed ,   elems }   ->   elems   end ) 
202203
203204      { dynamic ,  static }  -> 
204-         tuple_elim_negations_static ( static ,  & Function . identity / 1 )  ++ 
205-           tuple_elim_negations_static ( dynamic ,  fn  elems  ->  Enum . map ( elems ,  & dynamic / 1 )  end ) 
205+         unwrap_domain_tuple ( static ,  fn   { :closed ,   elems }   ->   elems   end )  ++ 
206+           unwrap_domain_tuple ( dynamic ,  fn  { :closed ,   elems }  ->  Enum . map ( elems ,  & dynamic / 1 )  end ) 
206207    end 
207208  end 
208209
209-   defp  tuple_elim_negations_static ( % { tuple:  dnf }  =  descr ,  transform )  when  map_size ( descr )  ==  1  do 
210-     Enum . map ( dnf ,  fn   { :closed ,   elements }   ->   transform . ( elements )   end ) 
210+   defp  unwrap_domain_tuple ( % { tuple:  dnf }  =  descr ,  transform )  when  map_size ( descr )  ==  1  do 
211+     Enum . map ( dnf ,  transform ) 
211212  end 
212213
213-   defp  tuple_elim_negations_static ( descr ,  _transform )  when  descr  ==  % { } ,  do:  [ ] 
214+   defp  unwrap_domain_tuple ( descr ,  _transform )  when  descr  ==  % { } ,  do:  [ ] 
214215
215216  defp  domain_to_flat_args ( domain ,  arity )  do 
216217    case  domain_to_args ( domain )  do 
@@ -1173,6 +1174,7 @@ defmodule Module.Types.Descr do
11731174
11741175        static_arrows  ==  [ ]  -> 
11751176          # TODO: We need to validate this within the theory 
1177+           arguments  =  Enum . map ( arguments ,  & upper_bound / 1 ) 
11761178          { :ok ,  dynamic ( fun_apply_static ( arguments ,  dynamic_arrows ,  false ) ) } 
11771179
11781180        true  -> 
@@ -1327,9 +1329,9 @@ defmodule Module.Types.Descr do
13271329    if  subtype? ( rets_reached ,  result ) ,  do:  result ,  else:  union ( result ,  rets_reached ) 
13281330  end 
13291331
1330-   defp  aux_apply ( result ,  input ,  returns_reached ,  [ { dom ,  ret }  |  arrow_intersections ] )  do 
1332+   defp  aux_apply ( result ,  input ,  returns_reached ,  [ { args ,  ret }  |  arrow_intersections ] )  do 
13311333    # Calculate the part of the input not covered by this arrow's domain 
1332-     dom_subtract  =  difference ( input ,  args_to_domain ( dom ) ) 
1334+     dom_subtract  =  difference ( input ,  args_to_domain ( args ) ) 
13331335
13341336    # Refine the return type by intersecting with this arrow's return type 
13351337    ret_refine  =  intersection ( returns_reached ,  ret ) 
@@ -1426,7 +1428,7 @@ defmodule Module.Types.Descr do
14261428          # determines emptiness. 
14271429          length ( neg_arguments )  ==  positive_arity  and 
14281430            subtype? ( args_to_domain ( neg_arguments ) ,  positive_domain )  and 
1429-             phi_starter ( neg_arguments ,  negation ( neg_return ) ,  positives ) 
1431+             phi_starter ( neg_arguments ,  neg_return ,  positives ) 
14301432        end ) 
14311433    end 
14321434  end 
@@ -1464,27 +1466,75 @@ defmodule Module.Types.Descr do
14641466  # 
14651467  # See [Castagna and Lanvin (2024)](https://arxiv.org/abs/2408.14345), Theorem 4.2. 
14661468  defp  phi_starter ( arguments ,  return ,  positives )  do 
1467-     n  =  length ( arguments ) 
1468-     # Arity mismatch: if there is one positive function with a different arity, 
1469-     # then it cannot be a subtype of the (arguments->type) functions. 
1470-     if  Enum . any? ( positives ,  fn  { args ,  _ret }  ->  length ( args )  !=  n  end )  do 
1471-       false 
1469+     # Optimization: When all positive functions have non-empty domains, 
1470+     # we can simplify the phi function check to a direct subtyping test. 
1471+     # This avoids the expensive recursive phi computation by checking only that applying the 
1472+     # input to the positive intersection yields a subtype of the return 
1473+     if  all_non_empty_domains? ( [ { arguments ,  return }  |  positives ] )  do 
1474+       fun_apply_static ( arguments ,  [ positives ] ,  false ) 
1475+       |>  subtype? ( return ) 
14721476    else 
1473-       arguments  =  Enum . map ( arguments ,  & { false ,  & 1 } ) 
1474-       phi ( arguments ,  { false ,  return } ,  positives ) 
1477+       n  =  length ( arguments ) 
1478+       # Arity mismatch: functions with different arities cannot be subtypes 
1479+       # of the target function type (arguments -> return) 
1480+       if  Enum . any? ( positives ,  fn  { args ,  _ret }  ->  length ( args )  !=  n  end )  do 
1481+         false 
1482+       else 
1483+         # Initialize memoization cache for the recursive phi computation 
1484+         arguments  =  Enum . map ( arguments ,  & { false ,  & 1 } ) 
1485+         { result ,  _cache }  =  phi ( arguments ,  { false ,  negation ( return ) } ,  positives ,  % { } ) 
1486+         result 
1487+       end 
14751488    end 
14761489  end 
14771490
1478-   defp  phi ( args ,  { b ,  t } ,  [ ] )  do 
1479-     Enum . any? ( args ,  fn  { bool ,  typ }  ->  bool  and  empty? ( typ )  end )  or  ( b  and  empty? ( t ) ) 
1491+   defp  phi ( args ,  { b ,  t } ,  [ ] ,   cache )  do 
1492+     { Enum . any? ( args ,  fn  { bool ,  typ }  ->  bool  and  empty? ( typ )  end )  or  ( b  and  empty? ( t ) ) ,   cache } 
14801493  end 
14811494
1482-   defp  phi ( args ,  { b ,  ret } ,  [ { arguments ,  return }  |  rest_positive ] )  do 
1483-     phi ( args ,  { true ,  intersection ( ret ,  return ) } ,  rest_positive )  and 
1484-       Enum . all? ( Enum . with_index ( arguments ) ,  fn  { type ,  index }  -> 
1485-         List . update_at ( args ,  index ,  fn  { _ ,  arg }  ->  { true ,  difference ( arg ,  type ) }  end ) 
1486-         |>  phi ( { b ,  ret } ,  rest_positive ) 
1487-       end ) 
1495+   defp  phi ( args ,  { b ,  ret } ,  [ { arguments ,  return }  |  rest_positive ] ,  cache )  do 
1496+     # Create cache key from function arguments 
1497+     cache_key  =  { args ,  { b ,  ret } ,  [ { arguments ,  return }  |  rest_positive ] } 
1498+ 
1499+     case  Map . get ( cache ,  cache_key )  do 
1500+       nil  -> 
1501+         # Compute result and cache it 
1502+         { result1 ,  cache }  =  phi ( args ,  { true ,  intersection ( ret ,  return ) } ,  rest_positive ,  cache ) 
1503+ 
1504+         if  not  result1  do 
1505+           # Store false result in cache 
1506+           cache  =  Map . put ( cache ,  cache_key ,  false ) 
1507+           { false ,  cache } 
1508+         else 
1509+           # This doesn't stop if one intermediate result is false? 
1510+           { result2 ,  cache }  = 
1511+             Enum . with_index ( arguments ) 
1512+             |>  Enum . reduce_while ( { true ,  cache } ,  fn  { type ,  index } ,  { acc_result ,  acc_cache }  -> 
1513+               { new_result ,  new_cache }  = 
1514+                 List . update_at ( args ,  index ,  fn  { _ ,  arg }  ->  { true ,  difference ( arg ,  type ) }  end ) 
1515+                 |>  phi ( { b ,  ret } ,  rest_positive ,  acc_cache ) 
1516+ 
1517+               if  new_result  do 
1518+                 { :cont ,  { acc_result  and  new_result ,  new_cache } } 
1519+               else 
1520+                 { :halt ,  { false ,  new_cache } } 
1521+               end 
1522+             end ) 
1523+ 
1524+           result  =  result1  and  result2 
1525+           # Store result in cache 
1526+           cache  =  Map . put ( cache ,  cache_key ,  result ) 
1527+           { result ,  cache } 
1528+         end 
1529+ 
1530+       cached_result  -> 
1531+         # Return cached result 
1532+         { cached_result ,  cache } 
1533+     end 
1534+   end 
1535+ 
1536+   defp  all_non_empty_domains? ( positives )  do 
1537+     Enum . all? ( positives ,  fn  { args ,  _ret }  ->  not  empty? ( args_to_domain ( args ) )  end ) 
14881538  end 
14891539
14901540  defp  fun_union ( bdd1 ,  bdd2 )  do 
@@ -1831,6 +1881,10 @@ defmodule Module.Types.Descr do
18311881  #    b) If only the last type differs, subtracts it 
18321882  # 3. Base case: adds dnf2 type to negations of dnf1 type 
18331883  # The result may be larger than the initial dnf1, which is maintained in the accumulator. 
1884+   defp  list_difference ( _ ,  dnf )  when  dnf  ==  @ non_empty_list_top  do 
1885+     0 
1886+   end 
1887+ 
18341888  defp  list_difference ( dnf1 ,  dnf2 )  do 
18351889    Enum . reduce ( dnf2 ,  dnf1 ,  fn  { t2 ,  last2 ,  negs2 } ,  acc_dnf1  -> 
18361890      last2  =  list_tail_unfold ( last2 ) 
@@ -1858,6 +1912,8 @@ defmodule Module.Types.Descr do
18581912    end ) 
18591913  end 
18601914
1915+   defp  list_empty? ( @ non_empty_list_top ) ,  do:  false 
1916+ 
18611917  defp  list_empty? ( dnf )  do 
18621918    Enum . all? ( dnf ,  fn  { list_type ,  last_type ,  negs }  -> 
18631919      last_type  =  list_tail_unfold ( last_type ) 
@@ -2118,9 +2174,6 @@ defmodule Module.Types.Descr do
21182174
21192175  defp  dynamic_to_quoted ( descr ,  opts )  do 
21202176    cond  do 
2121-       descr  ==  % { }  -> 
2122-         [ ] 
2123- 
21242177      # We check for :term literally instead of using term_type? 
21252178      # because we check for term_type? in to_quoted before we 
21262179      # compute the difference(dynamic, static). 
@@ -2130,6 +2183,9 @@ defmodule Module.Types.Descr do
21302183      single  =  indivisible_bitmap ( descr ,  opts )  -> 
21312184        [ single ] 
21322185
2186+       empty? ( descr )  -> 
2187+         [ ] 
2188+ 
21332189      true  -> 
21342190        case  non_term_type_to_quoted ( descr ,  opts )  do 
21352191          { :none ,  _meta ,  [ ] }  =  none  ->  [ none ] 
@@ -2398,6 +2454,10 @@ defmodule Module.Types.Descr do
23982454    if  empty? ( type ) ,  do:  throw ( :empty ) ,  else:  type 
23992455  end 
24002456
2457+   defp  map_difference ( _ ,  dnf )  when  dnf  ==  @ map_top  do 
2458+     0 
2459+   end 
2460+ 
24012461  defp  map_difference ( dnf1 ,  dnf2 )  do 
24022462    Enum . reduce ( dnf2 ,  dnf1 ,  fn 
24032463      # Optimization: we are removing an open map with one field. 
@@ -3048,10 +3108,15 @@ defmodule Module.Types.Descr do
30483108    zip_non_empty_intersection! ( rest1 ,  rest2 ,  [ non_empty_intersection! ( type1 ,  type2 )  |  acc ] ) 
30493109  end 
30503110
3111+   defp  tuple_difference ( _ ,  dnf )  when  dnf  ==  @ tuple_top  do 
3112+     0 
3113+   end 
3114+ 
30513115  defp  tuple_difference ( dnf1 ,  dnf2 )  do 
30523116    Enum . reduce ( dnf2 ,  dnf1 ,  fn  { tag2 ,  elements2 } ,  dnf1  -> 
30533117      Enum . reduce ( dnf1 ,  [ ] ,  fn  { tag1 ,  elements1 } ,  acc  -> 
3054-         tuple_eliminate_single_negation ( tag1 ,  elements1 ,  { tag2 ,  elements2 } )  ++  acc 
3118+         tuple_eliminate_single_negation ( tag1 ,  elements1 ,  { tag2 ,  elements2 } ) 
3119+         |>  tuple_union ( acc ) 
30553120      end ) 
30563121    end ) 
30573122  end 
@@ -3066,8 +3131,10 @@ defmodule Module.Types.Descr do
30663131    if  ( tag  ==  :closed  and  n  <  m )  or  ( neg_tag  ==  :closed  and  n  >  m )  do 
30673132      [ { tag ,  elements } ] 
30683133    else 
3069-       tuple_elim_content ( [ ] ,  tag ,  elements ,  neg_elements )  ++ 
3134+       tuple_union ( 
3135+         tuple_elim_content ( [ ] ,  tag ,  elements ,  neg_elements ) , 
30703136        tuple_elim_size ( n ,  m ,  tag ,  elements ,  neg_tag ) 
3137+       ) 
30713138    end 
30723139  end 
30733140
0 commit comments