The Egison Programming Language

Egison is a functional programming language featuring its expressive pattern-matching facility. Egison allows users to define efficient and expressive pattern-matching methods for arbitrary user-defined data types including non-free data types such as lists, multisets, sets, trees, graphs, and mathematical expressions. This is the repository of the interpreter of Egison.

For more information, visit our website.

What's New in Egison 5

Egison 5 introduces a static type system based on Hindley-Milner type inference. The type checker infers types automatically, so type annotations are completely optional. You can add type annotations for documentation and safety, but they are not required.

-- 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)

In addition, Egison 5 supports:

• Type classes: Haskell-style type classes and instances (class Eq a where ..., instance Eq Integer where ...)
• Algebraic data types: User-defined inductive data types (inductive Maybe a := | Nothing | Just a)
• Polymorphism: Parametric polymorphism with type variables (def id {a} (x: a) : a := x)
• Symbol declarations: declare symbol x, y, z for declaring symbolic variables used in tensor and math calculations

Refereed Papers

Pattern Matching

• Satoshi Egi, Yuichi Nishiwaki: Non-linear Pattern Matching with Backtracking for Non-free Data Types (APLAS 2018)
• Satoshi Egi, Yuichi Nishiwaki: Functional Programming in Pattern-Match-Oriented Programming Style ( 2020)

Tensor Index Notation

• Satoshi Egi: Scalar and Tensor Parameters for Importing Tensor Index Notation including Einstein Summation Notation (Scheme Workshop 2017)

Non-Linear Pattern Matching for Non-Free Data Types

We can use non-linear pattern matching for non-free data types in Egison. A non-free data type is a data type whose data have no canonical form, or a standard way to represent that object. For example, multisets are non-free data types because a multiset {a,b,b} has two other syntastically different representations: {b,a,b} and {b,b,a}. Expressive pattern matching for these data types enables us to write elegant programs.

Twin Primes

We can use pattern matching for enumeration. The following code enumerates all twin primes from the infinite list of prime numbers with pattern matching!

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)]

Poker Hands

The following code is a program that determines poker-hands written in Egison. All hands are expressed in a single pattern.

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

inductive pattern Suit := | spade | heart | club | diamond
inductive pattern Card := | card Suit Integer

def suit := algebraicDataMatcher | spade | heart | club | diamond
def card := algebraicDataMatcher | card suit (mod 13)

def poker (cs: [Card]) : String :=
  match cs as multiset card with
  | [card $s $n, card #s #(n - 1), card #s #(n - 2), card #s #(n - 3), card #s #(n - 4)]
    -> "Straight flush"
  | [card _ $n, card _ #n, card _ #n, card _ #n, _]
    -> "Four of a kind"
  | [card _ $m, card _ #m, card _ #m, card _ $n, card _ #n]
    -> "Full house"
  | [card $s _, card #s _, card #s _, card #s _, card #s _]
    -> "Flush"
  | [card _ $n, card _ #(n - 1), card _ #(n - 2), card _ #(n - 3), card _ #(n - 4)]
    -> "Straight"
  | [card _ $n, card _ #n, card _ #n, _, _]
    -> "Three of a kind"
  | [card _ $m, card _ #m, card _ $n, card _ #n, _]
    -> "Two pair"
  | [card _ $n, card _ #n, _, _, _]
    -> "One pair"
  | [_, _, _, _, _] -> "Nothing"

Graphs

We can pattern-match against graphs. We can write a program to solve the travelling salesman problem in a single pattern-matching expression.

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

def graphData : [(String, [(String, Integer)])] :=
  [ ("Berlin",    [("St. Louis", 14), ("Oxford", 2),  ("Nara", 14), ("Vancouver", 13)])
  , ("St. Louis", [("Berlin", 14),    ("Oxford", 12), ("Nara", 18), ("Vancouver", 6)])
  , ("Oxford",    [("Berlin", 2),     ("St. Louis", 12), ("Nara", 15), ("Vancouver", 10)])
  , ("Nara",      [("Berlin", 14),    ("St. Louis", 18), ("Oxford", 15), ("Vancouver", 12)])
  , ("Vancouver", [("Berlin", 13),    ("St. Louis", 6),  ("Oxford", 10), ("Nara", 12)]) ]

def trips : [(Integer, [String])] :=
  matchAll graphData as graph with
    | (#"Berlin", ($s_1, $p_1) :: _) :: (loop $i (2, 4, _)
                                           (( #s_(i - 1)
                                           , ($s_i, $p_i) :: _ ) :: ...)
                                           (( #s_4
                                           , ( #"Berlin" & $s_5
                                           , $p_5 ) :: _ ) :: _)) ->
      (sum (map (\i -> p_i) (between 1 5)), s)

Egison as a Computer Algebra System

As an application of Egison pattern matching, we have implemented a computer algebra system on Egison. The most part of this computer algebra system is written in Egison and extensible using Egison.

Symbolic Algebra

Egison treats unbound variables as symbols.

> declare symbol x, y
> x
x
> (x + y)^2
x^2 + 2 * x * y + y^2
> (x + y)^4
x^4 + 4 * x^3 * y + 6 * x^2 * y^2 + 4 * x * y^3 + y^4

We can handle algebraic numbers, too.

• Definition of sqrt in root.egi

> sqrt x
sqrt x
> sqrt 2
sqrt 2
> x + sqrt y
x + sqrt y

Complex Numbers

The symbol i is defined to rewrite i^2 to -1 in Egison library.

• Rewriting rule for i in normalize.egi

> declare symbol x, y
> i * i
-1
> (1 + i) * (1 + i)
2 * i
> (x + y * i) * (x + y * i)
x^2 + 2 * x * y * i - y^2

Square Root

The rewriting rule for sqrt is also defined in Egison library.

• Rewriting rule for sqrt in normalize.egi

> declare symbol x, y
> sqrt 2 * sqrt 2
2
> sqrt 6 * sqrt 10
2 * sqrt 15
> sqrt (x * y) * sqrt (2 * x)
x * sqrt 2 * sqrt y

The 5th Roots of Unity

The following is a sample to calculate the 5th roots of unity.

• Definition of qF' in equations.egi

> qF' 1 1 (-1)
((-1 + sqrt 5) / 2, (-1 - sqrt 5) / 2)
> def t := fst (qF' 1 1 (-1))
> qF' 1 (-t) 1
((-1 + sqrt 5 + sqrt 2 * sqrt (-5 - sqrt 5)) / 4, (-1 + sqrt 5 - sqrt 2 * sqrt (-5 - sqrt 5)) / 4)
> def z := fst (qF' 1 (-t) 1)
> z
(-1 + sqrt 5 + sqrt 2 * sqrt (-5 - sqrt 5)) / 4
> z ^ 5
1

Differentiation

We can implement differentiation easily in Egison.

• Definition of d/d in derivative.egi

> declare symbol x
> d/d (x ^ 3) x
3 * x^2
> d/d (e ^ (i * x)) x
exp (x * i) * i
> d/d (d/d (log x) x) x
-1 / x^2
> d/d (cos x * sin x) x
-2 * (sin x)^2 + 1

Taylor Expansion

The following sample executes Taylor expansion on Egison. We verify Euler's formula in the following sample.

• Definition of taylorExpansion in derivative.egi

> declare symbol x
> take 8 (taylorExpansion (e^(i * x)) x 0)
[1, x * i, - x^2 / 2, - x^3 * i / 6, x^4 / 24, x^5 * i / 120, - x^6 / 720, - x^7 * i / 5040]
> take 8 (taylorExpansion (cos x) x 0)
[1, 0, - x^2 / 2, 0, x^4 / 24, 0, - x^6 / 720, 0]
> take 8 (taylorExpansion (i * sin x) x 0)
[0, x * i, 0, - x^3 * i / 6, 0, x^5 * i / 120, 0, - x^7 * i / 5040]
> take 8 (map2 (+) (taylorExpansion (cos x) x 0) (taylorExpansion (i * sin x) x 0))
[1, x * i, - x^2 / 2, - x^3 * i / 6, x^4 / 24, x^5 * i / 120, - x^6 / 720, - x^7 * i / 5040]

Tensor Index Notation

Egison supports tesnsor index notation. We can use Einstein notation to express arithmetic operations between tensors.

The method for importing tensor index notation into programming is discussed in Egison tensor paper.

The following sample is from Riemann Curvature Tensor of S2 - Egison Mathematics Notebook.

declare symbol r, θ, φ: MathExpr

-- Parameters
def x : Vector MathExpr := [| θ, φ |]

def X : Vector MathExpr := [| r * sin θ * cos φ -- x
          , r * sin θ * sin φ -- y
          , r * cos θ         -- z
          |]

def e_i_j : Matrix MathExpr := ∂/∂ X_j x~i

-- Metric tensors
def g[_i_j] : Matrix MathExpr := generateTensor (\[a, b] -> V.* e_a e_b) [2, 2]
def g[~i~j] : Matrix MathExpr := M.inverse g_#_#

g_#_# -- [| [| r^2, 0 |], [| 0, r^2 * (sin θ)^2 |] |]_#_#
g~#~# -- [| [| 1 / r^2, 0 |], [| 0, 1 / (r^2 * (sin θ)^2) |] |]~#~#

-- Christoffel symbols
def Γ_i[_j_k] : Tensor MathExpr := (1 / 2) * (∂/∂ g_i_k x~j + ∂/∂ g_i_j x~k - ∂/∂ g_j_k x~i)

Γ_1_#_# -- [| [| 0, 0 |], [| 0, -1 * r^2 * (sin θ) * (cos θ) |] |]_#_#
Γ_2_#_# -- [| [| 0, r^2 * (sin θ) * (cos θ) |], [| r^2 * (sin θ) * (cos θ), 0 |] |]_#_#

def Γ~i_j_k : Tensor MathExpr := withSymbols [m]
  g~i~m . Γ_m_j_k

Γ~1_#_# -- [| [| 0, 0 |], [| 0, -1 * sin θ * cos θ |] |]_#_#
Γ~2_#_# -- [| [| 0, (cos θ) / (sin θ) |], [| (cos θ) / (sin θ), 0 |] |]_#_#

-- Riemann curvature
def R~i_j_k_l : Tensor MathExpr := withSymbols [m]
  ∂/∂ Γ~i_j_l x~k - ∂/∂ Γ~i_j_k x~l + Γ~m_j_l . Γ~i_m_k - Γ~m_j_k . Γ~i_m_l

R~#_#_1_1 -- [| [| 0, 0 |], [| 0, 0 |] |]~#_#
R~#_#_1_2 -- [| [| 0, (sin θ)^2 |], [| -1, 0 |] |]~#_#
R~#_#_2_1 -- [| [| 0, -1 * (sin θ)^2 |], [| 1, 0 |] |]~#_#
R~#_#_2_2 -- [| [| 0, 0 |], [| 0, 0 |] |]~#_#

Differential Forms

By designing the index completion rules for omitted indices, we can use the above notation to express a calculation handling the differential forms.

The following sample is from Curvature Form - Egison Mathematics Notebook.

declare symbol r, θ, φ: MathExpr

-- Parameters and metric tensor
def x : Vector MathExpr := [| θ, φ |]

def g_i_j : Matrix MathExpr := [| [| r^2, 0 |], [| 0, r^2 * (sin θ)^2 |] |]_i_j
def g~i~j : Matrix MathExpr := [| [| 1 / r^2, 0 |], [| 0, 1 / (r^2 * (sin θ)^2) |] |]~i~j

-- Christoffel symbols
def Γ_j_l_k : Tensor MathExpr := (1 / 2) * (∂/∂ g_j_l x~k + ∂/∂ g_j_k x~l - ∂/∂ g_k_l x~j)

def Γ~i_k_l : Tensor MathExpr := withSymbols [j] g~i~j . Γ_j_l_k

-- Riemann curvature
def R~i_j_k_l : Tensor MathExpr := withSymbols [m]
  ∂/∂ Γ~i_j_l x~k - ∂/∂ Γ~i_j_k x~l + Γ~m_j_l . Γ~i_m_k - Γ~m_j_k . Γ~i_m_l

-- Exterior derivative
def d (t : Tensor MathExpr) : Tensor MathExpr := !(flip ∂/∂) x t

-- Connection form
def ω~i_j : Matrix MathExpr := Γ~i_j_#

-- Curvature form
def Ω~i_j : Tensor MathExpr := withSymbols [k]
  antisymmetrize (d ω~i_j + ω~i_k ∧ ω~k_j)

Ω~#_#_1_1 -- [| [| 0, 0 |], [| 0, 0 |] |]~#_#
Ω~#_#_1_2 -- [| [| 0, (sin θ)^2  / 2|], [| -1 / 2, 0 |] |]~#_#
Ω~#_#_2_1 -- [| [| 0, -1 * (sin θ)^2 / 2 |], [| 1 / 2, 0 |] |]~#_#
Ω~#_#_2_2 -- [| [| 0, 0 |], [| 0, 0 |] |]~#_#

Egison Mathematics Notebook

Here are more samples.

• Egison Mathematics Notebook

Comparison with Related Work

There are a lot of existing work for pattern matching.

The advantage of Egison is that it fulfills the following two requirements at the same time.

1. Efficient backtracking algorithm for non-linear pattern matching.
2. Extensibility of patterns.

Additionally, it fulfills the following requirements.

3. Polymorphism of patterns.
4. Pattern matching with infinitely many results.

Check out our paper for details.

Installation

Installation guide is available on our website.

If you are a beginner of Egison, it would be better to install egison-tutorial as well.

We also have online interpreter and online tutorial. Enjoy!

Editor Support

Egison provides syntax highlighting plugins for the following editors:

• Emacs: emacs/egison-mode.el -- See emacs/README.md for installation instructions.
• Vim / Neovim: vim/ -- See vim/README.md for installation instructions.
• VS Code / Cursor: vscode-extension/ -- See vscode-extension/INSTALL.md for installation instructions.

Notes for Developers

You can build Egison as follows:

$ cabal build

For testing, see test/README.md.

Community

We have a mailing list. Please join us!

We are on Twitter. Please follow us.

License

Egison is released under the MIT license.

We used husk-scheme by Justin Ethier as reference to implement the base part of the previous version of the interpreter.

Sponsors

Egison is sponsored by Rakuten, Inc. and Rakuten Institute of Technology.