101–110 of 197 posts
Earlier quoted context omitted.
What, to you, is an ultra strong type system? Both OCaml and Haskell are used in plenty of non academic contexts. Do you mean something like Coq or F*?
"plenty" is relative. You don't see many GAFAM products created in either, and that's because of the trade off OP talks about.
Earlier quoted context omitted.
The Ceylon language allowed you to do that sort of thing with types. If you "added" two maps together of types `Map ` and `Map `, you would get back a `Map ` (or, equivalently, `Map | Map `). But for some slightly complex reasons, most language designers find adhoc union types (which are required for this to work) a bad idea. See the Kotlin work related to that, they explicitly want to keep that out of the language (…
> If you "added" two maps together of types `Map ` and `Map `, you would get back a `Map ` (or, equivalently, `Map | Map `). But these are obviously not equivalent: the first type is a map where all values are either strings or ints, and the second one is either a map where all values are strings, or all values are ints. If that's confusing, consider: {foo: 1, bar: "2"}. It satisfies `Map ` but not `Map | Map `. (In…
EDIT: ok, I just wanted to say that one type, `Map`, is a supertype of `Map | Map`, so if a function accepts the former, it also accepts the latter. They're not equivalent but you can substitute one for the other (one way only) and still perform the same operations (always assuming read-only types, if you introduce mutation everything becomes horrible).
I was trying to emphasize how having type "combinations" ends up causing the type system to become undecidable as you end up with infinite combinations possible, but as I haven't really gone too deeply into why, I am having trouble to articulate the argument.
Earlier quoted context omitted.
Typescript also does the former, albeit with less friendly syntax. X: 1 | 2 | 3 // …
Kinda but not really. It actually handles type inference on string concatenation, but doesn't understand math. type N = 1 | 2 const x1:N = 1 const x2:N = 1 const sum:N = x1 + x2 Typescript (the version running on my box) considers this an error.
I’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’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.
Even history of "required", rather simple restriction on the value, is showing that putting that logic into type system is too much of a burden.
https://capnproto.org/faq.html#how-do-i-make-a-field-require...
Earlier quoted context omitted.
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?
I’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.
Unfortunately, the more powerful the type system, the harder it is to make inferences. Generality comes at a cost.
types are not interfaces. interfaces describe behavior, types describe shape and structure. the difference is subtle but important.
I’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 regret to say that every type level Gordian knot that I have ever been exposed to came from attempts to do this. I think a lot of the problem is that many of the constraints and acceptable values for data are not determined until well after first deployment. The "knot" comes in when you are explicitly changing data and code to add a feature that you didn't anticipate at the start. This is a lot like schemaless data…
This is very similar to what Rich Hickey argued in "Simplicity Matters": https://youtu.be/rI8tNMsozo0?si=xTkpsLYTYh0jA5lB
Basically when you use a hash / JavaScript-style object rather than a fixed struct definition for your data (which amounts to a schema- less database in aggregate)
Easy addition of new properties
Co-existence of different versions of objects (newer objects will typically have more properties)
Introspection of properties and validation rules / reflection interface Timestamped {
timestamp: UTCTime;
}
interface Msg {
sender: PlayerId;
}
class Quote implements Timestamped, Msg {
timestamp: UTCTime;
sender: PlayerId;
}