← Back to context

Comment by sa1

10 hours 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?

7 comments

sa1

Reply
mechanicum  9 hours 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

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

[1]: https://www.irif.fr/~gc/papers/elixir-type-design.pdf

[2]: https://www.youtube.com/watch?v=gJJH7a2J9O8

[3]: https://www.youtube.com/watch?v=VYmo867YF6g

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

  • sa1  9 hours 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  9 hours 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

  • sa1  9 hours 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.