Type systems are leaky abstractions: the case of Map.take!/2(dashbit.co)
dashbit.co
Type systems are leaky abstractions: the case of Map.take!/2
https://dashbit.co/blog/type-systems-are-leaky-abstractions-map-take
32 comments
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?
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?
The title is really quite an annoying abuse of the term "leaky abstraction".
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.
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.
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.
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)
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.
So, this is trying to tackle and type this instead.
It’s not wrong, just a different vision.
> The basis of Erlang/Elixir/Clojure is that structs are just inflexible maps.
I mean the difference is that Erlang and Elixir have high-quality pattern matching baked in, not to mention stuff like dialyzer and set-theoretic types.
Clojure has multi-methods I guess, and stuff like defrecord that no one uses...and the turd that is spec. In my experience every Clojure codebase turns into map soup at some point without a tremendous amount of manual labor.
...so it's not as black and white as you're saying, I guess is my point. And for example, I'd always take Haskell over Erlang or Elixir even though Haskell's records are widely and justifiably derided, because the language taken as a whole is that much nicer to use, and stuff like lens smooths some of the rough edges over pretty well.
I mean the difference is that Erlang and Elixir have high-quality pattern matching baked in, not to mention stuff like dialyzer and set-theoretic types.
Clojure has multi-methods I guess, and stuff like defrecord that no one uses...and the turd that is spec. In my experience every Clojure codebase turns into map soup at some point without a tremendous amount of manual labor.
...so it's not as black and white as you're saying, I guess is my point. And for example, I'd always take Haskell over Erlang or Elixir even though Haskell's records are widely and justifiably derided, because the language taken as a whole is that much nicer to use, and stuff like lens smooths some of the rough edges over pretty well.
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...)...
“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.
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.
Meaning, it's just as hard as no one following rules, but on top of that I get blindsided by expectations of security.
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.
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'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.
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.
> 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.
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.
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?
I think it's only fair to ask how you would apply that quote to your own preferred conventions.
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.
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.
Type systems are uncomposable leaning towers
I can't decide to use the PHP type system for some of my program then the Haskell type system elsewhere I can't combine them they're infectious they don't preserve well over the wire
They're often used for more than one purpose suboptimally
I'm either in 100% agreement with the language's type system or I'm unhappy in some aspects and so I'm unhappy with the language
People seem to choose their languages more on the type system than more fundamental aspects of their language
I think what most users want is static analysis and they don't understand how that is different from a type system they just assume you have to have a type system for static analysis
There's also no conversation about how complex a type system should be to support static analysis in fact some type systems are full blown turing complete
I think there's a more interesting conversation to be had around correctness in a collaborative environment that we're not having at large because type systems exist and consume the conversations
So language developers continue finding the perfect one that is a million little choices working together that must be perfect for everyone
It's a itch that will never be satisfied
I can't decide to use the PHP type system for some of my program then the Haskell type system elsewhere I can't combine them they're infectious they don't preserve well over the wire
They're often used for more than one purpose suboptimally
I'm either in 100% agreement with the language's type system or I'm unhappy in some aspects and so I'm unhappy with the language
People seem to choose their languages more on the type system than more fundamental aspects of their language
I think what most users want is static analysis and they don't understand how that is different from a type system they just assume you have to have a type system for static analysis
There's also no conversation about how complex a type system should be to support static analysis in fact some type systems are full blown turing complete
I think there's a more interesting conversation to be had around correctness in a collaborative environment that we're not having at large because type systems exist and consume the conversations
So language developers continue finding the perfect one that is a million little choices working together that must be perfect for everyone
It's a itch that will never be satisfied
> 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.
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.
> 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.
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.
This seems like a really easy problem to avoid by simply having a better type system and knowing how to use it. namely just have the take! function return an optional map where it returns Some(map) if the map has the expected keys and None if the map it would have returned in the non-asserting version wouldn't have been valid (I.e, wouldn't have had the expected keys). Then if you really want to assert on this, you just use .unwrap or .expect.
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
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
> just have the take! function return an optional map
A map of what ?
A map of what ?
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.