Skip to content

Conversation

@gldubc
Copy link
Member

@gldubc gldubc commented Mar 25, 2025

Implementing set-theoretic function types with correct variance properties: contravariant for arguments, covariant for returns.

The representation uses BDDs: binary trees with functions as internal nodes and 0/1 leaves where paths to 1-leaves represent function intersections present in the type.

So type (integer() -> atom()) and (float() -> pid()) is represented as:

                integer() -> atom()
                /                \
    float() -> pid()             0
    /              \
    1               0

Function nodes are triples {tag, inputs, output} where tag is :weak (:strong to be implemented), inputs is a list of argument types, and output is the return type.

Set-theoretic operations (union, intersection, difference) distribute along the BDD structure.

Function operators include:

  • fun_domain/1 - extracts the domain from a function type
  • fun_apply/2 - calculates return type when applying arguments to a function type
  • fun_fetch/2 - checks if a type contains a function of specific arity

Function types have a given arity, and we can represent the type of "functions of arity 3" as (none(), none(), none()) -> term().

For dynamic functions, we apply the formula
app(fun, args) = app(down(fun), up(args)) ∨ app(dynamic(up(fun)), down(args))
where
- up(type) means uniting the dynamic part of a type with its static part (so up(dynamic(integer()) or float()) = number())
- down(type) means replacing the dynamic part of a type with none()

TODO:

  • Add support for strong function types, but should only be needed for the type annotation version of Elixir
  • Test performance

@josevalim
Copy link
Member

Add support for strong function types, but should only be needed for the type annotation version of Elixir

Theoretically the typed signature that we have today in apply.ex are all strong, but I assume there is no concern about making them weak for now.

@josevalim josevalim added this to the v1.19 milestone May 9, 2025
@josevalim josevalim merged commit df007f7 into elixir-lang:main May 12, 2025
10 checks passed
@josevalim
Copy link
Member

💚 💙 💜 💛 ❤️

@josevalim josevalim deleted the function-types branch May 12, 2025 15:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

3 participants