published…2024-09-17?
Sounds like someone needed a type that expresses "date no later than now".
Types as Interfaces
81–90 of 197 posts
Re: Types as Interfaces
#82Indeed, TypeScript can do exactly this and more, without much ceremony: type FooBar = Foo & Bar I doubt you will find a language where it is less clunky. Edit: Oh, I typed this on mobile, this was supposed to be a comment on another comment by posix_monad.
Typescript has a phenomenal type-system indeed. However, its foundations are not very sound. The types are pragmatic and that's what counts mostly, but going forward it would be great to have type-systems that are even more powerful and also theoretically sound with a simpler foundation (= less edge cases and workarounds). Languages like Idris are working on this. Typescript can't really be this language because it i…
What does "soundness" mean here? I love typescript's type system, except for the quirks that are inherited from javascript, which I sometimes find infuriating, and I'm wondering if you're talking about the same thing. For example, the fact that typescript- through javascript- only exposes a single `number` type is so annoying. Sometimes that's fine, but other times it would be nice to be able to say "No, this isn't just any damn number, this is an integer! This is an iterable ID for god's sake!" so you at the very least get a static error when you try to pass in `1.001`, or something that could be `1.001`. And that's just a very basic example of how a collection of number types with more granularity would be an improvement. Especially if they were a little more robust than that and were composable. Imagine being able to type `integer | negativeFloat` or other such wacky composed types. Ideally you could compose your types programmatically, and define shit like "the type is a `float` who's floor value has a % 3 of 0".
Re: Types as Interfaces
#83I’ve come to believe that a type should be capable of reflecting any arbitrary rules a programmer knows about the bounds of a value. The only real implementations of this I see are mostly academic with a dependent type system like Idris. We’re many years from that becoming mainstream, if it ever will be.
The benefits of such an approach would be substantial. However, nobody has gotten the costs down below "eye watering", or similar other metaphors. It's not that it can't be done, it's that it is not yet known if it can be done in a way that comes out positive on the cost/benefits engineering analysis. I am open to the possibility that it can, but at the same time, I'd say if I draw the trendline of progress in this a…
Slightly more optimistically: As we go along, small pieces go from "too expensive to actually use" to "usable on real projects, but nobody does yet", and then to "doesn't everybody do that?"
This is the story of improvements in type systems over the last 70 years. But the progress is very slow. So this is only slightly more optimistic...
Re: Types as Interfaces
#84Earlier quoted context omitted.
Not sure whether this is what you intended, but Go structs can embed other structs type Foo struct { foo int } type Bar struct { bar string } type FooBar struct { Foo Bar }
This doesn't function as an interface though. You cannot pass a FooBar to a function that expects a Foo, for example, and although you can fairly easily reference the Foo-part of a FooBar instance (`foobar.Foo`) there is no way to pass e.g. an array of FooBar instances to a function that takes a slice of Foo[] as its argument. That's the problem to be solved.
Totally achievable by using interfaces instead of structs
type Foo interface {
Foo() int
}
type Bar interface {
Bar() string
}
type FooBar interface {
Foo
Bar
}
Re: Types as Interfaces
#85meh. or you could use mixins.
Re: Types as Interfaces
#86I’ve come to believe that a type should be capable of reflecting any arbitrary rules a programmer knows about the bounds of a value. The only real implementations of this I see are mostly academic with a dependent type system like Idris. We’re many years from that becoming mainstream, if it ever will be.
I'm surprised that most popular languages don't even do simple type constraints. Like x: 1..100 y: "yes" | "no" I feel that there are lots of low hanging fruits when it comes to typing which would improve both program readability and correctness.
How would you ensure that the values of the types doesn't invalidate the contract? Easy for basic assignment, but not sure how you would do that when doing arbitrary mutation.
Re: Types as Interfaces
#87Indeed, TypeScript can do exactly this and more, without much ceremony: type FooBar = Foo & Bar I doubt you will find a language where it is less clunky. Edit: Oh, I typed this on mobile, this was supposed to be a comment on another comment by posix_monad.
Elixir is taking a similar direction if I'm understanding correctly (they seem to insist their type system is fundamentally from Typescript's, but to this day I cannot understand how, both are structural and based on set theory)
Is elixir's type system sound?
Re: Types as Interfaces
#88Earlier quoted context omitted.
I'm surprised that most popular languages don't even do simple type constraints. Like x: 1..100 y: "yes" | "no" I feel that there are lots of low hanging fruits when it comes to typing which would improve both program readability and correctness.
TypeScript does the latter. The former is difficult to track through arithmetic operations.
Typescript also does the former, albeit with less friendly syntax.
X: 1 | 2 | 3 // …Re: Types as Interfaces
#89Earlier quoted context omitted.
The benefits of such an approach would be substantial. However, nobody has gotten the costs down below "eye watering", or similar other metaphors. It's not that it can't be done, it's that it is not yet known if it can be done in a way that comes out positive on the cost/benefits engineering analysis. I am open to the possibility that it can, but at the same time, I'd say if I draw the trendline of progress in this a…
Slightly more optimistically: As we go along, small pieces go from "too expensive to actually use" to "usable on real projects, but nobody does yet", and then to "doesn't everybody do that?" This is the story of improvements in type systems over the last 70 years. But the progress is very slow. So this is only slightly more optimistic...
This is where I'd really be interested in seeing an AI system help. Don't write an AI system that helps me shovel out vast quantities of code, and then solves the problem of the resulting incomprehensible mass of code being impossible to work with by making it even easier to shovel out yet more masses of code to deal with the even larger masses of AI-generated code. It does not take a genius to see that this ends up with even the AIs being staggered by the piles of code in the world until all intelligences, natural and otherwise, are completely bogged down. (Exponential complexity growth defeats everyone in this physical universe, even hypothetically optimal AIs running on pure computronium.) Write me an AI that can help me drive something closer to Idris and bridge the gap between that overly-rigid world I'm complaining about and the more human/real-world goals I'm really trying to accomplish, have the AI and the programmer come to a meeting-of-the-minds and produce something with exactly the right rigidity in it, and help me reuse the results of other's work.
I mean... we're going to end up with the first one. But a man can dream. And while I will cynically say we're going to end up with the first one, it is at least possible that we will then recognize there's a problem and pursue this second approach. But not until the first approach bites us, hard.
Re: Types as Interfaces
#90Earlier quoted context omitted.
I empathize with this point of view - if not in any other way then in principle. However, as a counterpoint, I'd suggest that encoding all known invariants as types may be prohibitively cumbersome and time-consuming - to the point where writing the program becomes more of an exercise in proofs rather than producing something useful. Often the invariants of a program are implied or can be easily inferred by the reader…
The problem is that user inferring doesn't scale. For small projects this is reasonable but for enterprise software engineering it is easy for a constraint that isn't enforced by the type system to be missed by an engineer leading to a bug. Whereas typed constraints naturally propagate throughout the system.
Yeah - in theory they are the same thing. You can have a dependent type that's an array with a length of 5 or you can create a type called ArrayLengthFive, and in both cases the type checker ensures that you don't accidentally use an unbounded array.
But the difference is that with a dependent type, you get more guarantees (e.g. my ArrayLengthFive type could actually allow for arrays of length 20!). And the type checker forces you to prove the bounds (there could be a bug in my code when I create an ArrayLengthFive). And the dependent type allows other parts of the system to use the type info, whereas ArrayLengthFive is just an opaque type.
I do think there is room for both ways of working. In the string -> Email example, it's probably enough to parse your string and just call it an email. You don't need to try to encode all the rules about an email into the type itself. But there are certainly other cases where it is useful to encode the data constraints into the type so that you can do more operations downstream.