In your example, wouldn't `none()` be a type for `x` that satisfies both `Integer.to_string(x)` and `Atom.to_string(x)`? Or do you special-case `none()` and error if it occurs?
In our case, we implement a bidirectional system where before applying x to Integer.to_string, we compute the domain of Integer.to_string (which is integer) and pass it up. If x is a dynamic type, then we refine it. So on the first call, x refines to `dynamic & integer`, then we apply it.
The second refinement fails because it becomes none, so we discard it, but it means the application on Atom.to_string will fail anyway. So yes, we check for emptiness and discard none.
If the body of the function contained only the first or the second call, the verdict would have been that x is respectively an Integer or an Atom and the type of the function is the type of the contained expression.
That depends on the implementation of gradual typing. Elixir implements gradual set-theoretic types where dynamic types are a range of existing types and can be refined for typing violations. Here is a trivial example:
Since the function is untyped, `x` gets an initial value of `dynamic()`, but it still reports a typing violation because it first gets refined as `dynamic(integer())` which is then incompatible with the `atom()` type.We also introduced the concept of strong arrows, which allows dynamic and static parts of a codebase to interact without introducing runtime checks and remaining sound. More information here: https://elixir-lang.org/blog/2023/09/20/strong-arrows-gradua...