7 ms·
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
by 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 agoIf 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.