3 ms·

What do set-theoretic types mean? Aren’t types an alternative approach meant to avoid the paradoxes with sets? Is it just being used as a marketing term?

by sa1 4mo ago

mechanicum 4mo ago
Short answer: “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”. Long answer, well, there are blog posts[0], the Design Principles of the Elixir Type System paper[1] and related presentations[2, 3, 4] that talk about it at length. Giuseppe Castagna’s site has many more related papers: https://www.irif.fr/~gc/topics.en.html https://www.irif.fr/~gc/topics.en.html [0]: 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... [1]: https://www.irif.fr/~gc/papers/elixir-type-design.pdf https://www.irif.fr/~gc/papers/elixir-type-design.pdf [2]: https://www.youtube.com/watch?v=gJJH7a2J9O8 https://www.youtube.com/watch?v=gJJH7a2J9O8 [3]: https://www.youtube.com/watch?v=VYmo867YF6g https://www.youtube.com/watch?v=VYmo867YF6g [4]: https://www.youtube.com/watch?v=giYbq4HmfGA https://www.youtube.com/watch?v=giYbq4HmfGA
- sa1 4mo ago
  Sets and types are foundational mathematical concepts so I’m looking for how elixir’s types fit in that context. Union and intersection are not something that belongs only to sets.
ch4s3 4mo ago
It means that the types are built on unions, intersections, and negations[1]. It's a polymorphic type system with inference at the function level. It also does some type narrowing with pattern matching. [1] https://www.irif.fr/_media/users/gduboc/elixir-types.pdf https://www.irif.fr/_media/users/gduboc/elixir-types.pdf
- sa1 4mo ago
  Unions, intersections and negations are available in types as well and are by no means exclusive to sets. The distinguishing feature of a set vs type is that a value belongs to just one type while it can belong to several sets.
  - spider-mario 4mo ago
    Types do not inherently have any such restrictions. A value can belong to several types. In fact, if you posit types to have union, that necessarily follows.
    - sa1 4mo ago
      I think they do, and as you mentioned you can explicitly remove such a restriction. Sets and types are once again two different kinds of objects in mathematical theory, and a set-theoretic type doesn’t seem to be based either on set theory or type theory.
      - spider-mario 4mo ago
        If types have unions/intersections/negations, as you originally seemed to imply, then “a value belongs to just one type” is false (if x is of type A then it’s also of type A ∪ B for any B). If they don’t unless you add them to “explicitly remove such a restriction”, then that means you’re making types more set-like (set-theoretic). In strict “type theory”, it’s the latter: types don’t have unions (in the sense that set-theoretic types do). There are sum types, which are different.

What do set-theoretic types mean? Aren’t types an alternative approach meant to avoid the paradoxes with sets? Is it just being used as a marketing term?

by sa1 4mo ago

What do set-theoretic types mean? Aren’t types an alternative approach meant to avoid the paradoxes with sets? Is it just being used as a marketing term?

mechanicum 4mo ago

Short answer: “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”. Long answer, well, there are blog posts[0], the Design Principles of the Elixir Type System paper[1] and related presentations[2, 3, 4] that talk about it at length. Giuseppe Castagna’s site has many more related papers: https://www.irif.fr/~gc/topics.en.html https://www.irif.fr/~gc/topics.en.html [0]: 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... [1]: https://www.irif.fr/~gc/papers/elixir-type-design.pdf https://www.irif.fr/~gc/papers/elixir-type-design.pdf [2]: https://www.youtube.com/watch?v=gJJH7a2J9O8 https://www.youtube.com/watch?v=gJJH7a2J9O8 [3]: https://www.youtube.com/watch?v=VYmo867YF6g https://www.youtube.com/watch?v=VYmo867YF6g [4]: https://www.youtube.com/watch?v=giYbq4HmfGA https://www.youtube.com/watch?v=giYbq4HmfGA

sa1 4mo ago
Sets and types are foundational mathematical concepts so I’m looking for how elixir’s types fit in that context. Union and intersection are not something that belongs only to sets.

ch4s3 4mo ago

It means that the types are built on unions, intersections, and negations[1]. It's a polymorphic type system with inference at the function level. It also does some type narrowing with pattern matching. [1] https://www.irif.fr/_media/users/gduboc/elixir-types.pdf https://www.irif.fr/_media/users/gduboc/elixir-types.pdf

sa1 4mo ago
Unions, intersections and negations are available in types as well and are by no means exclusive to sets. The distinguishing feature of a set vs type is that a value belongs to just one type while it can belong to several sets.
- spider-mario 4mo ago
  Types do not inherently have any such restrictions. A value can belong to several types. In fact, if you posit types to have union, that necessarily follows.
  - sa1 4mo ago
    I think they do, and as you mentioned you can explicitly remove such a restriction. Sets and types are once again two different kinds of objects in mathematical theory, and a set-theoretic type doesn’t seem to be based either on set theory or type theory.
    - spider-mario 4mo ago
      If types have unions/intersections/negations, as you originally seemed to imply, then “a value belongs to just one type” is false (if x is of type A then it’s also of type A ∪ B for any B). If they don’t unless you add them to “explicitly remove such a restriction”, then that means you’re making types more set-like (set-theoretic). In strict “type theory”, it’s the latter: types don’t have unions (in the sense that set-theoretic types do). There are sum types, which are different.