Like yes, it would be nice for Map(ICar[] cars, keys).wingspan to throw a type error because cars is typed and we know keys can't include things not in ICar.
But to say that Map(Any[] things, keys) should have ahead of time type checking seems like you're not really using types except when inconvenient. Which might be taken as a no true scotsman or "holding it wrong" argument but... Maybe they are holding it wrong.
(Speaking as a former Windows/CLR PM now working in a Ruby monolith... It's hell and indeed trying to add types via sorbet has been miserable and useless)
So, this is trying to tackle and type this instead.
It’s not wrong, just a different vision.
Trying to make that work for static validation requires dependent typing: the type of the result depends on the term passed in. Or, you could use row types, record types, or any of the other data structures richly typed languages use at their core to be more expressive of intent than just a Map from Any to Any.
let keys = (keyof typeof users)[]
Like I get it's a contrived example and maybe I'm missing some nuance to it, but if we're obsessed with type-safety why are we treating a array of strings as an array of keys (which are more like atoms)?
I thought the answer might be we're looking for duck typing-ish behavior, but then the proposed take signature doesn't work either?
For the reasons explored in the post, I prefer my type systems optional. It has been my experience and observation that typing in languages follow an 90:10 rule. You get 90% of the gains for 10% of the effort. And the remaining 10% for 9x the effort.
I’m rather happy with the way Python allows me to do the easy ones and/or pick the hotspots.
I’ve worked in exhaustively typed languages, and while it gives a sense of safety, it’s literally exhausting. And, anecdotally, I feel I dealt with more zero divides, subscript woops, and other runtime validation errors than I had in less typed languages.
Not that it matters. Soon, we’ll use semantically vague human language, to prompt, cajole, nudge LLM agents to produce programs that are (lossy) statistical approximations of what might be correct programs.
Meaning, it's just as hard as no one following rules, but on top of that I get blindsided by expectations of security.
You can even see popular FOSS Python packages that have very limited type checking.
Any time I've worked on a python codebase with 3 or more people on a reasonably sized project, it turns into a mess than becomes much more of a cognitive load than any compiled language. Here are my experiences:
- numerous lsp errors and warnings that drown out real bugs and issues (no one is null checking in python, or correctly typing their functions beyond the primitive types)
- hodgepodge of tools like conda, python version <= 3.5, etc. required for project (because one person refuses to migrate to uv)
We've seen the exact opposite trend of what you've said. Typescript has surged in popularity because the quality of LLM output scales with context, and untyped languages like python/JS leave most of that context out that no machine can parse. These tools do not reason. They are token generators. Pure functions. Some outputs have more weight than others.
Soon, we’ll use semantically vague human language, to prompt, cajole, nudge LLM agents to produce programs that are (lossy) statistical approximations of what might be correct programs.
If humans move further and further away from actual code, what do they care what language the product is made in?
The difference is that Enum is maybe a total function - the domain of the function is always well defined, while Map take is trying to be dressed up as a total function but its really something thats only partial.
So the type system needs a way to describe a map that has "at least these keys" a bit like the enum case. So that requires some polymorphism.
I mean, if you define a function calling Map.take! that returns one of two possible set of keys based on a random number, I’m not sure it’s actually possible to get a map where you’re certain what keys exist.