[bobwaycott]

From the original paper[0]:

> We present a gradual type system for Elixir, based on the framework of semantic subtyping ... [which] provides a type system centered on the use of set-theoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations. The system is a polymorphic type system with local type inference, that is, functions are explicitly annotated with types that may contain type variables, but their applications do not require explicit instantiations: the system deduces the right instantiations of every type variable. It also features precise typing of pattern matching combined with type narrowing: the types of the capture variables of the pattern and of some variables of the matched expression are refined in the branches to take into account the results of pattern matching.

[0]: https://www.irif.fr/_media/users/gduboc/elixir-types.pdf

[williamdclt]

sounds like what typescript does, I'm not clear if the Elixir approach is different from "structural typing" (as TS calls it) or if they're rediscovering the same thing. Either way, I'm happy it's the way they're going

[josevalim]

While both Elixir and TypeScript are structural, they are different type systems. A set-theoretic type system is not one that has unions, intersections, negations, but rather one where the foundation of the type system is represented on top of unions, intersections, and negations. Even relations such as subtyping, compatibility, etc. are expressed as set-theoretic. We also have a very different approach to dynamic/gradual typing (which is sound): https://elixir-lang.org/blog/2023/09/20/strong-arrows-gradua...

I recommend reading Giuseppe Castagna's work for those who want to dig deeper: https://www.irif.fr/~gc/

[throwawaymaths]

Elixir is going to be fundamentally different from TS though. The base set of datatypes is quite well defined, and function activities are rather composable unlike JS where "basically anything can happen".

[weatherlight]

Typescript's type system isn't sound. The Set theoretical type system proposed for Elixir is.