@@ -93,23 +93,42 @@ defmodule Module.Types.Descr do
93
93
Creates a function type with the given arguments and return type.
94
94
95
95
## Examples
96
- iex> fun([integer()], atom()) # Creates (integer) -> atom
97
- iex> fun([integer(), float()], boolean()) # Creates (integer, float) -> boolean
96
+
97
+ fun([integer()], atom())
98
+ #=> (integer -> atom)
99
+
100
+ fun([integer(), float()], boolean())
101
+ #=> (integer, float -> boolean)
98
102
"""
99
103
def fun ( args , return ) when is_list ( args ) , do: fun_descr ( args , return )
100
104
101
105
@ doc """
102
- Creates the top function type for the given arity, where all arguments are none()
103
- and return is term().
106
+ Creates the top function type for the given arity,
107
+ where all arguments are none() and return is term().
104
108
105
109
## Examples
106
- iex> fun(1) # Creates (none) -> term
107
- iex> fun(2) # Creates (none, none) -> term
110
+
111
+ fun(1)
112
+ #=> (none -> term)
113
+
114
+ fun(2)
115
+ #=> Creates (none, none) -> term
108
116
"""
109
117
def fun ( arity ) when is_integer ( arity ) and arity >= 0 do
110
118
fun ( List . duplicate ( none ( ) , arity ) , term ( ) )
111
119
end
112
120
121
+ @ doc """
122
+ Tuples represent function domains, using unions to combine parameters.
123
+
124
+ Example: for functions (integer, float ->:ok) and (float, integer -> :error)
125
+ domain isn't {integer|float,integer|float} as that would incorrectly accept {float,float}
126
+ Instead, it is {integer,float} or {float,integer}
127
+
128
+ Made public for testing.
129
+ """
130
+ def domain_descr ( types ) when is_list ( types ) , do: tuple ( types )
131
+
113
132
## Optional
114
133
115
134
# `not_set()` is a special base type that represents an not_set field in a map.
@@ -704,11 +723,11 @@ defmodule Module.Types.Descr do
704
723
if not empty? ( descr ) and fun_only? ( descr , arity ) , do: :ok , else: :error
705
724
706
725
{ dynamic , static } ->
707
- empty_static = empty? ( static )
726
+ empty_static? = empty? ( static )
708
727
709
728
cond do
710
- not empty_static -> if fun_only? ( static , arity ) , do: :ok , else: :error
711
- empty_static and not empty? ( intersection ( dynamic , fun ( arity ) ) ) -> :ok
729
+ not empty_static? -> if fun_only? ( static , arity ) , do: :ok , else: :error
730
+ empty_static? and not empty? ( intersection ( dynamic , fun ( arity ) ) ) -> :ok
712
731
true -> :error
713
732
end
714
733
end
@@ -880,47 +899,46 @@ defmodule Module.Types.Descr do
880
899
881
900
# Function types are represented using Binary Decision Diagrams (BDDs) for efficient
882
901
# handling of unions, intersections, and negations.
902
+ #
903
+ # Currently, they only represent weak types. It is yet to be decided how all of the
904
+ # types will be encoded in the descr.
883
905
884
906
### Key concepts:
885
907
886
- # * BDD structure: A tree with function nodes and :fun_top/:fun_bottom leaves. Paths to :fun_top
887
- # represent valid function types. Nodes are positive when following a left
888
- # branch (e.g. (int, float) -> bool) and negative otherwise.
908
+ # * BDD structure: A tree with function nodes and :fun_top/:fun_bottom leaves.
909
+ # Paths to :fun_top represent valid function types. Nodes are positive when
910
+ # following a left branch (e.g. (int, float -> bool) and negative otherwise.
889
911
890
912
# * Function variance:
891
913
# - Contravariance in arguments: If s <: t, then (t → r) <: (s → r)
892
914
# - Covariance in returns: If s <: t, then (u → s) <: (u → t)
893
915
894
916
# * Representation:
895
917
# - fun(): Top function type (leaf 1)
896
- # - Function literals: {tag, [t1, ..., tn], t} where [t1, ..., tn] are argument types and t is return type
897
- # tag is either `:weak` or `:strong`
898
- # TODO: implement `:strong`
918
+ # - Function literals: {[t1, ..., tn], t} where [t1, ..., tn] are argument types and t is return type
899
919
# - Normalized form for function applications: {domain, arrows, arity} is produced by `fun_normalize/1`
900
920
901
921
# * Examples:
902
922
# - fun([integer()], atom()): A function from integer to atom
903
923
# - intersection(fun([integer()], atom()), fun([float()], boolean())): A function handling both signatures
904
924
905
- # Note: Function domains are expressed as tuple types. We use separate representations rather than
906
- # unary functions with tuple domains to handle special cases like representing functions of a
907
- # specific arity (e.g., (none,none->term) for arity 2).
908
-
925
+ # Note: Function domains are expressed as tuple types. We use separate representations
926
+ # rather than unary functions with tuple domains to handle special cases like representing
927
+ # functions of a specific arity (e.g., (none,none->term) for arity 2).
909
928
defp fun_new ( inputs , output ) , do: { { inputs , output } , :fun_top , :fun_bottom }
910
929
911
- @ doc """
912
- Creates a function type from a list of inputs and an output where the inputs and/or output may be dynamic.
913
-
914
- For function (t → s) with dynamic components:
915
- - Static part: (upper_bound(t) → lower_bound(s))
916
- - Dynamic part: dynamic(lower_bound(t) → upper_bound(s))
917
-
918
- When handling dynamic types:
919
- - `upper_bound(t)` extracts the upper bound (most general type) of a gradual type.
920
- For `dynamic(integer())`, it is `integer()`.
921
- - `lower_bound(t)` extracts the lower bound (most specific type) of a gradual type.
922
- """
923
- def fun_descr ( args , output ) when is_list ( args ) do
930
+ # Creates a function type from a list of inputs and an output
931
+ # where the inputs and/or output may be dynamic.
932
+ #
933
+ # For function (t → s) with dynamic components:
934
+ # - Static part: (upper_bound(t) → lower_bound(s))
935
+ # - Dynamic part: dynamic(lower_bound(t) → upper_bound(s))
936
+ #
937
+ # When handling dynamic types:
938
+ # - `upper_bound(t)` extracts the upper bound (most general type) of a gradual type.
939
+ # For `dynamic(integer())`, it is `integer()`.
940
+ # - `lower_bound(t)` extracts the lower bound (most specific type) of a gradual type.
941
+ defp fun_descr ( args , output ) when is_list ( args ) do
924
942
dynamic_arguments? = are_arguments_dynamic? ( args )
925
943
dynamic_output? = match? ( % { dynamic: _ } , output )
926
944
@@ -949,16 +967,11 @@ defmodule Module.Types.Descr do
949
967
defp lower_bound ( :term ) , do: :term
950
968
defp lower_bound ( type ) , do: Map . delete ( type , :dynamic )
951
969
952
- # Tuples represent function domains, using unions to combine parameters.
953
- # Example: for functions (integer,float)->:ok and (float,integer)->:error
954
- # domain isn't {integer|float,integer|float} as that would incorrectly accept {float,float}
955
- # Instead, it is {integer,float} or {float,integer}
956
- def domain_descr ( types ) when is_list ( types ) , do: tuple ( types )
957
-
958
970
@ doc """
959
971
Calculates the domain of a function type.
960
972
961
973
For a function type, the domain is the set of valid input types.
974
+
962
975
Returns:
963
976
- `:badfunction` if the type is not a function type
964
977
- A tuple type representing the domain for valid function types
@@ -1021,7 +1034,7 @@ defmodule Module.Types.Descr do
1021
1034
1022
1035
defp fun_domain_static ( :term ) , do: :badfunction
1023
1036
defp fun_domain_static ( % { } ) , do: { :ok , none ( ) }
1024
- defp fun_domain_static ( :emptyfunction ) , do: { :ok , none ( ) }
1037
+ defp fun_domain_static ( :empty_function ) , do: { :ok , none ( ) }
1025
1038
1026
1039
@ doc """
1027
1040
Applies a function type to a list of argument types.
@@ -1205,7 +1218,7 @@ defmodule Module.Types.Descr do
1205
1218
## Return Values
1206
1219
#
1207
1220
# - `{domain, arrows, arity}` for valid function BDDs
1208
- # - `:emptyfunction ` if the BDD represents an empty function type
1221
+ # - `:empty_function ` if the BDD represents an empty function type
1209
1222
#
1210
1223
# ## Internal Use
1211
1224
#
@@ -1232,7 +1245,7 @@ defmodule Module.Types.Descr do
1232
1245
end
1233
1246
end )
1234
1247
1235
- if arrows == [ ] , do: :emptyfunction , else: { domain , arrows , arity }
1248
+ if arrows == [ ] , do: :empty_function , else: { domain , arrows , arity }
1236
1249
end
1237
1250
1238
1251
# Checks if a function type is empty.
@@ -1262,12 +1275,12 @@ defmodule Module.Types.Descr do
1262
1275
# 2. There exists a negative function that negates the whole positive intersection
1263
1276
1264
1277
## Examples
1278
+ #
1265
1279
# - `{[fun(1)], []}` is not empty
1266
1280
# - `{[fun(1), fun(2)], []}` is empty (different arities)
1267
1281
# - `{[fun(integer() -> atom())], [fun(none() -> term())]}` is empty
1268
1282
# - `{[], _}` (representing the top function type fun()) is never empty
1269
1283
#
1270
- # TODO: test performance
1271
1284
defp fun_empty? ( [ ] , _ ) , do: false
1272
1285
1273
1286
defp fun_empty? ( positives , negatives ) do
@@ -1278,9 +1291,12 @@ defmodule Module.Types.Descr do
1278
1291
1279
1292
{ positive_arity , positive_domain } ->
1280
1293
# Check if any negative function negates the whole positive intersection
1281
- # e.g. (integer()->atom()) is negated by
1282
- # i) (none()->term()) ii) (none()->atom())
1283
- # ii) (integer()->term()) iv) (integer()->atom())
1294
+ # e.g. (integer() -> atom()) is negated by:
1295
+ #
1296
+ # * (none() -> term())
1297
+ # * (none() -> atom())
1298
+ # * (integer() -> term())
1299
+ # * (integer() -> atom())
1284
1300
Enum . any? ( negatives , fn { neg_arguments , neg_return } ->
1285
1301
# Filter positives to only those with matching arity, then check if the negative
1286
1302
# function's domain is a supertype of the positive domain and if the phi function
@@ -1311,7 +1327,7 @@ defmodule Module.Types.Descr do
1311
1327
1312
1328
# Implements the Φ (phi) function for determining function subtyping relationships.
1313
1329
#
1314
- ## Algorithm
1330
+ # # # Algorithm
1315
1331
#
1316
1332
# For inputs t₁...tₙ, booleans b₁...bₙ, negated return type t, and set of arrow types P:
1317
1333
#
@@ -1324,7 +1340,6 @@ defmodule Module.Types.Descr do
1324
1340
# Returns true if the intersection of the positives is a subtype of (t1,...,tn)->(not t).
1325
1341
#
1326
1342
# See [Castagna and Lanvin (2024)](https://arxiv.org/abs/2408.14345), Theorem 4.2.
1327
-
1328
1343
defp phi_starter ( arguments , return , positives ) do
1329
1344
n = length ( arguments )
1330
1345
# Arity mismatch: if there is one positive function with a different arity,
@@ -1399,27 +1414,25 @@ defmodule Module.Types.Descr do
1399
1414
defp fun_to_quoted ( :fun , _opts ) , do: [ { :fun , [ ] , [ ] } ]
1400
1415
1401
1416
defp fun_to_quoted ( bdd , opts ) do
1402
- arrows = bdd |> fun_get ( )
1417
+ arrows = fun_get ( bdd )
1403
1418
1404
- for { positives , negatives } <- arrows ,
1405
- not fun_empty? ( positives , negatives ) do
1419
+ for { positives , negatives } <- arrows , not fun_empty? ( positives , negatives ) do
1406
1420
fun_intersection_to_quoted ( positives , opts )
1407
1421
end
1408
1422
|> case do
1409
1423
[ ] -> [ ]
1410
- [ single ] -> [ single ]
1411
1424
multiple -> [ Enum . reduce ( multiple , & { :or , [ ] , [ & 2 , & 1 ] } ) ]
1412
1425
end
1413
1426
end
1414
1427
1415
1428
defp fun_intersection_to_quoted ( intersection , opts ) do
1416
1429
intersection
1417
1430
|> Enum . map ( fn { args , ret } ->
1418
- { :-> , [ ] , [ [ to_quoted ( tuple_descr ( :closed , args ) , opts ) ] , to_quoted ( ret , opts ) ] }
1431
+ { :__block__ , [ ] ,
1432
+ [ [ { :-> , [ ] , [ Enum . map ( args , & to_quoted ( & 1 , opts ) ) , to_quoted ( ret , opts ) ] } ] ] }
1419
1433
end )
1420
1434
|> case do
1421
1435
[ ] -> { :fun , [ ] , [ ] }
1422
- [ single ] -> single
1423
1436
multiple -> Enum . reduce ( multiple , & { :and , [ ] , [ & 2 , & 1 ] } )
1424
1437
end
1425
1438
end
0 commit comments