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.
Sorry, perhaps I'm being a little obtuse. What I'm ultimately trying to get at is that sometimes its useful to have different types for the same data under different circumstances. A subset of data might benefit from a narrower type.
For example, suppose we have some CSV file that contains a bunch of patient information, including average white blood cell count and birthdate. This CSV file might contain bad data! So perhaps we type it as:
This covers all our bases, but it's also somewhat annoying to work with. Perhaps we only want to find patients with WBC counts outside a certain range, and discard those lines where the data is invalid. In which case, we could write a narrower type, and simply not parse the CSV rows that are invalid:
So in this case we have a couple of options for types. The latter type decouples the birthdate (it's never even parsed), but adds the restriction that the WBC count needs to be numerical; while the former type is a more accurate representation of the CSV file overall, but has greater coupling.
Obviously which we use depends on the nature of our program, but what I'm trying to get at is that a type isn't set in stone, but something we choose. Ideally we choose the most restrictive and decoupled type for the circumstances, but that might result in having many hundreds of different variations of the same type, so there's a tension between the number of distinct types and how specific or narrow they are.
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.
Granted, but Clojure's approach can result in greater decoupling with less effort, particularly when dealing with imperfect data.
In the previous examples I presented a scenario where we might want to think carefully about how exactly we store data that might contain invalid fields. But in Clojure we don't care - we can quite easily have a data structure that's partially invalid or unparsed - the entire problem of how we represent this data in memory is sidestepped.
We can still define what constitutes valid fields:
But these schema definitions are independent of the type system (i.e. decoupled), so we can apply them selectively or not at all. We can say "this function requires patient data with valid birthdates and WBC counts, but we don't care about any other field".
Could you do the same in Rust or other similar languages? Sure, it's ultimately just maps and predicates. But many languages aren't geared up to make that pleasant to use.
Perhaps we only want to find patients with WBC counts outside a certain range, and discard those lines where the data is invalid. In which case, we could write a narrower type, and simply not parse the CSV rows that are invalid:
These two types aren't typing the same data, though: in the latter case (in Rust) you've actually thrown away some of the data, and the type reflects that. In some languages like Clojure or TypeScript you can't distinguish that from the case where you haven't actually thrown away the data and are secretly carrying it around as well as whatever data is explicitly typed there, but if you want to get it back you have to know that it was once there, i.e. have additional (conceptual) type information that you chose not to write down.
Granted, but Clojure's approach can result in greater decoupling with less effort, particularly when dealing with imperfect data.
I think this isn't a great comparison: the usual vehicle for this thing in Rust is the trait, which manages to abstract over the representation statically without introducing a bunch of runtime machinery for it (though you can opt in to the machinery by using a trait object!). That's very idiomatic in Rust, although the trait syntax is a bit noisier (because it's more general).
the entire problem of how we represent this data in memory is sidestepped.
It's not sidestepped — the language just makes an opinionated choice for you, which you can't avoid.
these schema definitions are independent of the type system (i.e. decoupled), so we can apply them selectively or not at all
These are just predicates; I don't think they have much to do with this discussion? They don't help you to type your data: you (the programmer) still have to carry that type information around in your head in order to work with the values even after they are validated.
Could you do the same in Rust or other similar languages? Sure, it's ultimately just maps and predicates. But many languages aren't geared up to make that pleasant to use.
There are good reasons for that, though. Nominal typing allows you to express and enforce constraints that aren't necessarily enforced by the structure of the type, at the cost of some extra ceremony. And systems languages often want to be able to express types that cannot be treated this way: types in which there is no sensible way to ‘ignore’ a value. Clojure makes some things easier to write by forcing you to carry around a bunch of extra stuff (both runtime data and static semantics) with all your values; that's a perfectly valid choice that makes an important subset of programs nicer to write, but it also excludes values that don't fit into that category or can't reasonably be coupled to their RTTI.
As we get better at writing compilers we're increasingly seeing a move towards mechanisms like Rust's traits or C++'s concepts that allow the programmer to actually abstract over the representation of a type (as opposed to forcing a uniform representation as is common in dynamically typed languages). If you do that well you can get the best of both worlds semantically, but these kinds of systems languages will always be a bit heavier syntactically because the syntax needs to support a wider range of types.
These two types aren't typing the same data, though: in the latter case (in Rust) you've actually thrown away some of the data, and the type reflects that.
In Clojure the data is thrown away too, just at a slightly later point. The data is parsed then destructured then processed, and it is at the destructuring stage that irrelevant data is discarded and marked for GC.
Just as the Rust function avoids coupling by using a more narrow type, the Clojure function avoids coupling by using a more narrow binding.
I think this isn't a great comparison: the usual vehicle for this thing in Rust is the trait, which manages to abstract over the representation statically without introducing a bunch of runtime machinery for it
But you have to create and implement those traits. I'm not saying this is impossible in Rust; just a lot more onerous because you don't get all the machinery Clojure has that makes it trivial.
These are just predicates; I don't think they have much to do with this discussion?
This might be why we're talking past each other. When I say "type", I mean a set of possible values. I don't think this is an uncommon definition; the first sentence of the "data type" Wikipedia page pretty much defines it the same way.
Given this definition, you perhaps see why we can narrow a runtime type by composing it with a predicate.
My understanding is that you view types differently, as more of an interpretation of some sequence of bits, rather than a set of data values. Is that correct?
As we get better at writing compilers we're increasingly seeing a move towards mechanisms like Rust's traits or C++'s concepts that allow the programmer to actually abstract over the representation of a type (as opposed to forcing a uniform representation as is common in dynamically typed languages).
I agree that's there's no reason in principle that you couldn't statically type it with a sufficiently advanced compiler.
Comments
Sorry, perhaps I'm being a little obtuse. What I'm ultimately trying to get at is that sometimes its useful to have different types for the same data under different circumstances. A subset of data might benefit from a narrower type.
For example, suppose we have some CSV file that contains a bunch of patient information, including average white blood cell count and birthdate. This CSV file might contain bad data! So perhaps we type it as:
This covers all our bases, but it's also somewhat annoying to work with. Perhaps we only want to find patients with WBC counts outside a certain range, and discard those lines where the data is invalid. In which case, we could write a narrower type, and simply not parse the CSV rows that are invalid: So in this case we have a couple of options for types. The latter type decouples the birthdate (it's never even parsed), but adds the restriction that the WBC count needs to be numerical; while the former type is a more accurate representation of the CSV file overall, but has greater coupling.Obviously which we use depends on the nature of our program, but what I'm trying to get at is that a type isn't set in stone, but something we choose. Ideally we choose the most restrictive and decoupled type for the circumstances, but that might result in having many hundreds of different variations of the same type, so there's a tension between the number of distinct types and how specific or narrow they are.
Granted, but Clojure's approach can result in greater decoupling with less effort, particularly when dealing with imperfect data.
In the previous examples I presented a scenario where we might want to think carefully about how exactly we store data that might contain invalid fields. But in Clojure we don't care - we can quite easily have a data structure that's partially invalid or unparsed - the entire problem of how we represent this data in memory is sidestepped.
We can still define what constitutes valid fields:
But these schema definitions are independent of the type system (i.e. decoupled), so we can apply them selectively or not at all. We can say "this function requires patient data with valid birthdates and WBC counts, but we don't care about any other field".Could you do the same in Rust or other similar languages? Sure, it's ultimately just maps and predicates. But many languages aren't geared up to make that pleasant to use.
These two types aren't typing the same data, though: in the latter case (in Rust) you've actually thrown away some of the data, and the type reflects that. In some languages like Clojure or TypeScript you can't distinguish that from the case where you haven't actually thrown away the data and are secretly carrying it around as well as whatever data is explicitly typed there, but if you want to get it back you have to know that it was once there, i.e. have additional (conceptual) type information that you chose not to write down.
I think this isn't a great comparison: the usual vehicle for this thing in Rust is the trait, which manages to abstract over the representation statically without introducing a bunch of runtime machinery for it (though you can opt in to the machinery by using a trait object!). That's very idiomatic in Rust, although the trait syntax is a bit noisier (because it's more general).
It's not sidestepped — the language just makes an opinionated choice for you, which you can't avoid.
These are just predicates; I don't think they have much to do with this discussion? They don't help you to type your data: you (the programmer) still have to carry that type information around in your head in order to work with the values even after they are validated.
There are good reasons for that, though. Nominal typing allows you to express and enforce constraints that aren't necessarily enforced by the structure of the type, at the cost of some extra ceremony. And systems languages often want to be able to express types that cannot be treated this way: types in which there is no sensible way to ‘ignore’ a value. Clojure makes some things easier to write by forcing you to carry around a bunch of extra stuff (both runtime data and static semantics) with all your values; that's a perfectly valid choice that makes an important subset of programs nicer to write, but it also excludes values that don't fit into that category or can't reasonably be coupled to their RTTI.
As we get better at writing compilers we're increasingly seeing a move towards mechanisms like Rust's traits or C++'s concepts that allow the programmer to actually abstract over the representation of a type (as opposed to forcing a uniform representation as is common in dynamically typed languages). If you do that well you can get the best of both worlds semantically, but these kinds of systems languages will always be a bit heavier syntactically because the syntax needs to support a wider range of types.
In Clojure the data is thrown away too, just at a slightly later point. The data is parsed then destructured then processed, and it is at the destructuring stage that irrelevant data is discarded and marked for GC.
Just as the Rust function avoids coupling by using a more narrow type, the Clojure function avoids coupling by using a more narrow binding.
But you have to create and implement those traits. I'm not saying this is impossible in Rust; just a lot more onerous because you don't get all the machinery Clojure has that makes it trivial.
This might be why we're talking past each other. When I say "type", I mean a set of possible values. I don't think this is an uncommon definition; the first sentence of the "data type" Wikipedia page pretty much defines it the same way.
Given this definition, you perhaps see why we can narrow a runtime type by composing it with a predicate.
My understanding is that you view types differently, as more of an interpretation of some sequence of bits, rather than a set of data values. Is that correct?
I agree that's there's no reason in principle that you couldn't statically type it with a sufficiently advanced compiler.