# elly

Elly is a small language layered on Muon (see `muon-spec.md`). Muon defines only
lexical and structural syntax; Elly assigns evaluation semantics to Muon
structures — chains, items, and tuples. Elly source is therefore valid Muon:
Muon is a superset of Mu source code, and Elly is one front-end over it.

This document specifies only a first, deliberately small subset of Elly:

- variable **references**
- function **application**
- function **abstraction** (definition) and name binding
- **symbols** (`.foo`)
- integer **numbers** (`Int`, arbitrary precision) and their `__Int_*` builtins
- positional **tuples**

For the broader vision (records, maps, typing, uniqueness) see `elly-intro.md`.
Everything outside this subset is collected under *deferred* at the end.

## relationship to muon

Elly evaluates Muon structure. Each construct in this subset is a
reinterpretation of a Muon production:

| Elly construct     | Muon production                |
| ------------------ | ------------------------------ |
| reference          | `<sym>` (identifier)           |
| symbol literal     | `<prefixed>` — `.` (see below) |
| integer literal    | `<sym>` (numeric)              |
| application        | `<chain>` (juxtaposition)      |
| abstraction / bind | `<prefixed>` — `&` (see below) |
| tuple              | `<tuple>`                      |

Elly uses Muon's whitespace and separator rules unchanged, but — unlike Muon,
which gives neither any meaning — Elly distinguishes them semantically:

- **juxtaposition** (whitespace within a chain) is **application**: `(f x)` is
  one chain, the application of `f` to `x`.
- a **separator** `<sep>` (`,` or newline) delimits **tuple elements**:
  `(f, x)` is a two-element tuple.

This is the one place a reader must keep the Muon layer in mind: `(f x)` and
`(f, x)` are different Elly values built from the same characters modulo a comma.

A program in this subset is a single expression (one `<chain>`). Top-level
sequencing of multiple chains in a `<seq>` is deferred — it needs
binding/sequencing semantics not in this subset.

Comments (`<comm>`) may appear between items as in Muon; they are ignored by
evaluation.

### the `&` extension to muon

Abstraction needs a marker that is itself part of the notation, so Muon's
`<item>` is extended with a *prefixed item*:

```ebnf
(* no whitespace *)
<prefixed> ::= "&" <item>
```

At the Muon layer this is purely structural and carries no meaning, exactly as
`:` or `-1` are just `<sym>`s. Elly gives `&<item>` the meaning "introduce a
binding". `&` attaches to the item immediately after it (no whitespace): `&x` is
one prefixed item. This addition is reflected in `muon-spec.md`'s `<item>`
production.

## values

The literal values in this subset are symbols (see *symbols*), integers (see
*integers*) and functions; tuples compose them.

Strings as values are deferred, as is the wider numeric tower (`Num`: rationals,
floats, complex), of which `Int` is the first, integer-only slice.

### references

A bare name is a **reference**, never a binding. It evaluates to the value bound
by the nearest enclosing `&`-binder of the same name; if there is none, it is a
free name resolved in the surrounding (e.g. top-level / builtin) environment.

```elly
x        // the value bound by an enclosing &x, else a free name
```

Because binding is always marked with `&`, shadowing is explicit — a name is
never rebound by accident. The corollary is an accepted hazard in this subset:
omitting a `&` where you meant to bind silently turns an intended binding into a
reference.

The standalone name `_` is the **discard** pattern (see *abstraction*), not a
name: it never binds a value and is not a valid reference.

Names beginning with a double underscore (`__`) are **reserved** for builtins
and special forms (e.g. `__call`, `__keys` in `elly-intro.md`). They may be
*referenced* — they resolve in the surrounding environment like any other free
name — but a `&`-binder may not introduce a new one.

Two words are **keywords**: `let` (the local binding form; see *local binding*)
and `with` (reserved for a future form, currently unused). Unlike `__`-names, a
keyword is not even a reference — it is syntax, so it may be neither read nor
bound anywhere. This is the one exception to "a bare name is always a reference":
`let` and `with` are recognized as keywords first. (Using `with` at all is an
error until its form is designed.)

## application

Juxtaposition of items in a chain is function application, **left-associative**:

```elly
f x      // apply f to x
f x y    // (f x) y
```

```ebnf
(* top-level expressions: mapped from a muon.chain *)
<expr> ::=
    | <let>              (* local binding; see "local binding" *)
    | <iexpr>? <abs>
    | <iexpr>
    
(* "itemic" expressions: mapped from a muon.chain of muon.item *)
<iexpr> ::=
    | <iexpr> <aexpr>    (* left-associative *)
    | <aexpr>
         
(* "atomic" expressions: mapped from a muon.item *)
<aexpr> ::= 
   | <name>          (* a reference to a binding *)
   | <symbol>        (* an atomic symbol like `.x`, `.0`, etc *)
   | <int>           (* an arbitrary-precision integer literal; see integers *)
   | <unit>          (* the empty tuple, from a 0-chain muon.tuple *)
   | "(" <expr> ")"  (* grouping / 1-tuple, from a 1-chain muon.tuple *)
   | <tuple>         (* an n-tuple, from a 2+-chain muon.tuple; see tuples *)

(* an identifier: latin letters, digits and `_`, not starting with a digit, and
   not the standalone `_` (the discard pattern; see abstraction). A name may
   start with `__`, but only to reference a builtin — never to bind a new name. *)
<name> ::= (* a <muon.sym> matching the above that is not a number *)

(* a `.`-prefixed literal: `.` glued to a single name or number segment. *)
<symbol> ::= (* a <muon.prefixed> with `.` sigil wrapping a name or number *)

(* an integer literal: `0`, `-123`, `+7`, `1_000_000`, `0xCAFE`, `0b1010`.
   Recognized before <name>; a `.`-prefixed item is a <symbol>, not an <int>.
   See integers for the full digit/base/separator grammar. *)
<int> ::= (* a <muon.sym> matching the integer grammar in "integers" *)
<abs> ::= "&"<name> <expr>  (* the header is mapped from <muon.prefixed> *)

(* local binding; the keyword "let" leads a muon.chain, then a binder group
   (a muon.tuple) and the body. See "local binding". *)
<let>     ::= "let" "(" <binding> (<sep> <binding>)* ")" <expr>
<binding> ::= <binder> "=" <expr>   (* <binder> as in abstraction: <name> or "_" *)
```

A trailing `<abs>` is the application's last argument and captures the rest of
the expression.

### symbols

Elly symbols are `.`-prefixed literals that evaluate to themselves (unless the
context gives them another meaning, e.g. tuple projection). A symbol is a `.`
directly glued to a single name or number segment:

```elly
.foo        // a symbol `.foo`
.0          // a symbol `.0`
```

A symbol wraps exactly one segment. Because `.` is a Muon sigil that breaks
symbols (see `muon-spec.md`), `.foo.bar` is *not* one symbol but the chain
`.foo .bar` — two symbols juxtaposed, i.e. successive projections; the two spell
the same value. The bare dot `.` (nothing glued to its right) is a Muon `<punct>`,
not a symbol — Elly reserves the spaced dot for a future application /
composition combinator and rejects it as an atom for now.

## abstraction

`&name expr` defines a one-parameter function named `name` with body `expr`
(λ-abstraction). The body is **the rest of the expression**: `&` has the lowest
precedence and extends to the end of the expression.

```elly
&x x       // the identity function
&x &y x    // (&x (&y x)) — returns a constant function
```

Binders curry, right-nested, mirroring left-nested application:

```elly
&x &y e  ==  &x (&y e)     // abstraction, right-associative
f x y    ==  (f x) y       // application, left-associative
```

Because abstraction is greediest-right, a lambda used as a non-final argument
must be parenthesized:

```elly
f x &y g y     // (f x) (&y (g y))  — the lambda captures the tail
f (&x x) y     // ((f (&x x)) y)    — parens keep the lambda as one argument
```

A `&` must be followed by a binder and a body; `&x` with nothing after it is
ill-formed (yet).

The binder `_` is the **discard** pattern: `&_ e` still consumes one applied
argument (β-reduction cancels the `&` as usual), but binds no name — the
argument is dropped. A binder may not introduce a name starting with `__`;
those are reserved for builtins and special forms, so `&__x e` is ill-formed.

```ebnf
(* no whitespace between "&" and <binder> *)
<abs>    ::= "&" <binder> <expr>   (* body is the rest of the expr, right-nested *)
<binder> ::= <name>                (* bind a new name; not one starting with `__` *)
           | "_"                   (* discard: consume the argument, bind nothing *)
```

A more technical explanation of "mirroring": abstraction and application are 
the introduction and elimination forms of functions. Applying an abstraction
substitutes the argument for the bound name — β-reduction cancels one `&` 
against one applied argument: `(&x e) a   →   e[x := a]`.


## local binding (`let`)

Binding a value to a name is, at bottom, abstraction-and-application: `(&x e) v`
evaluates `e` with `x` bound to `v`. But that reads backwards — the value sits
*after* the body. `let` is **sugar** for the same thing, written name-first:

```elly
let (x = v) e          // ≡ (&x e) v  — evaluate e with x bound to v
let (x = .foo) x       // → .foo
```

`let` adds no evaluation semantics of its own: it lowers to `App`/`Abs` and
inherits everything from them — strict, value-first evaluation, and the fact that
a binder may be `_` (discard) but not a `__`-name.

The body is **the rest of the expression**, exactly like `&`: `let` has the
lowest precedence and extends to the end, so `let (x = 1) f x` is
`let (x = 1) (f x)`, and a `let` used as a non-final argument must be
parenthesized.

A binder group may hold **several** bindings, separated by `<sep>` (`,` or
newline). They are **sequential**: each right-hand side sees the binders to its
left, so `let (a = 1, b = a) …` is valid and `b` is `1`. This desugars to nested
`let`s:

```elly
let (a = va, b = vb) e   ≡   let (a = va) (let (b = vb) e)   ≡   (&a ((&b e) vb)) va
```

so `va` is evaluated in the enclosing scope and `vb` in the scope where `a` is
bound. Being nested `&`/apply, `let` is therefore **non-recursive** — a
right-hand side never sees its own binder. Because the group is a Muon `<seq>`,
blank lines, hanging separators, and comments between bindings are allowed, so a
group can be laid out as a block:

```elly
let (
  a = 1

  // b builds on a
  b = a
) __Int_add a b        // → 2
```

TODO: a binder group is written like a tuple, `(a = 1, b = 2)`, but it is **not**
a tuple value — after `let` this parenthesized `<seq>` is read as a left-to-right
binding group, so (unlike tuple elements, which are independent expressions in
one scope) scope threads through the commas. This is the same
same-characters/different-reading hazard as `(f x)` vs `(f, x)`; a future parallel
form (all right-hand sides in the enclosing scope) is what the reserved keyword
`with` is earmarked for.

Recursion is still not directly expressible: an abstraction is anonymous and a
name refers only to an *enclosing* binder, and `let` — desugaring to it — is the
same. It can be recovered with a fixpoint combinator once the evaluation strategy
is fixed; both are deferred.


## tuples

A tuple groups zero or more expressions, written as a Muon `<seq>` in
parentheses. Elements are the `<chain>`s of the sequence, delimited by `<sep>`
(`,` or newline); each element chain is evaluated as an `<expr>`.

```elly
()               // unit — the empty tuple
(.a, .b)         // a 2-tuple, elements indexed .0 and .1
(.a, .b, .c)     // a 3-tuple
```

A single-element tuple **is** that element — one-chain parentheses are pure
grouping:

```
(x)         // == x
(f x)       // == f x        (one chain: application)
(&x x)      // == the identity function
```

Contrast the separator, which builds a tuple:

```
(f, x)      // a 2-tuple of f and x
```

Positional indices are `.0`, `.1`, …; named fields / records are deferred.

```ebnf
<unit>  ::= "(" ")"                          (* a 0-chain muon.tuple *)
<tuple> ::= "(" <expr> (<sep> <expr>)+ ")"   (* 2+ elements; <sep> and grouping
                                                per muon-spec.md *)
```

**Projection is not a separate form — it is syntax-level "application" of a
tuple to a symbol that desugars into a getter on the tuple** (like
`Tuple.get_elem` in Elixir). Since juxtaposition is application, `(.zero, .one).0`
is an `<iexpr>`: the tuple "applied" to the symbol `.0`, desugaring to the getter
that selects the named position:

- `(.zero, .one).0` evaluates to `.zero`
- `(.zero, .one).1` evaluates to `.one`
- `().0` and `(.foo).1` do not name a valid position (an error)

Note: the typeless interpreter may implement this as a literal special-cased
`App(<tuple>, <symbol>)`, but a typechecker will not accept a tuple in function
position, so it must treat projection as the distinct getter it desugars to.


## integers

Integers are **arbitrary precision**, signed, and **self-evaluating**. This
subset provides only `Int`; the wider numeric tower — rationals, floats, complex
— is deferred under a future `Num`, with `Int` as its integer-only subset.

### literals

An integer literal is a Muon `<sym>` that is not a `<symbol>` (not `.`-prefixed)
and matches:

```ebnf
(* recognized before <name>. `_` separates digit groups and may not lead,
   trail, or double. *)
<int>       ::= <sign>? <magnitude>
<sign>      ::= "-" | "+"
<magnitude> ::= <dec> | <hex> | <bin>
<dec>       ::= <digit>  ("_"? <digit>)*                 (* base 10 *)
<hex>       ::= "0" ("x"|"X") <hexdig> ("_"? <hexdig>)*  (* base 16 *)
<bin>       ::= "0" ("b"|"B") <bit>    ("_"? <bit>)*     (* base 2  *)
```

```elly
0
-123
+7
1_000_000
0xCAFE       // == 51966
0b1010       // == 10
```

The base prefix, sign and separators are notational only: `0xF`, `15`, `0b1111`
and `+15` all denote the same value. A `<sym>` that is neither a `<symbol>`, a
valid `<int>`, nor a valid `<name>` (e.g. `1a`, `0xZZ`, `--1`) is an error;
operator-like syms remain deferred. Note that `.0` is the **symbol** `.0` (a
`.`-prefixed `0`, a projection index), never the integer `0`.

### semantics

- An integer is self-evaluating: it evaluates to itself.
- **Equality** is by mathematical value (`+0`, `-0`, `0` are all equal).
- **String representation** is canonical signed decimal, without separators or a
  redundant sign / leading zeros: `0`, `15`, `-123`.

### builtins

Arithmetic and elimination are **builtins** in the reserved `__` namespace (see
*references*): free names resolved from the runtime environment, referenceable
but not bindable. All are **curried** (`f x y` = `(f x) y`) and **strict** in
their integer arguments; supplying a non-integer where an integer is required is
an error.

| builtin | shape | meaning |
| --- | --- | --- |
| `__Int_add x y` | `Int → Int → Int` | `x + y` |
| `__Int_sub x y` | `Int → Int → Int` | `x − y` (in this order) |
| `__Int_mul x y` | `Int → Int → Int` | `x × y` |
| `__Int_pow x y` | `Int → Int → Int` | `x` to the power `y` (`y ≥ 0`) |
| `__Int_divrem x y` | `Int → Int → (Int, Int)` | Euclidean quotient and remainder `(q, r)` |
| `__Int_eq m n onEqual onElse` | `Int → Int → (() → r) → (() → r) → r` | `onEqual ()` if `m = n`, else `onElse ()` |
| `__Int_less m n onLess onElse` | `Int → Int → (() → r) → (() → r) → r` | `onLess ()` if `m < n`, else `onElse ()` |
| `__Int_for from to state onEach` | `Int → Int → s → (Int → s → s) → s` | ascending fold over `from … to−1` |

- `__Int_sub x y` subtracts in written order: `__Int_sub 2 5` is `−3`.
- `__Int_pow x y` raises `x` to the power `y`, with `0^0 = 1`. The exponent must
  be non-negative: `y < 0` would give a non-integer and is an error.
- `__Int_divrem x y` returns the Euclidean pair `(q, r)` with `q = x ÷ y` and
  `r = x − y·q` normalized to `0 ≤ r < |y|`, so `x = y·q + r` always holds.
  A zero divisor (`y = 0`) is an error.
- `__Int_eq` tests **equality**: the two branches are thunks (each `() → r`,
  forced with `()`), so only the taken side evaluates; the operands `m`/`n` are
  already in the caller's scope, so neither branch receives them. It is the
  subset's fundamental conditional — there is no boolean or symbol eliminator yet.
- `__Int_less` tests strict **order** `m < n`, with the same thunk-branch shape.
  Equal operands take `onElse`. Combined with `__Int_eq` it yields the rest of the
  ordering (`leq`, `geq`, …) by composition.
- `__Int_for from to state onEach` computes
  `onEach (to−1) (… (onEach (from+1) (onEach from state)) …)` — `onEach` takes the
  **index first**, accumulator second, returning the next accumulator. It iterates
  **ascending only** over the half-open range `[from, to)`; `from ≥ to` runs zero
  iterations and yields `state` (so an inverted range is a harmless no-op). It is
  the bounded iteration primitive, standing in for the fixpoint combinator this
  subset still defers.

```elly
// factorial: iterate i from 1 to n inclusive, acc ← acc × i
&n __Int_for 1 (__Int_add n 1) 1 (&i &acc __Int_mul acc i)

// sum 0 … n−1
&n __Int_for 0 n 0 (&i &acc __Int_add acc i)

// absolute value, via a sign test (0 named explicitly; no __Int_neg)
&n __Int_less n 0 (&_ __Int_sub 0 n) (&_ n)
```

A comparison returning a symbol (`.lt`/`.eq`/`.gt`) is deliberately **not**
provided: this subset cannot eliminate a symbol, so the result would be unusable.
Ordering is expressed instead through `__Int_less` and `__Int_eq` directly.

## deferred

Intentionally out of this subset (carrying `TODO:` here and/or in
`elly-intro.md`):

- the wider numeric tower **`Num`** — rationals, floats, complex (with `Int` as a
  subset), and any numeric coercions
- named tuple **fields / records** (`(foo: 1, bar: 2)`)
- **maps** (`{ … }`)
- **strings** as values
- **patterns** in binders beyond the bare name and the standalone `_` discard
- the `.` and `|>` application **combinators** — `.` now lexes as an infix
  `<punct>` (a spaced dot, e.g. `f . g`) awaiting these semantics
- **typing** (`<expr> as <ty>`)
- **recursion** / fixpoint combinator, and the **evaluation strategy**
  (call-by-value vs -name/-need) it depends on
- **uniqueness / references**, for which `^` is reserved (not `&`)
- value **equality** and **string representation** (open in `elly-intro.md`)