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

José Valim explores the limitations of type systems through the lens of a proposed Map.take!/2 function in Elixir. The function takes a map and a list of keys, returning only those keys while raising if any are missing. While trivial to implement in a dynamic language, typing it precisely proves difficult: a broad map() return type loses all key information, and TypeScript's keyof/Pick approach breaks down when keys are computed conditionally rather than inlined. Refactoring the inline calls into a variable causes TypeScript to widen the type to string[], losing precision. Using 'as const' restores some precision but introduces unsoundness — the type claims keys may be present that aren't guaranteed at runtime. The only sound alternative returns Partial types, defeating the function's purpose. Macros are proposed as an escape hatch: by requiring the key list to be a compile-time literal, the macro can expand to precise record access expressions the type system can verify. The post concludes that dynamic programs can be correct yet unverifiable by type systems, and that adding types to dynamic languages involves real trade-offs between expressiveness, boilerplate, and type system complexity.