The Nix expression language has been dynamically typed since it was designed in 2003, and that has never quite been comfortable. Nix’s primary data structure, the attribute set, is an unordered string-keyed map. Functions accept attrsets, return attrsets, merge attrsets, and destructure them. The entire NixOS configuration surface is attrsets all the way down. Without static types, the best you get is a runtime error when evaluation reaches a type mismatch, which in a lazy language can happen long after the mismatched value was defined.
typenix takes an unusual approach to this problem: rather than building a new type checker, extending the Nix parser, or designing a whole new language, it encodes Nix types as TypeScript types and lets the TypeScript compiler do the checking. The TypeScript toolchain handles inference, error reporting, and IDE integration. typenix just has to map Nix’s type semantics onto TypeScript’s type system, which turns out to be expressive enough to cover most of the ground.
Why Typing Nix Is Hard
Before getting into how typenix works, it helps to understand what makes Nix resistant to static typing. The surface problems are easy to see; the deep ones are less obvious.
The with statement is one of the deep problems. with pkgs; [ git vim curl ] injects all attributes of pkgs into lexical scope. To statically check whether git is a valid name, a type checker needs to know the full shape of pkgs at the point of the with, which in practice means evaluating pkgs partially or tracking its type across module boundaries. Hindley-Milner inference, the basis of most functional language type systems, cannot handle this without substantial extensions.
The callPackage pattern is another hard case. In nixpkgs, packages are defined as functions that take their dependencies as named arguments:
# hello/default.nix
{ stdenv, fetchurl, lib }:
stdenv.mkDerivation rec {
pname = "hello";
version = "2.12";
src = fetchurl {
url = "mirror://gnu/hello/hello-${version}.tar.gz";
sha256 = "1ayhp9v4m4rdhjmnl2bq3cibrbqqkgjbl3s7yk2nhlh8vj3ay16g";
};
}callPackage inspects the function’s argument names at runtime using builtins.functionArgs, then supplies matching values from the package set. Typing this correctly requires dependent types or something like row polymorphism, because the function’s required inputs are determined by the shape of its argument list, which is itself a value the type system would need to inspect.
Dynamic attribute access compounds this further: set.${dynamicKey} accesses an attrset with a key known only at runtime. A type system conservative enough to reject this would break enormous amounts of existing nixpkgs code.
The NixOS module system does provide runtime type checking for configuration options, using types like lib.types.str, lib.types.listOf lib.types.int, and lib.types.submodule. These are attrset values with a check function field, evaluated during nixos-rebuild. They are not static types; they are runtime contracts. They work well for the NixOS configuration surface but do not cover package definitions or arbitrary Nix library code.
What typenix Does
typenix’s core insight is that TypeScript’s type system is structurally typed, recursive, and Turing-complete through conditional and mapped types. Nix’s semantics, especially the straightforward parts, map onto TypeScript types directly.
An attribute set in Nix is a string-keyed record with typed values. TypeScript’s object types are exactly that:
// Nix: { name = "hello"; version = "2.12"; isFree = true; }
type HelloAttrs = {
name: string;
version: string;
isFree: boolean;
};A Nix lambda is a single-argument function, represented in TypeScript as a function type:
// Nix: x: x + 1
type Increment = (x: number) => number;Nix lists become typed arrays or tuples:
// Nix: [ 1 2 3 ]
type IntList = number[];
// Nix: [ 1 "hello" true ] (heterogeneous)
type Mixed = [number, string, boolean];The // operator, which merges two attrsets with right-hand values taking precedence, maps to a TypeScript mapped type:
type NixMerge<L, R> = Omit<L, keyof R> & R;
type Base = { name: string; version: string; meta: object };
type Override = { meta: { description: string }; patches: string[] };
type Result = NixMerge<Base, Override>;
// Result: { name: string; version: string; meta: { description: string }; patches: string[] }This is structurally correct: Result has name and version from Base, meta from Override (overriding Base’s meta), and patches from Override.
TypeScript’s structural subtyping also lines up well with how Nix functions consume attrsets. A Nix function that destructures { stdenv, lib, ... } accepts any attrset with at least stdenv and lib attributes; the ... catches the rest. In TypeScript, a function accepting { stdenv: Stdenv; lib: Lib } is compatible with any object that has at least those fields, which is structural subtyping by definition.
The TypeScript Features That Make This Work
Three TypeScript features do most of the heavy lifting.
Conditional types, introduced in TypeScript 2.8, enable type-level branching:
type NixTypeOf<T> =
T extends string ? "string" :
T extends number ? "int" | "float" :
T extends boolean ? "bool" :
T extends null ? "null" :
T extends any[] ? "list" :
T extends object ? "set" :
T extends (...args: any[]) => any ? "lambda" :
never;This mirrors builtins.typeOf at the type level. The infer keyword inside conditional types extracts components of composite types, which is useful for modeling function signatures:
type ArgType<F> = F extends (arg: infer A) => any ? A : never;
type RetType<F> = F extends (...args: any[]) => infer R ? R : never;Mapped types let you transform every key in an object type, covering operations like builtins.mapAttrs:
type MapAttrs<T, F extends (k: string, v: any) => any> = {
[K in keyof T]: F extends (k: K, v: T[K]) => infer R ? R : never;
};Template literal types, added in TypeScript 4.1, handle string interpolation:
type NixInterpolate<Prefix extends string, Value extends string> =
`${Prefix}${Value}`;
type Version = "2.12";
type TarballName = NixInterpolate<"hello-", Version>;
// TarballName = "hello-2.12"These three features combine to make TypeScript’s type system Turing-complete. Projects like ts-sql have implemented full SQL parsers in TypeScript types alone. typenix operates in the same space: using TypeScript as a meta-programming substrate where the “program” being run is type inference over Nix expressions.
Where It Breaks Down
The hard Nix constructs are hard for the same reason they resist every typing approach: they require the type checker to reason about values, not just types.
with pkgs; [ git vim ] requires knowing the type of pkgs at the point where the with is evaluated. TypeScript has no equivalent to scope injection from a value, so typenix has to rewrite with idioms manually. This is tractable in small examples but becomes a real maintenance burden in practice, since with lib; appears at the top of nearly every nixpkgs file.
builtins.functionArgs f returns an attrset whose keys are the argument names of function f. This is introspection over a function’s structure at runtime; TypeScript does not support extracting argument names as string literals from arbitrary function types. You can extract argument types with conditional types, but extracting names requires the function to be expressed as a very specific generic signature.
Lazy evaluation creates another asymmetry. Nix’s laziness means let x = abort "crash"; in "ok" is a valid program that evaluates to "ok" because x is never forced. TypeScript has no laziness model; its type system evaluates eagerly. A typenix encoding would likely assign x a never type (since abort throws), making the overall type conservative but not incorrect.
At nixpkgs scale, TypeScript’s practical limits on recursive type depth and conditional type instantiation would become a real obstacle. TypeScript has a recursion limit on conditional types to prevent infinite loops, and complex mapped type chains over large attrsets would produce slow type checking or outright errors. This is not a theoretical concern; it is the same wall that TypeScript-as-a-metaprogramming-environment consistently runs into.
The Landscape of Prior Attempts
typenix is one position in a space that several projects have approached differently.
Nickel, developed at Tweag, is the most serious alternative. Rather than typing Nix, Nickel is a new language with gradual typing built in from the start. Its type system uses row polymorphism for records, which handles open attrsets correctly. A Nickel function with type { foo: Num | r } -> Num accepts any record with at least a foo : Num field, where r is the row variable capturing additional fields. Nickel also has first-class contracts for runtime enforcement in untyped regions:
let Port | contract = fun label value =>
if value >= 0 && value <= 65535 then value
else blame label
in
{ port | Port = 8080 }Nickel is a clean-slate redesign and does not aim to type existing Nix code or integrate with nixpkgs. That makes it cleaner but also means it cannot help with the existing large nixpkgs codebase.
PureNix takes a third approach: write typed PureScript, compile to Nix. You get the full Haskell-style type system at the source level, and the types are erased in the Nix output. This works for pure library code but cannot express the full range of Nix idioms, especially anything involving derivations or nixpkgs conventions.
The nil language server by oxalica does lightweight local type inference to support IDE features: hover types, go-to-definition, basic completion. It infers types for obvious cases but makes no claim to soundness. It is practical and widely used, covering the most useful IDE features without attempting the unsolvable parts.
An academic paper by Tobias Pflug explored applying Hindley-Milner inference to a restricted subset of Nix. The conclusion was that HM works well for pure functional code but fails at with, dynamic attribute access, and builtins.functionArgs, which are three of the most commonly used features in real nixpkgs code.
What This Approach Gets Right
The typenix approach has a property the other approaches do not: it delivers IDE integration essentially for free. By encoding Nix types as TypeScript types, it inherits the entire TypeScript toolchain. tsc reports type errors. tsserver provides hover types and completion in VS Code. TypeScript’s structural error messages, while sometimes verbose, are informative. Building a full language server for a new type system from scratch is a major project; typenix sidesteps that entirely.
The approach also requires no changes to the Nix evaluator or the Nix language spec. It is a layer on top, which means it can be adopted incrementally for specific modules without requiring a nixpkgs-wide annotation effort.
The trade-off is that the encoding is not round-trip. You write TypeScript that represents Nix, not actual Nix that gets checked. The correspondence between the TypeScript representation and the Nix that will actually be evaluated has to be maintained manually, and there is no guarantee that a typenix-valid TypeScript encoding reflects the same semantics as the Nix that runs. For catching attrset shape errors and function signature mismatches, this is probably good enough. For deep semantic correctness, the gap matters.
The question of whether to retrofit types onto an existing dynamically typed language or redesign around types from the start is one the JavaScript and Python communities spent years navigating. TypeScript and Mypy both chose the retrofit path, and both hit similar walls with dynamic features like eval, __getattr__, and scope-injection patterns. The lesson from those ecosystems is that gradual typing retrofits can cover a large portion of the useful cases well, and the remaining edge cases require either accepting incomplete coverage or encoding the dynamic behavior in increasingly complex type machinery. typenix is at the beginning of that curve, and the TypeScript-as-engine approach is clever enough that it is worth watching to see how far it gets.