7 ms·

> 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

by Twey 7d ago

> 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.

weavejester 7d ago
> 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. Then at which point does a type become equivalent to a restriction that could be decoupled from the underlying type by choosing a broader type? > No, you just have to be explicit about the possibility of a birthdate (or other fields) being of a wide type Yes, you could recreate Clojure's semantics in Rust. More accurately, I'd say you'd be looking at defining it like so: struct WbcCount { wbc_count: Vec<u64> } struct BirthDate { birth_date: Box<dyn Any> } Since we want to be able to reason about these keypairs individually. You might have a structure that has a WbcCount but not a BirthDate, or one with a BirthDate but not a WbcCount, or one with neither. We'd then be faced with the challenge of creating a type that could contain an arbitrary number of unique structs, and to be able to pull a struct out of that set by its type. Realistically we'd probably just use a HashMap at that point and discard all static typing. Alternatively, we could create a mega struct that contains every possible field we could want to use, whether or not we know they are related, and use this data structure to represent all structured data in the application. The "if everything is coupled, nothing is" approach. But both of those options are difficult or unidiomatic to write. Languages like Rust, Java, etc. encourage coupling of data because it's more convenient and space efficient to group data together in records/structs. In Clojure, there's no need to do so; we can couple only when necessary. If we don't need to know the birthdate to calculate the white blood cell count, then we can exclude that field from the input type checking. Most statically typed languages find this difficult, with TypeScript being one of the few exceptions in this regard.
- Twey 6d ago
  > Then at which point does a type become equivalent to a restriction that could be decoupled from the underlying type by choosing a broader type? I'm not totally sure how to interpret this question. If I already have a type that includes all the values I want as a subset, I can restrict that type by limiting the values it can take and restricting or removing the operations on it to guarantee they never produce any of the forbidden values. That's the basis of refinement type systems like Liquid Haskell etc. For any type I can describe this way I can also build it ‘from the ground up’ by starting with the empty type and adding operations, though it might not be as convenient. But the converse isn't true: not every type I can build additively can be refined subtractively from another type. For a start, you need to have a broader type to begin with, so that has to already be built somehow: you can't refine an 8-bit integer into an HTTP server. > You might have a structure that has a WbcCount but not a BirthDate, or one with a BirthDate but not a WbcCount, or one with neither. Remember that a `Box<dyn Any>` could also be a ‘no value’ type like `()` or a ‘maybe no value’ type like `Option<Date>`. But yes, there are many equivalent ways to write it depending on how likely the values are to exist; the precise formulation is just a question of ergonomics. > We'd then be faced with the challenge of creating a type that could contain an arbitrary number of unique structs, and to be able to pull a struct out of that set by its type. By its name, but yes, that's exactly what you get with the `other_fields` field in my example above. > and discard all static typing Well, that's not quite true: we discard (syntactically, but not conceptually!) the type information about the fields of this struct, but we can regain it later (from the conceptual information we retain) by trying to downcast the `Any`. Then you get your static type information back and the compiler can help you again. > But both of those options are difficult or unidiomatic to write. Sorry, I hope I haven't come across too harsh to Clojure here. As I thought I was clear about above, Clojure's ergonomics for writing dynamically-typed code are vastly superior to Rust's. By coupling runtime type information to values and restricting itself to only being able to deal with values that are data and have runtime type data attached, Clojure gets to make a whole bunch of simplifying assumptions that reduce the work the programmer has to do when dealing with such values. That's the trade-off: Rust chooses to be able to express a much wider range of types by not requiring that coupling, but in exchange you have to be much more explicit when you do want to couple runtime type information to your values. Some languages like C# aim to be able to do both, i.e. start strongly typed and drop down ergonomically into dynamic typing as desired, but Rust is not one of those languages. > If we don't need to know the birthdate to calculate the white blood cell count, then we can exclude that field from the input type checking. But that very exclusion requires that you know enough about the value to know that it can be safely ‘excluded’ without having any additional information about it. Specifically you need to know: - how to access a subfield of the type regardless of the other fields on it — this requires that it contain RTTI - how to discard the value — this requires that it have a destructor with a known calling convention - how to move/copy the value into the function (and maybe even move out of the function if you return it or imperatively add it to some global state) — this requires that you know a ‘moving constructor’ for the value that can be used to safely move it to another location In the Rust case you need to write down these things explicitly so the compiler can make sure you don't pass a value that doesn't satisfy them. In Clojure, the reason you don't need to write them down is that every value in the language is restricted to only be able to represent such values, so those constraints are implicitly on every function that you write.

by Twey 7d ago

weavejester 7d ago

> 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. Then at which point does a type become equivalent to a restriction that could be decoupled from the underlying type by choosing a broader type? > No, you just have to be explicit about the possibility of a birthdate (or other fields) being of a wide type Yes, you could recreate Clojure's semantics in Rust. More accurately, I'd say you'd be looking at defining it like so: struct WbcCount { wbc_count: Vec<u64> } struct BirthDate { birth_date: Box<dyn Any> } Since we want to be able to reason about these keypairs individually. You might have a structure that has a WbcCount but not a BirthDate, or one with a BirthDate but not a WbcCount, or one with neither. We'd then be faced with the challenge of creating a type that could contain an arbitrary number of unique structs, and to be able to pull a struct out of that set by its type. Realistically we'd probably just use a HashMap at that point and discard all static typing. Alternatively, we could create a mega struct that contains every possible field we could want to use, whether or not we know they are related, and use this data structure to represent all structured data in the application. The "if everything is coupled, nothing is" approach. But both of those options are difficult or unidiomatic to write. Languages like Rust, Java, etc. encourage coupling of data because it's more convenient and space efficient to group data together in records/structs. In Clojure, there's no need to do so; we can couple only when necessary. If we don't need to know the birthdate to calculate the white blood cell count, then we can exclude that field from the input type checking. Most statically typed languages find this difficult, with TypeScript being one of the few exceptions in this regard.

Twey 6d ago
> Then at which point does a type become equivalent to a restriction that could be decoupled from the underlying type by choosing a broader type? I'm not totally sure how to interpret this question. If I already have a type that includes all the values I want as a subset, I can restrict that type by limiting the values it can take and restricting or removing the operations on it to guarantee they never produce any of the forbidden values. That's the basis of refinement type systems like Liquid Haskell etc. For any type I can describe this way I can also build it ‘from the ground up’ by starting with the empty type and adding operations, though it might not be as convenient. But the converse isn't true: not every type I can build additively can be refined subtractively from another type. For a start, you need to have a broader type to begin with, so that has to already be built somehow: you can't refine an 8-bit integer into an HTTP server. > You might have a structure that has a WbcCount but not a BirthDate, or one with a BirthDate but not a WbcCount, or one with neither. Remember that a `Box<dyn Any>` could also be a ‘no value’ type like `()` or a ‘maybe no value’ type like `Option<Date>`. But yes, there are many equivalent ways to write it depending on how likely the values are to exist; the precise formulation is just a question of ergonomics. > We'd then be faced with the challenge of creating a type that could contain an arbitrary number of unique structs, and to be able to pull a struct out of that set by its type. By its name, but yes, that's exactly what you get with the `other_fields` field in my example above. > and discard all static typing Well, that's not quite true: we discard (syntactically, but not conceptually!) the type information about the fields of this struct, but we can regain it later (from the conceptual information we retain) by trying to downcast the `Any`. Then you get your static type information back and the compiler can help you again. > But both of those options are difficult or unidiomatic to write. Sorry, I hope I haven't come across too harsh to Clojure here. As I thought I was clear about above, Clojure's ergonomics for writing dynamically-typed code are vastly superior to Rust's. By coupling runtime type information to values and restricting itself to only being able to deal with values that are data and have runtime type data attached, Clojure gets to make a whole bunch of simplifying assumptions that reduce the work the programmer has to do when dealing with such values. That's the trade-off: Rust chooses to be able to express a much wider range of types by not requiring that coupling, but in exchange you have to be much more explicit when you do want to couple runtime type information to your values. Some languages like C# aim to be able to do both, i.e. start strongly typed and drop down ergonomically into dynamic typing as desired, but Rust is not one of those languages. > If we don't need to know the birthdate to calculate the white blood cell count, then we can exclude that field from the input type checking. But that very exclusion requires that you know enough about the value to know that it can be safely ‘excluded’ without having any additional information about it. Specifically you need to know: - how to access a subfield of the type regardless of the other fields on it — this requires that it contain RTTI - how to discard the value — this requires that it have a destructor with a known calling convention - how to move/copy the value into the function (and maybe even move out of the function if you return it or imperatively add it to some global state) — this requires that you know a ‘moving constructor’ for the value that can be used to safely move it to another location In the Rust case you need to write down these things explicitly so the compiler can make sure you don't pass a value that doesn't satisfy them. In Clojure, the reason you don't need to write them down is that every value in the language is restricted to only be able to represent such values, so those constraints are implicitly on every function that you write.