Emacs Lisp recently got a new type-checker add-on called et. Of course, Emacs already has a type system and more extensive work in this area was done when the native compiler was added (comp.el and comp-cstr.el). Compatibility types with Common Lisp are also provided by cl-lib, which gives Emacs the vocabulary already known from Common Lisp. In other words, et is not the first one. For a few years now there has also been Elsa, an external type-checker in an older “Haskell-style” mould.

While et only surfaced publicly a couple of days ago (its initial commit dates to April 4th), it shows what a modern type-checker looks like. Where Elsa is a mature static analysis tool that happens to contain a type system, et is a deep type system that happens to come with a thin tool around it. They expose what the other is missing—and together, they raise an architectural question about whether static tools should be built parallel to Emacs or layered onto it.

1. What et Is

Plainly, et is a static type checker in the style of mypy or TypeScript. et-defun expands into a standard cl-defun with a (declare (et ...)) block attached; at runtime it costs nothing, annotations compile away to nothing.

What sets et apart is the expressiveness of its type system. It provides parametric polymorphism with constraints, variance annotations (CONST, CO, CONTRA, ISO), a PolyFunction type whose return type depends on its input arguments, a deliberate distinction between read-only (&Cons) and read-write (ConsRW) cons cells, and per-key PlistRW types with separate read and write types. It supports flow-sensitive narrowing across loops and nonlocal exits, infers unannotated let variables from how they are used and mutated in the body, checks nested places (car, cdr, plist-get, alist-get), and resolves function overloads when a return type depends on a noerror-style flag.

Because checking polymorphic constraints and overloads is computationally heavy, et includes a fine-grained per-file .eld cache. It fingerprints each defun against the sources and signatures it touches, and caches constraint-solving results structurally so that only functions whose dependencies actually changed get re-checked during an editing session.

2. Elsa: The Established Counterpart

If et is a 2020s dependent-output type system, Elsa is a 1990s type algebra wrapped in a batteries-included linting and IDE suite.

Elsa’s type system is built around unions, intersections, and differences. It supports value-constrained const types, readonly, structural plists, EIEIO classes, and predicate narrowing. In comparison to et, it lacks generics, variance, mutability tracking, or general constraint solving. Its analytical strength lies in its trinary flow analysis (true / false / maybe), which carefully tracks reachability and variable mutations across if, and, and or branches.

et currently offers only a batch Flymake/Flycheck backend, et-peek, and an AI-bootstrapped definitions/ folder while Elsa provides a complete ecosystem: around 1,500 curated built-in types, extensions for dash, seq, cl, and eieio, loadable style and dead-code rulesets, Elsafile.el, parallel dependency-layer workers, Eask/Cask CLI runners, and a working LSP server.

If you want to catch typos, find dead branches, and hook into LSP today, use Elsa. If you want generics, variance, read/write discipline, and constraint solving, et has the algebra.

3. Layering Onto Emacs vs. Building in Parallel

Beyond type checking, both projects also have the raw material to drive a source-to-source optimizer. elisp-optimizer.el demonstrates this by hooking into et’s type facts to fold branches, turn equal into eq, and inline mapcar. Elsa has these checks wired in mostly as linter suggestions but its 1,500 typed built-ins could just as easily fuel the same optimizations across standard library code. Where et could eventually push further is in its richer algebra: its read-only types (&Cons) and parametric generics allow an optimizer to eliminate redundant reads and preserve container element types in ways coarse union types cannot.

However, not everything is shiny. Both elsa and et make some choices I think are a bit questionable.

First, there is the cognitive tax of a parallel vocabulary. In et, you write Integer instead of integer, List<E> instead of list, and (declare (et (x Integer))) instead of (declare (type integer x)). Both Integer and integer map to integerp and denote the exact same runtime values. Having two names for the same concept in the same buffer is a pure tax on working memory whenever you move between standard cl-defun/cl-deftype code and et.

Second, building sideways forces mechanical duplication across the toolchain. Both Elsa (elsa–macroexpand-form) and et (et-check-expansion) maintain custom position-preserving readers and cons-cell source maps. But the duplication runs deeper:

In Elsa’s case, it re-implements scope and arity tracking from scratch. Emacs’s own byte-compiler already computes arities, detects free variables, tracks lexical bindings, and resolves closure scopes via cconv.el and byte-compile-form. Elsa duplicates all of this with its own elsa-scope, custom arity inspectors (elsa–arglist-to-arity), and free-variable checkers. Furthermore, Elsa requires its own comment parser and custom reader (elsa-reader.el) to scrape line-preceding type signatures (;; (foo :: (function …))) and maintains parallel elsa-declare-defun/elsa-declare-defvar files, creating a secondary module-loading system that mirrors Emacs’s own provide/require and feature registry.

et duplicates things differently: Emacs already parses (declare (type …)) via defun-declarations-alist for byte-opt.el and comp.el, yet because et hides its types inside (declare (et …)) and a custom string DSL (et:repr–parse-string), the native compiler remains blind to them while et runs a second parser over the same definitions. Worse, downstream tools like elisp-optimizer.el bolt a brand-new AST walker onto cconv-closure-convert—even admitting in a comment that byte-optimize-form-code-walker in byte-opt.el already does the prog1 folding the optimizer reimplements.

Duplicated walkers and scoping engines inevitably drift. When Emacs fixes a subtle scoping or macroexpansion bug in cconv or byte-opt, external tools stay broken until someone manually ports the fix. The same maintenance tax applies to the type catalogues: et’s LLM-generated definitions for the standard library and Elsa’s ~1,500 typed built-ins both exist outside core. The moment an Emacs primitive or third-party library changes its signature, the external definition in Et or Elsa silently become stale.

A layered version of neither tool exists yet. Both Elsa and Et are built as parallel universes alongside Emacs while still sharing the same space with Emacs, since they both run on top of Emacs. Steering future work toward a layered design guided by one producer, one consumer, one vocabulary at each seam rule would benefit each project and the entire Emacs community.

For Elsa

Elsa already possesses the greatest asset in the ecosystem: ~1,500 curated built-in type signatures. In a layered world, Elsa would:

Drop comment-based DSLs in favor of standard declarations: Replace ;; (foo :: (function (int) int)) and (put ‘foo ’elsa-type …) with standard (declare (type …)) and (declare (ftype …)) via defun-declarations-alist.

Export its built-in facts to Emacs: Expose its 1,500 signatures through Emacs’s existing symbol properties (side-effect-free, pure, and the native compiler’s comp-cstr type registry). That single move would instantly make Emacs’s native compiler (comp.el) and byte-opt.el drastically smarter for every user, even those not running Elsa.

Reuse the compiler’s scope: Instead of maintaining a duplicate lexical environment (elsa-scope) and ad-hoc arity checks, Elsa could consume the AST and closure records already produced by cconv.el and the byte compiler.

For et

Et possesses the richer type algebra and solver. In a layered world, et would:

Adopt Emacs’s public vocabulary: Use integer, string, cons, list, and function where Emacs already names them, reserving et names (poly-function, cons-rw, plist-rw) strictly for concepts Emacs lacks.

Keep polymorphism internal, export monomorphic facts: comp.el does not need to understand PolyFunction or variance; it just needs to know x is a fixnum on line 40. et already calculates those concrete monomorphic bounds.

Feed Emacs’s native seams: Register monomorphic instantiations as cl-deftype, declare function types via defun-declarations-alist, and emit (cl-the fixnum x) when narrowing branches.

The hard parts of et—the type algebra, the solver, the flow engine, and the cache—are already built. The right response from the community is to test it, file issues on Integer vs integer and (declare (et ...)) vs (declare (type ...)), and help steer a great parallel experiment into a layered extension of Emacs Lisp.

The Shared Payoff

If both tools fed Emacs’s standard type system, they would not only stop duplicating work, but also stop competing at the syntax layer. Elsa could consume et’s polymorphic solver for complex generics, et could consume Elsa’s 1,500 typed built-ins without having to regenerate them via AI, and downstream optimizers like elisp-optimizer.el would not need to write a third AST walker because byte-opt.el and comp.el would already receive the type facts directly.