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

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

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:

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

(* 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:

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

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

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

&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:

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.

(* 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:

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 lets:

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:

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

()               // 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.

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

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

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.

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

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