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.

At Dashbit, we help startups and enterprises adopt and grow their Elixir teams. We are the creators of Elixir, Nx, and Livebook, and we are the lead developers attempting to bring a set-theoretic type system to Elixir. We work with a limited number of clients and use our shared experiences to improve the Elixir ecosystem. Get in touch to learn how our team of experts can take your use of Elixir to the next level.

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: "[email protected]", age: 30}
iex> Map.take(user, [:name, :email])
%{name: "Alice", email: "[email protected]"}

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: "[email protected]", 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

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 possible violations could be caught by the type checker?

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: "[email protected]", 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. We want a type signature that tells us the exact shape of the return map, with its keys and possible values.

It is not possible to implement this function in many statically typed languages either, 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

So what are the possible ways forward?

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: "[email protected]", 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

After this article was published, @KenAKAFrosty suggested a different implementation for the take function which uses distributive conditionals, which is sound for the example above:

type TakeResult<T, Keys extends readonly (keyof T)[]> = Keys extends any ? Pick<T, Keys[number]> : never;

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

    for (const key of keys) {
        if (!(key in obj)) {
            throw new Error(`key "${String(key)}" not found in object`);
        }
        // minor type assertion is needed here because TypeScript
        // can't track dynamic assignment within distributive types
        (result as any)[key] = obj[key];
    }

    return result;
}

In a nutshell, when we refactored the snippet below

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

to share the keys variable, we were expecting take(user, keys1 | keys2) to be the same as take(user, keys1) | take(user, keys2), which is not always the case! Implementing distributive conditionals help address such cases, but at the cost of a much more complex type signature.

Even then, the types above do not make the signature airtight. If we slightly change our function to map over the keys before calling take, we are back to being unsound, even though the semantics are the same:

let keys;

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

keys = keys.map(x => x);
take(user, keys);

You can explore this new type signature in the playground.

Although the example is getting a bit more contrived, it shows how we can push the problem a bit further down the road by increasing the typing complexity, but also meaning that, when things break, it will become harder and harder to trace the root cause.

Alternatively, we could 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 we are certain the given keys exist!

Other attempts to solve this problem either require adding more typing complexity or by making type inference/checking more expensive, all which directly affect the developer experience. 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.