The article's summary is fair, but the title is IMO a bit of a click bait, because the problem as described really is that "shoehorning a richer type system atop an Any-typed language is leaky." The Any type leaks through. The principle that a Map from Any to Any is the only data structure of note leaks through.

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.

The author doesn't understand what a leaky abstraction is:

He writes:

"And in order to understand why that’s the case, you need to start digging into the workings of the type system (hence a leaky abstraction)."

Then he proceeds to just write more Typescript without dropping down to reading the Typescript compiler source code, which is what generally happens when you have to deal with a leaky abstraction.

When you have an ORM that generates SQL, but you have to read the generated SQL for performance reasons (N+1, etc), that's a leaky abstraction. The details end up leaking through.

This doesn't work with Typescript, since Typescript types don't appear in the generated Javascript code. The type system doesn't try to hide an underlying system that could possibly leak through. The type system is a new thing that wasn't there before.

What's particularly annoying about the blog post is that the topic at hand actually has very little to do with type systems. It's primarily about compile time evaluation of code. The keys needed for map access need to be known at compile time and by threading them through an if(Math.random() < 0.5), or a keys = keys.map(x => x); the compiler would have to evaluate every possible code path symbolically to generate a type signature. After all, the code could have been keys.map(x => x + "abc") or any other arbitrary expression that can be evaluated at compile time.

The compiler doesn't really give a damn about the types here, because they are kind of irrelevant and crystalize out of the results of compile time evaluation. keys.map(x => x) and keys.map(x => x + "abc") both take a list of strings and output a list of strings. The types are exactly as you expect, but the concrete values are different.

The only way out of this with a type system would be to encode values into the type system itself, which is kind of antithetical to the idea of typing.

Honestly I got hung up on understanding why for Typescript the declaration of `keys` shouldn't be:

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?

Surely type checking on the keys of effectively arbitrary maps is just a folly. Maps shouldn’t be used for these purposes. If you know the members at compile time, then put them in a proper record type, like a struct or dataclass, etc.

I dream of a day when everyone is using statically typed languages that support row polymorphism a la PureScript (https://book.purescript.org/chapter4.html#record-patterns-an...)...

Right - it feels like going skin deep on types and then complaining they didn't solve for very deep problems.

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)

The basis of Erlang/Elixir/Clojure is that structs are just inflexible maps.

So, this is trying to tackle and type this instead.

It’s not wrong, just a different vision.

“Every institution perishes by an excess of its own first principle.” - Lord Acton

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.

Every time I've interacted with optional type systems, it feels like I'm driving in a road where only 50% of the drivers follow the rules.

Meaning, it's just as hard as no one following rules, but on top of that I get blindsided by expectations of security.

I've worked with both Java and Python extensively. Python's type system is far more exhausting, tbh. You have to think about types in both languages, but at least in Java, the compiler and static analysis can tell you if there are type-related issues. In Python, runtime errors. Anything larger in Python becomes a nightmare to work with because you basically never know for sure what's being passed into a function without excessive type checking and testing.

And you can never mandate that optional type checking in a big enough team.

You can even see popular FOSS Python packages that have very limited type checking.

Why not? Have mypy/pyright/pryefly/ty type errors break CI. If you're starting a new project, there's no reason you shouldn't.

> Have mypy/pyright/pryefly/ty type errors break CI.

Only if types are present.

> If you're starting a new project, there's no reason you shouldn't. Most dependencies would still be untyped.

> Only if types are present.

Make sure they are. Set no implicit any in your type checker, and use a linter to ensure every function has type annotations.

> Most dependencies would still be untyped

Most is a big exaggeration. I understand it's dependent on the domain, but only a small subset of the ones I use in my projects are untyped, and you can write typed wrappers when necessary.

Also, perfect is the enemy of the good. I'd rather have a 90% typed codebase and work around untyped dependencies than abandon the idea at all.

Not to sound harsh, but it sounds like you're greenfielding most projects and don't have to worry about collaborating with a large dev team or onboarding new developers which is a luxurious position to have. It's been the exact inverse for me where getting up to speed or maintaining a python codebase is exhausing and maintaining rust/go/typescript projects has been much less of a burden.

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.

I think it's only fair to ask how you would apply that quote to your own preferred conventions.

    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.

That seems vanishingly unlikely next to the potential of using strongly typed, verifiable-at-compile-time languages.

If humans move further and further away from actual code, what do they care what language the product is made in?

> People seem to choose their languages more on the type system than more fundamental aspects of their language

The type system constraints *are* the most fundamental issue and the majority of the focus of any programming language designer.

On another note I would even add that this:

> Adding a type system to an existing dynamic language is a great exercise in showing all of the different ways type systems restrict the expressive power of programming languages.

Is a pro, not a con as the author makes it sound.

Most people want simple stupid predictable and readable code they need to change to pay their bills.

If people want expressiveness they can install their lisps or other languages full of macros and extensions.

Languages that unsurprisingly have never scaled despite how many fans they have: every single author reinvents the wheel, writes its own DSLs, reinvents their own patterns.

Haskell is also plagued by this, by allowing compiler extensions jumping from project to project is a pain, reading code in textual form is a pain, you consistently need compiler or runtime support.

> just have the take! function return an optional map

A map of what ?

No, I don't think that a better type system would help with this.

The problem here is that the blog post would be more appropriately titled "How far can we go with compile time evaluation of field symbols [0]?" Field symbols and collections of field symbols would need to be a first class feature in the language whose compile time evaluation is well defined.

[0] symbols = think Ruby symbols

So if we pretend a list is a function from an index to an entry for the moment ``` Enum.take(list , 2) ``` Is more like ``` Enum.take(list, [1,2]) ``` So if you apply that to a list of length 1 or zero, you just get either list[1], or []

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.

> Unfortunately, this decision completely defeats the purpose of adding a function similar to Map.take!, as the goal of the function is to return a map where we are certain the given keys exist!

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.

That particular contrived example is another case of "Map Any to Any is the only data structure" leaking into the thinking about types. If there's two alternatives, use an algebraic data type to express that.

I think his point was any logic branch which branches on any state injected by the world outside of the compilation scope.