5 ms·

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

kylecazar 2y ago
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-elixir-set-theoretic-types/ https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi...
pjam 2y ago
There’s a paper about it, linked from the blog post: https://arxiv.org/abs/2306.06391 https://arxiv.org/abs/2306.06391
bobwaycott 2y ago
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 https://www.irif.fr/_media/users/gduboc/elixir-types.pdf
- williamdclt 2y ago
  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
  - weatherlight 2y ago
    Typescript's type system isn't sound. The Set theoretical type system proposed for Elixir is.
    - lolinder 2y ago
      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=false#example/soundness https://www.typescriptlang.org/play/?strictFunctionTypes=fal...
      - zarathustreal 2y ago
        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.
        lolinder 2y ago
        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.
gregors 2y ago
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 https://www.youtube.com/watch?v=giYbq4HmfGA
- freedomben 2y ago
  Thanks, this is a fantastic talk. Long, but well worth it, especially if you work with Elixir
aatd86 2y ago
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.

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-elixir-set-theoretic-types/ https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi...

pjam 2y ago

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

bobwaycott 2y ago

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 https://www.irif.fr/_media/users/gduboc/elixir-types.pdf

williamdclt 2y ago
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
- weatherlight 2y ago
  Typescript's type system isn't sound. The Set theoretical type system proposed for Elixir is.
  - lolinder 2y ago
    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=false#example/soundness https://www.typescriptlang.org/play/?strictFunctionTypes=fal...
    - zarathustreal 2y ago
      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.
      - lolinder 2y ago
        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.

gregors 2y ago

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 https://www.youtube.com/watch?v=giYbq4HmfGA

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

aatd86 2y ago

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.