Full static type inference of set theoretic types

I’ve expected this response. You can translate this example to Enum.random(for x <- 1..n, y <- 1..n, when x != y, do: {Tuple.duplicate(nil, x), Tuple.duplicate(nil, y)}). And the false positive to 1 / (tuple_size(x) - tuple_size(y))

I don’t see how that changes anything. If we only have integer(), we won’t get any compile-time warning on 1/integer(). There is no false positive here.

Tuple.duplicate/2 with a dynamic value can also only emit tuple(), we cannot assert on the shape. If you have specific shapes, then you need specific tuple instantiations. In the same way someone should not expect String.to_atom(expr) to return a particular atom instance at compile-time.

Edit: in any case, I am not saying we won’t have a false positive ever. What I am saying we will make decisions in order to guarantee the type system is performant and minimize false positives on common Elixir idioms.

They apply, but only partially. As the paper states, they use BDD of DNF (which is essentially a lookup tree for disjoint intersections) with lazy unions, and this structure has problems where non-union operations are applied to the set during the inference and subtype checking after a series of union operations.

I would like to see some discussion of (current and/or impending) “idiomatic Elixir code” practices in the context of this work. For example, I’d think that writing lots of short functions (e.g., as recommended by @pragdave) would make things easier for the type inference code.


It is literally writing patterns and guards. It can be in function heads, case, etc. The size of the function does not matter. :slight_smile:

1 Like

Erm, imagine two implementations of some functionality. One uses a long, complex function chock full of flow control constructs (e.g., case, cond, if). The other has been decomposed into a set of small, tightly-focused functions which rely heavily on patterns and guards. Even if the compiler (etc) has no problem with the first approach, a coder might…


P.S. Once again; great work!

To clarify, you asked in context of the work, so my reply focused only on that. In context of the type inference in my earlier quote, the size does not matter. :slight_smile:

1 Like

How about a Number type so int and float can get expressed in one simple type.
This may be useful for something like your negate/1 example.
$ Number → Number

How about a template like T type so one could write “same in as out”
$ T → T

A possible syntax for this is covered in the recently published blog post:

$ a and number() -> a and number()
def identity(arg), do: arg

Or course, we can provide syntax sugar for those constraints:

$ a -> a when a: number()
def identity(arg), do: arg