SkillAgentSearch skills...

Egison

The Egison Programming Language

GenerateConvertImprove

Install / Use

/learn @egison/Egison
About this skill

Quality Score

0/100

Supported Platforms

Universal

README

The Egison Programming Language

Build Status

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 <a target="_blank" href="https://www.egison.org">our website</a>.

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

Tensor Index Notation

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.

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

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

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

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

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

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

egison

View profile

View on GitHub
GitHub Stars921
CategoryDevelopment
Updated3d ago
Forks31
egison/egison

Languages

Haskell

Security Score

100/100

Audited on Mar 24, 2026

No findings