Hacker News Reader

Comment by sapiogram | Hacker News Reader

Does anyone know what they mean by "set-theoretic types"? I'm a PL nerd, but I've never heard this term before.

The original post Jose wrote announcing the gradual typing project has a good summary of the goal specific to Elixir (2022)

https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi...

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

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

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

For more information about what that means, see this playground [0] from the TypeScript docs. PL people often make a big deal about TypeScript's lack of soundness as though it was some kind of mistake, but it was very much an intentional choice given the trade-offs they were making at the time.

If Elixir can pull off soundness without compromising expressivity that will be a huge feat, and I'm excited to see it!

[0] https://www.typescriptlang.org/play/?strictFunctionTypes=fal...

Yea I never bought this assertion from the TS team, saying “given the trade-offs at the time” is the same as saying “we’re already backed into a corner by previous decisions” - the decision(s) may have been intentional at each step but the design itself probably was not. Given the choice of sound or unsound, considering that the purpose of a type system is to give certain guarantees, a type system design must always choose soundness to be considered reasonable.

That being said, I don’t think it’s possible to “pull off soundness without compromising expressivity” because the expressivity in this context is self-referential types which equate to non-terminating unification logic (and thus, unsoundness). Still, I’m excited to see what they do with this type system! Reminds me a bit of Shen’s type system.

Is the TypeScript team correct in explaining that soundness would exclude functions accepting subtypes as laid out there? If so, it seems like any type system that was meant to be able to type common JavaScript idioms would have to be unsound.

Sub-types can be represented with algebraic types so I’m not sure that’s necessarily true, for example an abstract class with subclasses can be represented as a sum type

only if there is a fixed set of subclasses, which is not always or even mostly the case.

Yes and no - you can't have bi-variant argument types as shown here and be sound, but that does not mean you can't type those idioms. You just need the type system to be able to express a dependency between the name of the event handler and the type of the associated function. It is not exactly straightforward (this is a complex type system feature) though, I don't blame the TS devs for going for an escape hatch there.

(Edit: to be clear, allowing to refine function types in the way they do is part of the solution, the unsound part is that it is not checked afaik)

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/

I did read your article, and it’s actually how I came out with the idea that Elixir had come up with the same idea as TS haha!

I’m sure I’m missing something as I have no doubt you’re by far more knowledgeable than I am, but TS also represents types as sets (semantically, dunno about internal implementation), structural typing seems to inherently map to set theory

For example, about bounded polymorphism the article says “Of course, we can provide syntax sugar for those constraints”: seems like this sugar could be ‘a extends number’ to me, like typescript does. I don’t see how TS does _not_ map to set operations

Sorry for the late reply but I wanted to double check before following up. And I am glad I did because I was told my first response was inaccurate. :)

It is fair to call both TypeScript and Elixir as set-theoretic type system. The big difference is that Elixir's implements semantic subtyping. Here is the paper you can use to dig deeper. I hope it helps: https://www.irif.fr/~gc/papers/lics02.pdf

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".

If you're into watching talks, this will be well worth your time.

ElixirConf 2023 - José Valim - The foundations of the Elixir type system

https://www.youtube.com/watch?v=giYbq4HmfGA

Thanks, this is a fantastic talk. Long, but well worth it, especially if you work with Elixir

It's the definition of types as set of values. Then you have set operations on these types that are lade available. That translates into subtyping considerations.

Cf. Castagna's et.al. For semantic subtyping.

There’s a paper about it, linked from the blog post: https://arxiv.org/abs/2306.06391

Reply on news.ycombinator.com