egison-5.0.0: README.md

# The Egison Programming Language
[![Build Status](https://travis-ci.org/egison/egison.svg?branch=master)](https://travis-ci.org/egison/egison)

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.

```hs
-- 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](https://arxiv.org/abs/1808.10603) (APLAS 2018)
* Satoshi Egi, Yuichi Nishiwaki: [Functional Programming in Pattern-Match-Oriented Programming Style](https://doi.org/10.22152/programming-journal.org/2020/4/7) (<programming> 2020)

### Tensor Index Notation

* Satoshi Egi: [Scalar and Tensor Parameters for Importing Tensor Index Notation including Einstein Summation Notation](https://arxiv.org/abs/1702.06343) (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!

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

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

```hs
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`](https://github.com/egison/egison/blob/master/lib/math/algebra/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`](https://github.com/egison/egison/blob/master/lib/math/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`](https://github.com/egison/egison/blob/master/lib/math/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`](https://github.com/egison/egison/blob/master/lib/math/algebra/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`](https://github.com/egison/egison/blob/master/lib/math/analysis/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](https://en.wikipedia.org/wiki/Euler%27s_formula) in the following sample.

* [Definition of `taylorExpansion` in `derivative.egi`](https://github.com/egison/egison/blob/master/lib/math/analysis/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](https://en.wikipedia.org/wiki/Einstein_notation) to express arithmetic operations between tensors.

The method for importing tensor index notation into programming is discussed in [Egison tensor paper](https://arxiv.org/abs/1702.06343).

The following sample is from [Riemann Curvature Tensor of S2 - Egison Mathematics Notebook](https://www.egison.org/math/riemann-curvature-tensor-of-S2.html).


```hs
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](https://www.egison.org/math/curvature-form.html).

```hs
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](https://www.egison.org/math/)

## Comparison with Related Work

There are <a target="_blank" href="https://ghc.haskell.org/trac/ghc/wiki/ViewPatterns#Relatedwork">a lot of existing work</a> 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 <a target="_blank" href="https://arxiv.org/abs/1808.10603">our paper</a> for details.

## Installation

[Installation guide](https://egison.readthedocs.io/en/latest/reference/install.html) is available on our website.

If you are a beginner of Egison, it would be better to install <a target="_blank" href="https://github.com/egison/egison-tutorial">`egison-tutorial`</a> as well.

We also have [online interpreter](http://console.egison.org) and [online tutorial](http://try.egison.org/).
Enjoy!

## Editor Support

Egison provides syntax highlighting plugins for the following editors:

- **Emacs**: [`emacs/egison-mode.el`](emacs/) -- See [`emacs/README.md`](emacs/README.md) for installation instructions.
- **Vim / Neovim**: [`vim/`](vim/) -- See [`vim/README.md`](vim/README.md) for installation instructions.
- **VS Code / Cursor**: [`vscode-extension/`](vscode-extension/) -- See [`vscode-extension/INSTALL.md`](vscode-extension/INSTALL.md) for installation instructions.

## Notes for Developers

You can build Egison as follows:
```
$ cabal build
```

For testing, see [test/README.md](test/README.md).

## Community

We have <a target="_blank" href="https://www.egison.org/community.html">a mailing list</a>.
Please join us!

We are on <a target="_blank" href="https://twitter.com/Egison_Lang">Twitter</a>.
Please follow us.

## License

Egison is released under the [MIT license](https://github.com/egison/egison/blob/master/LICENSE).

We used [husk-scheme](http://justinethier.github.io/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.](http://global.rakuten.com/corp/) and [Rakuten Institute of Technology](http://rit.rakuten.co.jp/).