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

• José Valim
• March 3rd, 2026
• elixir , type system

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. In this article, we will discuss one of said examples by exploring a potential Map.take!/2 function as part of Elixir’s standard library.

Exploring the existing Map.take/2 function

In Elixir, our primary key-value data structure is called a map, and when using atom keys, maps behave as similar to what many programming languages would call “records”, which are key-value data structures where all fields are generally known upfront.

Elixir also has a function called Map.take/2, that accepts a map and a list of keys, and it returns a map with only the keys given to list of keys.

iex> user = %{id: 1, name: "Alice", email: "alice@example.com", age: 30}
iex> Map.take(user, [:name, :email])
%{name: "Alice", email: "alice@example.com"}

In Map.take/2, if you pass a key that does not exist, the key is ignored and not returned in the output map. However, when working with maps as records, we want to assert that the keys actually exist, hence a proposal to introduce Map.take!/2.

A proposal for Map.take!/2

Recently, Wojtek Mach proposed to add a Map.take!/2 to Elixir. In Elixir, the exclamation mark at the end implies the function may raise even when valid inputs are supplied. For example, File.read("foo") returns {:ok, contents} or {:error, reason}, but you can use File.read!("foo") if you expect the file to be there and, if it isn’t, all you can do is fail.

In this case, the goal of Map.take!/2 is to raise if one of the given keys are not part of the map. Something akin to:

iex> user = %{id: 1, name: "Alice", email: "alice@example.com", age: 30}
iex> Map.take!(user, [:name, :email, :missing])
** (KeyError) unknown key :missing

In Elixir (and other dynamic languages), implementing this function is relatively straight-forward, here is such implementation:

def take!(map, keys) when is_map(map) and is_list(keys) do
  Map.new(keys, fn key -> {key, Map.fetch!(map, key)} end)
end

On the other hand, it is not possible to implement this function in many statically typed languages, as this function effectively ranges over any keys of any record. In those situations, developers would be forced to write boilerplate functions per key combination (or per record), similar to below:

def take_name_and_email(user) do
  %{name: user.name, email: user.email}
end

def take_name_and_age(user) do
  %{name: user.name, age: user.age}
end

Since we are in the process of adding a type system to Elixir, one question arises: what would be the type signature of said Map.take! function and what exceptions could be caught during type-checking?

Note that we don’t expect all exceptions to be caught at compile-time. To recap a previous discussion on the topic, type systems used at scale today do not guarantee the absence of any runtime errors, but only typing ones. Many programming languages error when accessing the head of an empty list, most languages raise on division by zero or when computing the logarithm of negative numbers on a real domain, and others may fail to allocate memory or when unwrap is called. Nonetheless, it is still useful to understand how we would type it.

At the moment, the best type signature we could provide for the Map.take!/2 function above is:

$ map(), [term()] -> map()
def take!(map, keys) when is_map(map) and is_list(keys)

While the type signature above is not wrong, it is too broad. Nowhere it says the output is a subtype of the input map, nor the keys it has available, so we can’t do anything useful with its return type. Take this code:

user = %{id: 1, name: "Alice", email: "alice@example.com", age: 30}
Map.take!(user, [:name, :email])

According to the signature above, the return type is a map() and it doesn’t say anything about any of its keys. Therefore, we need to find a more precise definition for this function.

Enter TypeScript’s keyof

We can implement Map.take!/2 using TypeScript v5.9:

function take<T extends Record<string, any>, K extends keyof T>(
  obj: T,
  keys: readonly K[]
): Pick<T, K> {
  const result = {} as Pick<T, K>;

  for (const key of keys) {
    if (!(key in obj)) {
      throw new Error(`key "${String(key)}" not found in object`);
    }
    result[key] = obj[key];
  }

  return result;
}

The key - pun intended - to make this work is the keyof operator. With the function above, we can now write:

const user = { id: 1, name: "Alice", email: "alice@example.com", age: 30 };
const subset = take(user, ["name", "email"]);

and if you attempt to call subset.id, TypeScript will emit a typing violation, which is what we expect! But unfortunately, the signature above just works on the simplest of cases.

For example, imagine that in some cases you need to return a subset with keys “name” and “email”, and in other cases, you need to return “name” and “age”. I am using Math.random < 0.5 in the example below to exemplify this condition, but it could be any domain logic. Then you could write this:

if(Math.random() < 0.5) {
  return take(user, ["name", "email"]);
} else {
  return take(user, ["name", "age"]);
}

The code above will type check just fine and emit this type signature:

Pick<{
  id: number;
  name: string;
  email: string;
  age: number;
}, "name" | "email"> | Pick<{
  id: number;
  name: string;
  email: string;
  age: number;
}, "name" | "age">

If you attempt to access user.email on the type above, it will correctly emit a typing violation, as only one of the entries in the union have the email key.

However, let’s say that you decide to refactor the code above, so you call take only once:

let keys;

if(Math.random() < 0.5) {
  keys = ["name", "email"];
} else {
  keys = ["name", "age"];
}

return take(user, keys);

For all intents and purposes, the two versions are meant to be the same. However, the new version no longer type checks because the keys are inferred as string[].

I find this to be problematic because sometimes type systems work against best practices. Refactoring code, removing duplication, and encapsulating logic all lead to improvements to the code, but sometimes they can’t be implemented because they can’t be verified. 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).

Finding unsoundness

One potential alternative, suggested by justdev, is to use as const:

let keys;

if(Math.random() < 0.5) {
  keys = ["name", "email"] as const;
} else {
  keys = ["name", "age"] as const;
}

take(user, keys);

However, this function will return the type:

Pick<{
  id: number;
  name: string;
  email: string;
  age: number;
}, "name" | "email" | "age">

which is broader (aka less precise) than our original type, as it says it may return a combination of all three keys, while in practice, it is either name & email or name & age. At a further glance, this is clearly the wrong type signature, as we cannot actually guarantee both “email” and “age” fields will be there! We say this type is unsound, as the program once executed returns a value outside of its type.

Here is a playground if you want to play with the TypeScript code above. If you change the snippet to compute take(user, keys).email, it will say the result type is string, but once you execute the program, sometimes it will return a string, sometimes it will return undefined. Therefore, the values we see at runtime do not match type system signature, and we got no typing errors either! Given this signature is ultimately unsound, it wouldn’t be allowed in Elixir’s type system.

Paths to soundness

As far as I know, the only way to implement a sound version of take in TypeScript is to say the fetched keys are optional in the returned type. To see why this is the case, imagine that TypeScript’s take is called with these types:

take(user, ("name" | "age")[])

Where ("name" | "age")[] represents a list with “name” or “age”. This represents the following inputs and output at runtime:

take(user, [])              // {}
take(user, ["name"])        // { name: "Alice" }
take(user, ["age"])         // { age: 30 }
take(user, ["name", "age"]) // { name: "Alice", age: 30 }

In other words, once we say ("name" | "age")[], we have no guarantees which keys will actually be present, because the Array type itself does not include this information. It could be none, it could be both!

One way to solve this would be to have a more expressive representation for list/array types, one that could make a distinction between lists where both “name” and “age” must exist compared to a list where “name” and “age” may exist. While this makes the type system more precise, it comes at the cost of additional complexity. And, even then, it would not be enough to type the conditional Math.random() > 0.5 from the previous section (we could discuss ways of solving the conditional problem but those solutions would either introduce even more complexity or break at a future point too).

Another option is to indeed accept our list/array types are not precise enough, and therefore, once you take a list of keys, we cannot effectively assume any of the keys will be there. In TypeScript, this could be done by marking the return type of our take implementation as Partial<Pick<T, K>>. 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 the given keys exist!

So we are back to a sound and correct implementation, but the returned type still isn’t particularly useful. Is there anything else that could be done?

Macros for the rescue?

One option is to convert Map.take!/2 into a macro! By using a macro, Elixir could statically guarantee that the argument is a list of keys and generate the expanded code. Intuitively, instead of writing a bunch of boilerplate clauses, such as:

def take_name_and_email(user) do
  %{name: user.name, email: user.email}
end

def take_name_and_age(user) do
  %{name: user.name, age: user.age}
end

The user could invoke Map.take!(user, [:name, :age]), which would expand to %{name: user.name, age: user.age}, which the type system can correctly infer a precise result for! No type signatures necessary!

Curiously, the macro allows developers to enforce the limitations we have seen in the previous typing signatures. Our previous typing signatures for take were correct whenever the list of keys were given statically, something macros can enforce. Passing any other expression as the list of keys fails to compile.

This is not a new approach and it has been explored in other programming languages, such as Racket. Another good example of how macros could complement types is on operations such as printf, which cannot be trivially typed:

printf("Your integer is: %d, your string is: %s", an_integer, a_string)
printf("Your string is: %s, your integer is: %s", a_string, an_integer)

If printf is implemented as a macro, that requires the first argument to be a string at compile-time, then it could expand printf into code that enforces the desired types! For example, in Elixir, the first printf above could become the following (note <> is used for binary/string concatenation in Elixir):

"Your integer is: " <> Integer.to_string(an_integer) <> ", your string is: " <> a_string

However, we must ask ourselves: do we want to push developers to write macros to address limitations in our type systems? Or should we rejoice in the possibility?

Summing up

Dynamic programs are expressive and can be correct, but we can’t always statically verify them with our type systems. Many times these programs tend to be dismissed as “if you can’t type check it, it is bad code” but this article shows how such programs can arise when performing simple refactorings or when encapsulating shared functionality.

In particular, this article uses a Map.take!/2 function as one of many possible examples. Such cases are frustrating because, while the code is correct and can be verified with other techniques, such as testing, it fails to type in subtle ways that can only be understood by digging deep into the type system!

Studying those programs can be useful to discuss trade-offs in language design. On one side, one can decide to not support such constructs, keeping the host language simple, but leading to a lack of expressiveness and to an increase in boilerplate code. On the other hand, the language can add new typing abstractions,but increasing the language surface and its complexity. Macros and other language features could be used as a escape hatch, but they also come with pros and cons.

At the end of the day, I hope this article provides insights on adopting type systems for existing dynamic languages, and brings more nuance to discussions around static vs dynamic typing.