· 6 min read ·

Nix Gets a Type System Borrowed from TypeScript

Source: lobsters

The Nix expression language has never had static types. It has never had type annotation syntax. The closest thing to a type system in the standard Nix ecosystem is the NixOS module system’s runtime validators, which check values at evaluation time and produce friendly errors, but do nothing before you run the code. For most Nix users, this is an accepted tradeoff: the language is small and purely functional, so runtime errors are usually comprehensible. For anyone writing large nixpkgs derivations or complex NixOS module configurations, it is a persistent friction point.

typenix takes a different approach than most efforts to address this problem. Rather than designing a new type system for Nix, it reuses TypeScript’s. The bet is that TypeScript, which was purpose-built to retrofit types onto dynamically-typed JavaScript with structural object semantics, is essentially solving the same problem as Nix typing, just in a different syntax.

Why Nix Is Hard to Type

Nix is a purely functional, lazy, dynamically-typed language. Those properties combine in ways that defeat standard type inference approaches.

The most fundamental issue is that Nix has no type annotation syntax at all. There is no place to write String or Int or Package. Every function, every attribute set, every derivation is just an expression that evaluates to a value at runtime. A type checker has to infer everything from structure alone.

Attribute sets are the universal data structure in Nix. Packages are attribute sets. Modules are attribute sets. Configurations are attribute sets. The shape of a given attrset, meaning which keys it has and what type of value each key holds, is usually only knowable at evaluation time. The // merge operator makes this worse: set1 // set2 produces a new attrset where set2’s keys override set1’s. Tracking the resulting shape precisely requires reasoning about the types of both operands simultaneously, something closer to dependent typing than standard structural inference.

Function arguments in Nix use attrset destructuring: { pkgs, lib, config, ... }: .... The ... means the function accepts any attrset that contains at least pkgs, lib, and config plus any additional keys. This is row polymorphism, a feature that most production type systems, including TypeScript, handle only approximately.

Laziness introduces another complication. Because Nix is lazy, a subexpression that would cause a type error at runtime may never be evaluated if it is never forced. A sound type checker that rejects all such programs would reject valid Nix programs. A type checker that accepts them is unsound. Both tradeoffs are real.

Finally, with expr; brings all keys of an attrset into lexical scope. This makes scope analysis non-local: you cannot determine what names are in scope at a given point without knowing the runtime shape of the set passed to with.

What Everyone Else Tried

The prior attempts at solving Nix’s type problem mostly concluded that the language itself needed to change.

Nickel, developed by Tweag, is a typed configuration language that can compile to Nix. It uses gradual typing with contracts enforced at runtime, plus a static checker for fully-annotated code. Nickel is genuinely well-designed: it has record types with optional fields, polymorphic functions, refinement types via contracts, and a clean syntax. The problem is adoption. Nickel requires rewriting your configuration in a new language. Existing nixpkgs and NixOS configurations do not become typed; you have to start over.

PureNix takes the same approach from a different direction. It is a PureScript-to-Nix compiler. PureScript is a Haskell-like language with Hindley-Milner type inference. You write PureScript, get full static typing, and emit valid Nix as output. The generated Nix is often verbose and the tooling integration is limited, but the type system itself is rigorous. PureNix faced adoption challenges for the same reason Nickel does: it requires abandoning Nix as the source language.

On the tooling side, nil and nixd are Nix language servers that provide IDE support. nixd is particularly sophisticated: it runs the Nix evaluator in a constrained way to extract type information from NixOS options at edit time, providing type-aware completion for module options. This works well for the NixOS module system but is fundamentally runtime analysis, not static typing. It cannot catch errors before evaluation.

The pattern across all of these projects is: build something new, whether that is a new language, a new evaluator, or a new checker. typenix’s approach is different. It asks whether an existing type checker can be adapted instead.

TypeScript as a Structural Type Checker for Nix

TypeScript was designed specifically to type-check dynamically-typed JavaScript. JavaScript objects are structurally typed: if you pass an object with the right shape, it works, regardless of what class it came from or what name it was declared with. TypeScript’s type system is built around this model. It checks structure, not declarations.

Nix attribute sets have the same semantics. The language does not have nominal types. A function that expects { name, version } accepts any attrset with at least those two keys. TypeScript’s structural subtyping encodes this directly. An object type { name: string, version: string } in TypeScript accepts any object that has at least those fields with compatible types.

The mapping between Nix concepts and TypeScript types is reasonably clean for the common cases:

// Nix: { pname, version, src, buildInputs ? [] }:
// TypeScript equivalent:
type Derivation = {
  pname: string;
  version: string;
  src: NixPath;
  buildInputs?: NixPackage[];
};

// Nix: builtins.map (x: x + 1) list
// TypeScript equivalent:
declare function nixMap<A, B>(f: (a: A) => B): (list: A[]) => B[];

// Nix: { config, pkgs, lib, ... }:
// TypeScript equivalent:
type NixosModuleArgs = {
  config: NixosConfig;
  pkgs: Nixpkgs;
  lib: NixLib;
  [key: string]: unknown;
};

The [key: string]: unknown index signature on NixosModuleArgs approximates the ... row extension, though it is not precise, since it does not let TypeScript verify that additional keys have specific types.

For builtins and lib functions, typenix can provide type stubs in the same way that @types/node provides stubs for Node.js built-ins. TypeScript already has the machinery to type-check against a declared interface without having the implementation available. The Nix builtins are a finite, stable API; writing stubs for them is mechanical work, not research.

Where the Mapping Gets Strained

The // merge operator is the main place where TypeScript’s type system does not fit cleanly. TypeScript’s intersection type A & B models combining two object types, but it gives B’s fields precedence only loosely. The spread type { ...A, ...B } (modeled with mapped types or Omit<A, keyof B> & B) is closer to Nix’s override semantics, but this requires mapped type machinery for every merge operation. In practice, large Nix codebases use // extensively, and requiring precise TypeScript encodings of every merge could produce more noise than signal.

The with expression is essentially unhandable statically. TypeScript has no equivalent that is in common use and fully typed. The best a type checker can do is treat with expr; as introducing unknown-typed names, which provides no checking for code inside the with scope.

The NixOS module system’s config attrset is the deepest challenge. Its full type is the intersection of all option declarations across all imported modules, and those modules are only known at evaluation time. nixd’s approach of running the evaluator is probably the right answer for module-level completion, and a static type checker like typenix would need to either accept imprecision here or require explicit opt-in annotations on modules.

The Right Kind of Pragmatism

The deeper value in the typenix approach is not that it solves every Nix typing problem. It is that it demonstrates a viable path that does not require the community to rewrite millions of lines of Nix. TypeScript has a decade of engineering behind it: its checker handles recursive types, conditional types, template literals, mapped types, and generic constraints. It has broad IDE tooling support. It is already understood by a large developer population.

The analogous moment in JavaScript’s history is instructive. TypeScript did not replace JavaScript. It layered types on top of existing JavaScript, accepted that any would be everywhere initially, and provided value proportional to how much you annotated. Gradually, the ecosystem added .d.ts files for existing libraries, and coverage improved. A similar trajectory for Nix is plausible: start with typed stubs for builtins and common lib functions, provide checking for the common derivation patterns, and let coverage grow.

Nickel and PureNix are the right answer if you are starting a greenfield configuration codebase and want rigorous types from day one. typenix is the right answer if you have existing Nix code and want incremental, opt-in type checking without a rewrite. Both approaches are valid; they just serve different starting conditions.

The project is early, and the hardest problems, particularly // semantics, the NixOS module system, and lazy evaluation, remain open. But the core insight, that TypeScript’s structural type system is a reasonable fit for Nix’s data model, is sound enough to be worth following.

Was this interesting?