Full static type inference of set theoretic types

[hissssst]

@josevalim

Correct, but it is yet not decided that integers will be singleton values in our type system

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))

[josevalim]

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.

[hissssst]

@josevalim

@hissssst

Approaches suggested in the paper work only in certain cases.

Which cases? Can you please elaborate? Because the paper is about set-theoretic types and implementation of set-theoretic types, so I would be surprised if the suggestions listed there do not apply to the set-theoretic type system we are implementing.

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.

[Rich_Morin]

@josevalim

On your side, what you could do is to write patterns and guards, which is idiomatic Elixir code anyway, and this will help the VM optimize code and the future type system to find bugs.

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.

-r

[josevalim]

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

[Rich_Morin]

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…

-r

P.S. Once again; great work!

[josevalim]

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.

[DEvil0000]

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

[sabiwara]

@DEvil0000

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