> You appear to be saying that the values of a type cannot be a subset of another type; that is, there is no '1', only a '1' that is an integer, a '1' that is a short, and so forth, and every '1' is distinct.
That's true, and you can prove it simply by observing that they react differently to ‘the same’ operations, e.g. (2¹⁶ - 1) + 1 has a different value (that responds differently to tests like `≥ 0`) depending on which type we're talking about. There's an injection into the larger type (a type coercion) that is very well-behaved, but it's not an identity map — it changes the operations on the value.
> Further, what's the practical difference between a type defined as consisting of the numbers [1 2 3], and an integer that's restricted to those values?
Nothing (ish: you have to be careful to describe what happens to all the integer operations when restricted to your type) — that's a totally valid way to define a type. But it's not the only way to define a type, because the world of types is much bigger than the world of restricted sets of integers.
> I need to ensure that a patient has some birthdate that's an anticipated type
No, you just have to be explicit about the possibility of a birthdate (or other fields) being of a wide type, e.g.
struct Patient {
wbc_count: Vec<u64>,
birth_date: Box<dyn Any>,
other_fields: HashMap<String, Box<dyn Any>>,
}
Clojure just attaches that by default to every value.
That's true, and you can prove it simply by observing that they react differently to ‘the same’ operations, e.g. (2¹⁶ - 1) + 1 has a different value (that responds differently to tests like `≥ 0`) depending on which type we're talking about. There's an injection into the larger type (a type coercion) that is very well-behaved, but it's not an identity map — it changes the operations on the value.
> Further, what's the practical difference between a type defined as consisting of the numbers [1 2 3], and an integer that's restricted to those values?
Nothing (ish: you have to be careful to describe what happens to all the integer operations when restricted to your type) — that's a totally valid way to define a type. But it's not the only way to define a type, because the world of types is much bigger than the world of restricted sets of integers.
> I need to ensure that a patient has some birthdate that's an anticipated type
No, you just have to be explicit about the possibility of a birthdate (or other fields) being of a wide type, e.g.
Clojure just attaches that by default to every value.