Generally speaking, the more expressive a type system, the harder or more expensive it is to have full inference. If a language chooses to have performant type inference for all of its valid programs, then it often ends up with a type system that rejects more programs. A classic example in Haskell is (\x -> x x) (\y -> y) which is not valid because inference is undecidable (although iirc you can write that with some extensions and explicit type annotations).

I chose to accept more programs instead of full-blown type inference early on in our journey for three reasons:

• We must avoid breaking changes (i.e. rejecting valid programs today)

• If you don’t want to write the types, you can already not write the types today (and strong arrows/type inference from patterns and guards do their best to find errors)

• Users of languages with type inference often recommend writing the types anyways (at least for public functions, private functions can make use of other techniques such as inlining to find errors)

I believe there will be a paper at POPL 2023 on type inference of set-theoretic types which will go into more details. However, it will be too expensive to make it part of the compiler. The types it infers though are incredibly precise. For example, imagine you have a list of integers and strings, and you want to get only integers:

 Enum.filter(list_of_ints_and_strs, &is_integer/1) #=> [1, 23, 56, ...]

In most programming languages, filter has the type: [a], (a -> boolean()) -> [a], which means both incoming and outgoing list still has the type [integer() or string()], even if you keep only integers. However, with set theoretic types, we could get (and infer) the type:

[a or b], (a -> true) and (b -> false) -> [a]

Which in our example it would instantiate:

[integer() or binary()], (integer() -> true) and (binary() -> false) -> [integer()]

And therefore that the type system knows you removed all strings from the list. Being this precise has a high cost during inference (and we want to be precise!). At best, we could be able to use it as an explicit command like “what is the signature for this function” but not as part of compilation.

One last note: a type system with unions and intersections do not necessarily make it a set-theoretic type system. To be set-theoretic the foundation of the type system must all be based on set semantics. You can implement set operations in other ways.

That’s an excellent question and I ask myself the same. I believe we do want to provide mechanisms for the developers to know and/or enforce if arrows are strong or not, but it is yet unclear what those mechanisms should be.

Type errors will initially be emitted as warnings (and potentially for quite some time).

There is an implementation of set-theoretic types in the CDuce programming language, which already employs many optimization techniques we can lift from (some discussed in this paper). Given we took a “paper first” approach, I recommend reading the existing literature if you want to speculate on the implementation details. The literature exists precisely so we don’t have to rely solely on opinions.

I also don’t rule out the possibility of implementing the data types of the type system in a native programming language, such as Rust. Again, it is not my first option, I would prefer Elixir, but the type system is powered by different types of sets which define union/intersection/negation, which we could implement in a native language with the ultimate goal of performance. The traversal of AST and the application of the typing rules would still be done in Elixir.

In any case, it is either we do the paper-first, and then later find out it is too complex to implement, or we do implementation-first, and then find out the implementation is incorrect. If it fails, both end-up in the same place: we don’t have a type system up to our requirements. I already tried the implementation first approach back in 2018 and I know exactly where it ends: with you wondering if what you are doing is, by any chance, correct.

Excellent question, I was waiting for someone to ask it. We will start with option 1: we will fallback to dynamic. However, I can see us also doing option 3 in the future, if we can measure places where introducing the runtime checks will not decrease or will potentially improve performance.