Type systems are leaky abstractions: the case of Map.take!/2

▲ Type systems are leaky abstractions: the case of Map.take!/2(dashbit.co)

44 points by tosh 4 days ago | 19 comments

▲ Xophmeister 5 hours ago | parent | next [-]

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.

	▲	hirsin 4 hours ago \| parent \| next [-]
		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)
	▲	jiehong 3 hours ago \| parent \| prev [-]
		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.

▲ codebje 5 hours ago | parent | prev | next [-]

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.

	▲	andrewflnr 4 hours ago \| parent \| next [-]
		The title is really quite an annoying abuse of the term "leaky abstraction".
	▲	BoorishBears 4 hours ago \| parent \| prev [-]
		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?

▲ travisgriggs 7 hours ago | parent | prev | next [-]

“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.

▲ kace91 6 hours ago | parent | next [-]

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.

▲ HauntingPin 6 hours ago | parent | prev | next [-]

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.

▲

ashishb 5 hours ago | parent [-]

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.

	▲	maleldil 5 hours ago \| parent [-]
		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.

▲ waterTanuki 3 hours ago | parent | prev | next [-]

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.

▲ mpalmer 5 hours ago | parent | prev | next [-]

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

▲ mpalmer 5 hours ago | parent | prev [-]

    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?

▲ logicprog 7 hours ago | parent | prev | next [-]

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.

▲ foxes 7 hours ago | parent | prev | next [-]

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.

▲ mcphage 8 hours ago | parent | prev [-]

> 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.

	▲	codebje 3 hours ago \| parent \| next [-]
		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.
	▲	travisgriggs 7 hours ago \| parent \| prev [-]
		I think his point was any logic branch which branches on any state injected by the world outside of the compilation scope.