Comment by ch4s3
12 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
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.
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.
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.
1 reply →