@@ -26,7 +26,7 @@ defmodule Module.Types.Descr do
2626  @ bit_top  ( 1  <<<  7 )  -  1 
2727  @ bit_number  @ bit_integer  |||  @ bit_float 
2828
29-   @ fun_top  1 
29+   @ fun_top  :fun_top 
3030  @ atom_top  { :negation ,  :sets . new ( version:  2 ) } 
3131  @ map_top  [ { :open ,  % { } ,  [ ] } ] 
3232  @ non_empty_list_top  [ { :term ,  :term ,  [ ] } ] 
@@ -883,7 +883,7 @@ defmodule Module.Types.Descr do
883883
884884  ### Key concepts: 
885885
886-   # * BDD structure: A tree with function nodes and 0/1  leaves. Paths to leaf 1  
886+   # * BDD structure: A tree with function nodes and :fun_top/:fun_bottom  leaves. Paths to :fun_top  
887887  #   represent valid function types. Nodes are positive when following a left 
888888  #   branch (e.g. (int, float) -> bool) and negative otherwise. 
889889
@@ -906,19 +906,19 @@ defmodule Module.Types.Descr do
906906  # unary functions with tuple domains to handle special cases like representing functions of a 
907907  # specific arity (e.g., (none,none->term) for arity 2). 
908908
909-   defp  fun_new ( inputs ,  output ) ,  do:  { { :weak ,  inputs ,  output } ,  1 ,   0 } 
909+   defp  fun_new ( inputs ,  output ) ,  do:  { { :weak ,  inputs ,  output } ,  :fun_top ,   :fun_bottom } 
910910
911911  @ doc  """ 
912912  Creates a function type from a list of inputs and an output where the inputs and/or output may be dynamic. 
913913
914914  For function (t → s) with dynamic components: 
915-   - Static part:  (up (t) → down (s)) 
916-   - Dynamic part: dynamic(down (t) → up (s)) 
915+   - Static part:  (upper_bound (t) → lower_bound (s)) 
916+   - Dynamic part: dynamic(lower_bound (t) → upper_bound (s)) 
917917
918918  When handling dynamic types: 
919-   - `up (t)` extracts the upper bound (most general type) of a gradual type. 
919+   - `upper_bound (t)` extracts the upper bound (most general type) of a gradual type. 
920920    For `dynamic(integer())`, it is `integer()`. 
921-   - `down (t)` extracts the lower bound (most specific type) of a gradual type. 
921+   - `lower_bound (t)` extracts the lower bound (most specific type) of a gradual type. 
922922  """ 
923923  def  fun_descr ( args ,  output )  when  is_list ( args )  do 
924924    dynamic_arguments?  =  are_arguments_dynamic? ( args ) 
@@ -928,8 +928,8 @@ defmodule Module.Types.Descr do
928928      input_static  =  if  dynamic_arguments? ,  do:  materialize_arguments ( args ,  :up ) ,  else:  args 
929929      input_dynamic  =  if  dynamic_arguments? ,  do:  materialize_arguments ( args ,  :down ) ,  else:  args 
930930
931-       output_static  =  if  dynamic_output? ,  do:  down ( output ) ,  else:  output 
932-       output_dynamic  =  if  dynamic_output? ,  do:  up ( output ) ,  else:  output 
931+       output_static  =  if  dynamic_output? ,  do:  lower_bound ( output ) ,  else:  output 
932+       output_dynamic  =  if  dynamic_output? ,  do:  upper_bound ( output ) ,  else:  output 
933933
934934      % { 
935935        fun:  fun_new ( input_static ,  output_static ) , 
@@ -942,12 +942,12 @@ defmodule Module.Types.Descr do
942942  end 
943943
944944  # Gets the upper bound of a gradual type. 
945-   defp  up ( % { dynamic:  dynamic } ) ,  do:  dynamic 
946-   defp  up ( static ) ,  do:  static 
945+   defp  upper_bound ( % { dynamic:  dynamic } ) ,  do:  dynamic 
946+   defp  upper_bound ( static ) ,  do:  static 
947947
948948  # Gets the lower bound of a gradual type. 
949-   defp  down ( :term ) ,  do:  :term 
950-   defp  down ( type ) ,  do:  Map . delete ( type ,  :dynamic ) 
949+   defp  lower_bound ( :term ) ,  do:  :term 
950+   defp  lower_bound ( type ) ,  do:  Map . delete ( type ,  :dynamic ) 
951951
952952  # Tuples represent function domains, using unions to combine parameters. 
953953  # Example: for functions (integer,float)->:ok and (float,integer)->:error 
@@ -967,7 +967,7 @@ defmodule Module.Types.Descr do
967967  1. For static functions, returns their exact domain 
968968  2. For dynamic functions, computes domain based on both static and dynamic parts 
969969
970-   Formula is dom(t) = dom(up (t)) ∪ dynamic(dom(down (t))). 
970+   Formula is dom(t) = dom(upper_bound (t)) ∪ dynamic(dom(lower_bound (t))). 
971971  See Definition 6.15 in https://vlanvin.fr/papers/thesis.pdf. 
972972
973973  ## Examples 
@@ -1034,7 +1034,7 @@ defmodule Module.Types.Descr do
10341034  3. For mixed static/dynamic: computes all valid combinations 
10351035
10361036  # Function application formula for dynamic types: 
1037-   #   τ◦τ′ = (down (τ) ◦ up (τ′)) ∨ (dynamic(up (τ) ◦ down (τ′))) 
1037+   #   τ◦τ′ = (lower_bound (τ) ◦ upper_bound (τ′)) ∨ (dynamic(upper_bound (τ) ◦ lower_bound (τ′))) 
10381038  # 
10391039  # Where: 
10401040  # - τ is a dynamic function type 
@@ -1089,8 +1089,8 @@ defmodule Module.Types.Descr do
10891089  end 
10901090
10911091  # Materializes arguments using the specified direction (up or down) 
1092-   defp  materialize_arguments ( arguments ,  :up ) ,  do:  Enum . map ( arguments ,  & up / 1 ) 
1093-   defp  materialize_arguments ( arguments ,  :down ) ,  do:  Enum . map ( arguments ,  & down / 1 ) 
1092+   defp  materialize_arguments ( arguments ,  :up ) ,  do:  Enum . map ( arguments ,  & upper_bound / 1 ) 
1093+   defp  materialize_arguments ( arguments ,  :down ) ,  do:  Enum . map ( arguments ,  & lower_bound / 1 ) 
10941094
10951095  defp  are_arguments_dynamic? ( arguments ) ,  do:  Enum . any? ( arguments ,  & match? ( % { dynamic:  _ } ,  & 1 ) ) 
10961096
@@ -1101,12 +1101,17 @@ defmodule Module.Types.Descr do
11011101      # At this stage we do not check that the function can be applied to the arguments (using domain) 
11021102      with  { _domain ,  arrows ,  arity }  <-  fun_normalize ( fun_bdd ) , 
11031103           true  <-  arity  ==  length ( arguments )  do 
1104+         # Opti: short-circuits when inner loop is none() or outer loop is term() 
11041105        result  = 
1105-           Enum . reduce ( arrows ,  none ( ) ,  fn  intersection_of_arrows ,  acc  -> 
1106-             Enum . reduce ( intersection_of_arrows ,  term ( ) ,  fn  { _tag ,  _dom ,  ret } ,  acc  -> 
1107-               intersection ( acc ,  ret ) 
1106+           Enum . reduce_while ( arrows ,  none ( ) ,  fn  intersection_of_arrows ,  acc  -> 
1107+             Enum . reduce_while ( intersection_of_arrows ,  term ( ) ,  fn 
1108+               { _tag ,  _dom ,  _ret } ,  acc  when  acc  ==  @ none  ->  { :halt ,  acc } 
1109+               { _tag ,  _dom ,  ret } ,  acc  ->  { :cont ,  intersection ( acc ,  ret ) } 
11081110            end ) 
1109-             |>  union ( acc ) 
1111+             |>  case  do 
1112+               :term  ->  { :halt ,  :term } 
1113+               inner  ->  { :cont ,  union ( inner ,  acc ) } 
1114+             end 
11101115          end ) 
11111116
11121117        { :ok ,  result } 
@@ -1185,8 +1190,8 @@ defmodule Module.Types.Descr do
11851190
11861191  def  fun_get ( acc ,  pos ,  neg ,  bdd )  do 
11871192    case  bdd  do 
1188-       0  ->  acc 
1189-       1  ->  [ { pos ,  neg }  |  acc ] 
1193+       :fun_bottom  ->  acc 
1194+       :fun_top  ->  [ { pos ,  neg }  |  acc ] 
11901195      { fun ,  left ,  right }  ->  fun_get ( fun_get ( acc ,  [ fun  |  pos ] ,  neg ,  left ) ,  pos ,  [ fun  |  neg ] ,  right ) 
11911196    end 
11921197  end 
@@ -1244,8 +1249,8 @@ defmodule Module.Types.Descr do
12441249  # - `fun(integer() -> atom()) and not fun(atom() -> integer())` is not empty 
12451250  defp  fun_empty? ( bdd )  do 
12461251    case  bdd  do 
1247-       1  ->  false 
1248-       0  ->  true 
1252+       :fun_bottom  ->  true 
1253+       :fun_top  ->  false 
12491254      bdd  ->  fun_get ( bdd )  |>  Enum . all? ( fn  { posits ,  negats }  ->  fun_empty? ( posits ,  negats )  end ) 
12501255    end 
12511256  end 
@@ -1321,13 +1326,13 @@ defmodule Module.Types.Descr do
13211326  # See [Castagna and Lanvin (2024)](https://arxiv.org/abs/2408.14345), Theorem 4.2. 
13221327
13231328  defp  phi_starter ( arguments ,  return ,  positives )  do 
1324-     arguments  =  Enum . map ( arguments ,  & { false ,  & 1 } ) 
13251329    n  =  length ( arguments ) 
13261330    # Arity mismatch: if there is one positive function with a different arity, 
13271331    # then it cannot be a subtype of the (arguments->type) functions. 
13281332    if  Enum . any? ( positives ,  fn  { _tag ,  args ,  _ret }  ->  length ( args )  !=  n  end )  do 
13291333      false 
13301334    else 
1335+       arguments  =  Enum . map ( arguments ,  & { false ,  & 1 } ) 
13311336      phi ( arguments ,  { false ,  return } ,  positives ) 
13321337    end 
13331338  end 
@@ -1346,10 +1351,10 @@ defmodule Module.Types.Descr do
13461351
13471352  defp  fun_union ( bdd1 ,  bdd2 )  do 
13481353    case  { bdd1 ,  bdd2 }  do 
1349-       { 1 ,  _ }  ->  1 
1350-       { _ ,  1 }  ->  1 
1351-       { 0 ,  bdd }  ->  bdd 
1352-       { bdd ,  0 }  ->  bdd 
1354+       { :fun_top ,  _ }  ->  :fun_top 
1355+       { _ ,  :fun_top }  ->  :fun_top 
1356+       { :fun_bottom ,  bdd }  ->  bdd 
1357+       { bdd ,  :fun_bottom }  ->  bdd 
13531358      { { fun ,  l1 ,  r1 } ,  { fun ,  l2 ,  r2 } }  ->  { fun ,  fun_union ( l1 ,  l2 ) ,  fun_union ( r1 ,  r2 ) } 
13541359      # Note: this is a deep merge, that goes down bdd1 to insert bdd2 into it. 
13551360      # It is the same as going down bdd1 to insert bdd1 into it. 
@@ -1361,18 +1366,18 @@ defmodule Module.Types.Descr do
13611366  defp  fun_intersection ( bdd1 ,  bdd2 )  do 
13621367    case  { bdd1 ,  bdd2 }  do 
13631368      # Base cases 
1364-       { _ ,  0 }  ->  0 
1365-       { 0 ,  _ }  ->  0 
1366-       { 1 ,  bdd }  ->  bdd 
1367-       { bdd ,  1 }  ->  bdd 
1369+       { _ ,  :fun_bottom }  ->  :fun_bottom 
1370+       { :fun_bottom ,  _ }  ->  :fun_bottom 
1371+       { :fun_top ,  bdd }  ->  bdd 
1372+       { bdd ,  :fun_top }  ->  bdd 
13681373      # Optimizations 
13691374      # If intersecting with a single positive or negative function, we insert 
13701375      # it at the root instead of merging the trees (this avoids going down the 
13711376      # whole bdd). 
1372-       { bdd ,  { fun ,  1 ,   0 } }  ->  { fun ,  bdd ,  0 } 
1373-       { bdd ,  { fun ,  0 ,   1 } }  ->  { fun ,  0 ,  bdd } 
1374-       { { fun ,  1 ,   0 } ,  bdd }  ->  { fun ,  bdd ,  0 } 
1375-       { { fun ,  0 ,   1 } ,  bdd }  ->  { fun ,  0 ,  bdd } 
1377+       { bdd ,  { fun ,  :fun_top ,   :fun_bottom } }  ->  { fun ,  bdd ,  :fun_bottom } 
1378+       { bdd ,  { fun ,  :fun_bottom ,   :fun_top } }  ->  { fun ,  :fun_bottom ,  bdd } 
1379+       { { fun ,  :fun_top ,   :fun_bottom } ,  bdd }  ->  { fun ,  bdd ,  :fun_bottom } 
1380+       { { fun ,  :fun_bottom ,   :fun_top } ,  bdd }  ->  { fun ,  :fun_bottom ,  bdd } 
13761381      # General cases 
13771382      { { fun ,  l1 ,  r1 } ,  { fun ,  l2 ,  r2 } }  ->  { fun ,  fun_intersection ( l1 ,  l2 ) ,  fun_intersection ( r1 ,  r2 ) } 
13781383      { { fun ,  l ,  r } ,  bdd }  ->  { fun ,  fun_intersection ( l ,  bdd ) ,  fun_intersection ( r ,  bdd ) } 
@@ -1381,10 +1386,10 @@ defmodule Module.Types.Descr do
13811386
13821387  defp  fun_difference ( bdd1 ,  bdd2 )  do 
13831388    case  { bdd1 ,  bdd2 }  do 
1384-       { 0 ,  _ }  ->  0 
1385-       { _ ,  1 }  ->  0 
1386-       { bdd ,  0 }  ->  bdd 
1387-       { 1 ,  { fun ,  left ,   right } }  ->  { fun ,  fun_difference ( 1 ,   left ) ,  fun_difference ( 1 ,   right ) } 
1389+       { :fun_bottom ,  _ }  ->  :fun_bottom 
1390+       { _ ,  :fun_top }  ->  :fun_bottom 
1391+       { bdd ,  :fun_bottom }  ->  bdd 
1392+       { :fun_top ,  { fun ,  l ,   r } }  ->  { fun ,  fun_difference ( :fun_top ,   l ) ,  fun_difference ( :fun_top ,   r ) } 
13881393      { { fun ,  l1 ,  r1 } ,  { fun ,  l2 ,  r2 } }  ->  { fun ,  fun_difference ( l1 ,  l2 ) ,  fun_difference ( r1 ,  r2 ) } 
13891394      { { fun ,  l ,  r } ,  bdd }  ->  { fun ,  fun_difference ( l ,  bdd ) ,  fun_difference ( r ,  bdd ) } 
13901395    end 
@@ -2980,10 +2985,10 @@ defmodule Module.Types.Descr do
29802985
29812986  ## Examples 
29822987
2983-       iex> tuple_fetch(domain_descr ([integer(), atom()]), 0) 
2988+       iex> tuple_fetch(tuple ([integer(), atom()]), 0) 
29842989      {false, integer()} 
29852990
2986-       iex> tuple_fetch(union(domain_descr ([integer()]), domain_descr ([integer(), atom()])), 1) 
2991+       iex> tuple_fetch(union(tuple ([integer()]), tuple ([integer(), atom()])), 1) 
29872992      {true, atom()} 
29882993
29892994      iex> tuple_fetch(dynamic(), 0) 
0 commit comments