Egison matches patterns over data that has no canonical form

A language whose central feature is a matching facility

Egison is a functional programming language and the repository holds its interpreter, written in Haskell. The README describes it in one line: a functional programming language featuring an expressive pattern-matching facility, allowing users to define matching methods for arbitrary user-defined data types.

The audience that follows from that is specific. These are people who write symbolic mathematics, computer algebra, differential geometry work or algorithm exploration, where the natural program is a description of a shape rather than a traversal that reconstructs it. The topics attached to the repository list computer-algebra-system, differential-geometry and tensor alongside the language-level ones.

It is also a language with a research pedigree. The README points to refereed papers on non-linear pattern matching with backtracking for non-free data types, on pattern-match-oriented programming style, and on scalar and tensor parameters for importing tensor index notation including Einstein summation notation. Those papers are where the design questions are actually argued out.

The homepage is egison.org, and the README says the site holds more information. For anyone evaluating this, the interesting reading is the design/ directory in the repository, not the feature list.

Non-free data types are the reason the matching facility exists

The core technical idea is the treatment of non-free data types. The README defines one as a data type whose data have no canonical form, or standard way of representing that object. The example given is a multiset, where {a,b,b} has two other syntactically different representations, {b,a,b} and {b,b,a}.

Ordinary pattern matching assumes a canonical representation, so a match against a multiset either misses the intended case or matches several equivalent ones inconsistently. Egison allows non-linear pattern matching for these types, with backtracking, which means a pattern can try several ways of viewing the same data.

The data types named in the README as supported are lists, multisets, sets, trees, graphs and mathematical expressions, alongside arbitrary user-defined types. That list is the practical scope of the feature.

The payoff is that enumeration and search can be written as patterns. The README's twin prime example matches over the list of primes with a pattern that looks for two numbers two apart, rather than writing a loop with a filter.

def twinPrimes : [(Integer, Integer)] :=
  matchAll primes as list integer with
    | _ ++ $p :: #(p + 2) :: _ -> (p, p + 2)

take 8 twinPrimes
-- [(3, 5), (5, 7), (11, 13), (17, 19), (29, 31), (41, 43), (59, 61), (71, 73)]

The backtracking that makes this work is also the source of its cost, since a failing match has to try alternatives.

Egison 5 infers types, and annotations became optional

Version 5 introduced a static type system based on Hindley-Milner type inference, which is a large change for a language whose earlier releases had no such system. The README is clear about the consequence: the type checker infers types automatically, so type annotations are completely optional. You can add them for documentation and safety, but they are not required.

The example the README gives shows both styles side by side.

-- Type annotations are optional. Both styles work:
def fact n :=
  if n == 0 then 1 else n * fact (n - 1)

def fact (n : Integer) : Integer :=
  if n == 0 then 1 else n * fact (n - 1)

For a language used for exploration, that is the right default. An annotation-free definition can be typed as you go without rewriting earlier code, and inference still catches real errors.

The release history shows the version 5 line arriving in two steps. Version 5.0.0 was tagged on 2026-03-01 and version 5.1.0 on 2026-07-20. The previous release, version 4.1.3, dates from 2021-12-18, so the jump from 4 to 5 also carries several years of design work and is not a drop-in upgrade for existing code.

Type classes, inductive types and symbolic declarations in version 5

Alongside inference, version 5 adds a set of Haskell-flavoured language features. The README lists type classes with Haskell-style class and instance declarations, algebraic data types defined as user-defined inductive types, parametric polymorphism with type variables, and symbol declarations for symbolic variables used in tensor and math calculations.

Two of those deserve a note. The inductive type syntax means Egison now has ordinary algebraic data types alongside its pattern-oriented ones, which is what lets the poker hand example define suits and cards as data and then write a separate pattern type for matching them. The symbol declarations exist for the tensor use case, where a variable stands for an unspecified quantity rather than a value.

The syntax in the README looks like this.

inductive Suit := Spade | Heart | Club | Diamond
inductive Card := Card Suit Integer

inductive pattern Suit := | spade | heart | club | diamond
inductive pattern Card := | card Suit (Any for Integer)

The separation between the data type and the pattern type is the interesting part. A program declares how cards are built and separately declares how they can be matched, and the Any capability appears on the integer field to say that only value patterns and wildcards apply there.

Matcher types carry a capability index separate from the target

The most detailed part of the README describes the typing of matchers, and it is worth reading closely because it defines where the guarantees stop.

Matcher types have two indices, Matcher capability target. The capability describes which pattern constructors the matcher supports, independently of its ordinary target type. The ground capability Any supports value patterns and wildcards only. A structured capability uses a declared pattern type with the capabilities of its parameters, such as [p] or Maybe p.

The graph example shows how this is written.

def station : Matcher String String := string
def price : Matcher Any Integer := integer
def graph : Matcher [(String, [(String, Any)])] [(String, [(String, Integer)])] :=
  multiset (station, multiset (station, price))

The same matcher type is used for definitions, parameters and pattern requirements, and a requirement and the matcher expression it is matched with are related by ordinary type equality solved by unification over both sorts. The checker follows the rules of the core calculus of the type-pm paper, mechanized in type-pm-mech.

Egison-specific extensions, specifically gradual TAny values, computer-algebra pattern views, tensor types and pattern syntax specific to the Egison interpreter, are selected only by explicit non-core forms and can be reported with --outside-egison-core-warnings. That flag is the practical lever here: run with it and you learn when a program steps outside the mechanised core.

Where the typing story deliberately stops short

Two statements in the README set limits that should shape an evaluation, and neither is buried.

The first is that a formal correspondence theorem between the complete Haskell implementation and the Lean implementation is intentionally out of scope. In other words, the mechanised core is not a proof about the whole system you actually run, and the gap between the two is deliberate rather than pending work.

The second is that the implemented guarantees and the boundary of the legacy CAS pattern views are documented in design/matcher-capability.md. The legacy computer-algebra views are exactly the part a symbolic-mathematics user is most likely to depend on, so that document is the file to read before committing.

There is a further practical limit to the feature itself. Pattern matching with backtracking over non-free data types is expensive when a match fails, because the engine has to try other views of the same data. The repository layout shows the maintainers are conscious of resource limits: there is a BUILD-LOW-MEMORY.md file at the top level and separate benchmark/ and small-benchmark/ directories. The README does not document what the memory or time cost of a given pattern is, so the practical answer is to measure your own patterns rather than to trust a general claim.

Building the interpreter, running samples, and where releases stand

The repository is a Haskell project with a cabal file, egison.cabal, a Setup.hs and a cabal.project.local.dev for local configuration, alongside hs-src/, lib/, design/, scripts/ and directories for editors: emacs/, vim/ and a vscode-extension/.

The sample/ directory is the best tour of the language. It contains a STATUS.md and programs such as bellman-ford.egi, binary-counter.egi, bipartite-graph.egi, five-color.egi, mahjong.egi and n-queen.egi, plus subdirectories for io/, database/, math/ and physics/. There is also a mini-test/ and minitest/ directory alongside test/.

The README does not give an install command for the interpreter, so the project points you at egison.org for that, and the cabal file in the repository is where the build definition lives. The BUILD-LOW-MEMORY.md file is the document to read if you are compiling on a constrained machine.

On versions, 5.1.0 is the current release, tagged on 2026-07-20, and the repository is not archived with the last push on 2026-10-16, so the interpreter is being worked on. The licence field on the repository says MIT, which is permissive and imposes no obligation on derived work beyond keeping the notice.

Editorial conclusion

Egison fits researchers and students who want to write enumeration and search programs as patterns rather than as hand-rolled traversal code, and it is a good fit for symbolic work on multisets and graphs. It does not fit production service work, because it is an interpreter for an experimental language with a small ecosystem and a release history that skipped most of the decade between version 4.1.3 and version 5.0.0. Before adopting it, read design/matcher-capability.md to see which guarantees hold for your patterns, and run your program with --outside-egison-core-warnings so that Egison-specific extensions are visible instead of silent.

Frequently asked questions

Official sources

1. egison/egison on GitHub
2. License: MIT
3. Project website
4. README
5. Releases