FRESH

Hacker News

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

46 points by tosh

by codebje

2 subcomments

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.

by Xophmeister

2 subcomments

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.

by slifin

1 subcomments

by travisgriggs

5 subcomments

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

by logicprog

2 subcomments

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.

by foxes

0 subcomment

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.

by mcphage

2 subcomments

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

by stainlu

0 subcomment

by useftmly

0 subcomment