# AILang Form-A — LLM authoring specification

Form-A is the canonical textual surface of AILang. It is the form that
LLMs generate when asked to produce or edit AILang code, and the form
that `ail parse <file>.ail` reads. The inverse direction — printing
JSON-AST as Form-A — is `ail render <file>.ail.json`. Round-trip
through this pair is the gating contract: `parse(render(m)) == m`
for every well-formed module.

This document is the **complete LLM-targeted specification**. If you
are an LLM and this is in your context, you have everything you need
to produce valid Form-A. The file lives at
`crates/ailang-core/specs/form_a.md` next to the AST definitions, and
a unit test (`tests/spec_drift.rs`) walks every AST enum variant and
asserts its serde tag appears here — so this document cannot silently
fall behind the language.

## Why Form-A and not JSON

The hashable artefact is `.ail.json`, but no human or LLM should write
that directly. JSON-AST is a mechanical serialization with high
boilerplate (`{"k": "con", "name": "Int"}` per type reference, mandatory
field tags, every term wrapped). Form-A is the same information in a
Lisp-style S-expression dress that:

- omits structural noise (no field tags; positions carry meaning)
- has a real parser with positional error messages
- round-trips through `ail render` ↔ `ail parse` losslessly
- is the form every existing `examples/*.ail` is written in

LLMs generate Form-A; the toolchain converts to JSON.

## Conventions

- `NAME` is a bare identifier: letters, digits, `_`, `-`, `+`, `*`,
  `/`, `<`, `>`, `=`, `!`, `?`, `%`. Cannot start with a digit.
- `STRING` is a double-quoted UTF-8 literal: `"hello"`. Backslash
  escapes: `\"`, `\\`, `\n`, `\t`.
- `INT` is a signed decimal integer; leading `-` is allowed.
- Whitespace and `;`-prefixed line comments are insignificant.
- `?` after a clause means optional. `*` means zero or more.

## Module structure

```
(module NAME
  IMPORT*
  DEF*)
```

The module name MUST equal the file stem (`bench_list_sum.ail` →
`(module bench_list_sum ...)`).

## Imports

```
(import MODULE-NAME)
(import MODULE-NAME (as ALIAS))
```

The alias clause is optional. Imported modules are resolved relative
to the entry file's directory.

## Definitions

Five kinds, matched on the leading keyword:

### Function — `(fn ...)`

```
(fn NAME
  (doc STRING)?
  (suppress (code STRING) (because STRING))*
  (type FN-TYPE)
  (params NAME*)
  (body TERM))
```

`doc` is optional but recommended — it appears in the prose projection
and helps downstream readers (human and LLM).

`suppress` clauses silence advisory diagnostics for this def. The
`code` MUST be one of the registered codes (today: `over-strict-mode`).
The `because` MUST be a non-empty justification — empty / whitespace-
only `because` is itself an error (`empty-suppress-reason`).

`type` is a `(fn-type ...)` (possibly wrapped in `(forall ...)` for
polymorphic defs). All parameters of a `(fn ...)` MUST carry a mode
annotation — see *Modes* below.

`params` is a list of bare names that bind the parameters in `body`.
The list length must match the number of params in `type`.

### Data type — `(data ...)`

```
(data NAME
  (vars TYVAR+)?
  (doc STRING)?
  (ctor CTOR-NAME ARG-TYPE*)*)
```

`vars` makes the type polymorphic; absent means monomorphic. Each
`ctor` clause is one variant. `ARG-TYPE` is a `TYPE` — see below.

### Constant — `(const ...)`

```
(const NAME
  (doc STRING)?
  (type TYPE)
  (body TERM))
```

### Class — `(class ...)`

```
(class NAME
  (param TYVAR)
  (doc STRING)?
  (superclass (class CLASS-REF) (type TYVAR))?
  (method NAME (type FN-TYPE) (default TERM)?)*)
```

A class declaration introduces a typeclass with one type parameter (`param`)
and a list of method signatures.

`CLASS-REF` in the optional `superclass` clause follows the canonical-form
rule (see *Types* below): bare for same-module, `MODULE.CLASS` for
cross-module. The `superclass` slot is at most one — multi-superclass
chains are not yet supported.

Each `method` carries a function-typed signature. The bound type variable
named in `param` is in scope throughout the method's `(type ...)`. A
`(default ...)` clause provides a fallback implementation; absent means
the method is abstract-required (every instance MUST implement it).

Example (`examples/test_22c_user_class_e2e.ail`):

```
(class Foo
  (param a)
  (method foo
    (type (fn-type (params (borrow a)) (ret (con Int))))))
```

### Instance — `(instance ...)`

```
(instance
  (class CLASS-REF)
  (type TYPE)
  (doc STRING)?
  (method NAME (body LAM-TERM))*)
```

An instance declaration provides method implementations of `CLASS-REF` at
the concrete `TYPE`.

`CLASS-REF` follows the canonical-form rule: bare for same-module-to-
class (the instance and the class live in the same module), `MODULE.CLASS`
for cross-module (the class lives in another module — most commonly
`prelude.Show`, `prelude.Eq`, etc.).

Each `method` body is a `(lam ...)` term. The class's type parameter is
substituted for `TYPE` throughout the method body's parameter types and
return type; method bodies are type-checked under that substitution and
walk through the same identifier-resolution path as `(fn ...)` bodies,
so an unbound name inside a method body fires `[unbound-var]` at
`ail check`.

Two examples.

Same-module class + instance (`examples/mq3_class_eq_vs_fn_eq_classmod.ail`,
abbreviated):

```
(class MyEq (param a)
  (method myeq (type (fn-type (params (borrow a) (borrow a)) (ret (con Bool))))))
(instance
  (class MyEq)
  (type (con Int))
  (method myeq
    (body (lam (params (typed x (con Int)) (typed y (con Int))) (ret (con Bool)) (body true)))))
```

Cross-module qualified class (`examples/show_user_adt.ail`, abbreviated):

```
(instance
  (class prelude.Show)
  (type (con IntBox))
  (method show
    (body (lam (params (typed x (con IntBox))) (ret (con Str))
      (body (match x (case (pat-ctor MkIntBox n) (app int_to_str n))))))))
```

The `prelude.Show` qualifier is required here because `Show` is declared
in the `prelude` module, not the entry module. Writing `(class Show)`
bare would fail with `bare-cross-module-class-ref`.

## Types

Four shapes, all parenthesised except a bare type variable:

```
TYVAR-NAME                              ; type variable (e.g. `a`, `T`)
(con NAME TYPE-ARG*)                    ; type-constructor application
(fn-type (params PARAM*)
         (ret RETURN-PARAM)
         (effects EFFECT-NAME*)?)       ; function type
(forall (vars TYVAR+)
        (constraints (constraint CLASS-REF TYPE)+)?
        BODY-TYPE)                      ; polymorphic schema with optional constraints
```

`PARAM` and `RETURN-PARAM` are types, optionally wrapped in a mode
annotation:

```
TYPE                ; implicit mode (DO NOT USE in new (fn ...) defs)
(own TYPE)          ; caller transfers ownership; callee consumes
(borrow TYPE)       ; caller retains ownership; callee must not consume
```

`EFFECT-NAME` is a bare identifier — currently `IO` and `Diverge`.
Effects are a set; order is irrelevant.

Built-in type-constructors: `Int`, `Bool`, `Str`, `Unit`. User ADTs
use the name from the `(data ...)` def.

A `(forall ...)` may carry an optional `(constraints ...)` clause whose
inner items are `(constraint CLASS-REF TYPE)` pairs. Each constraint
requires the named class to have an instance at the given type; `TYPE`
is typically a type variable bound by the same `forall`. `CLASS-REF`
follows the canonical-form rule (bare for same-module, `MODULE.CLASS`
for cross-module). At a call site, every constraint must discharge — by
a matching instance in the workspace or by another constraint in the
caller's own schema. An undischargeable constraint fires `no-instance`
at `ail check`.

Examples:

```
(con Int)
(con List (con Int))
(fn-type (params (own (con List)) (borrow (con Int))) (ret (con Int)))
(forall (vars a) (fn-type (params (con List a)) (ret (con Int))))
(forall (vars a) (constraints (constraint prelude.Ord a))
                 (fn-type (params a a) (ret a)))
```

## Terms

Atom forms (no parens):

- `INT` — integer literal
- `STRING` — string literal
- `true`, `false` — bool literals
- `FLOAT` — IEEE-754 binary64 literal: e.g. `1.5`, `1.5e3`, `1e10`.
- `NAME` — variable reference (parameter, local, top-level def, or import alias)

Parenthesised forms:

```
(lit-unit)                              ; the unit value ()
(app FN ARG+)                           ; function application (≥1 arg)
(tail-app FN ARG+)                      ; tail-position application (Decision 8)
(do OP-NAME ARG*)                       ; effect operation
(tail-do OP-NAME ARG*)                  ; tail-position effect
(let NAME VALUE-TERM BODY-TERM)         ; binding
(let-rec NAME (params NAME*) (type FN-TYPE) (body TERM)
         (in BODY-TERM))                ; recursive let (fn-shaped)
(if COND-TERM THEN-TERM ELSE-TERM)      ; conditional
(match SCRUTINEE-TERM (case PAT BODY)+) ; pattern match (≥1 arm)
(term-ctor TYPE-NAME CTOR-NAME ARG*)    ; constructor application
(lam (params (typed NAME TYPE)*)
     (ret RETURN-TYPE)
     (effects EFFECT-NAME*)?
     (body TERM))                       ; anonymous function (Iter 8b)
(seq EFFECTFUL-TERM RESULT-TERM)        ; sequence; lhs evaluated for effect
(clone TERM)                            ; explicit RC clone (Iter 18c.1)
(reuse-as SOURCE-TERM BODY-TERM)        ; explicit reuse hint (Iter 18d.1)
```

Notes:

- `app` and `do` REQUIRE the right tag for the right thing.
  Constructors are NEVER called with `app`; always use `term-ctor`.
- `tail-app` / `tail-do` mark the call as occurring in tail position
  per Decision 8. Codegen lowers them to `musttail call`. Use the
  tail variant whenever a recursive call is the final action of an
  arm — it converts unbounded recursion into iteration. Non-tail
  variants are otherwise indistinguishable in semantics.
- `seq` is `(seq A B)` — A is evaluated for its effects and result
  discarded; B is the value of the whole expression. For pure A,
  prefer `(let _ A B)` or just drop A.
- `reuse-as` requires `SOURCE-TERM` to be a bare variable reference
  (a `NAME` in the term grammar). Anything else fails the linearity
  check with `reuse-as-source-not-bare-var`.

## Patterns

```
_                              ; wildcard; matches anything, binds nothing
NAME                           ; variable; binds the value to NAME
(pat-lit LIT-FORM)             ; literal match: integer, true/false, string
(pat-ctor CTOR-NAME FIELD*)    ; constructor; FIELD is itself a pattern
```

`LIT-FORM` is `INT`, `true`, `false`, or `STRING` — the same atoms used
as terms.

A pattern variable may bind at most once per arm. Pattern-binders are
in scope inside the arm body.

## Schema invariants enforced by `ail check`

The parser will accept syntactically valid Form-A that violates these;
the typechecker will not. Producing Form-A that obeys them yields
checked code on the first try.

1. **Mode annotations on every `(fn ...)` parameter.** Every type in
   the `(params ...)` clause of a `(fn ...)` definition's
   `(fn-type ...)` MUST be wrapped in `(own T)` or `(borrow T)`. The
   return type MUST also carry a mode whenever the type is heap-shaped
   (i.e. anything other than `(con Int)`, `(con Bool)`, `(con Unit)`,
   `(con Str)`). Implicit mode on a `(fn ...)` def is rejected.
2. **Constructors via `term-ctor`.** `Cons(1, Nil)` becomes
   `(term-ctor List Cons 1 (term-ctor List Nil))`, never
   `(app Cons 1 (app Nil))`.
3. **Effects on side-effecting fns.** A function whose body uses `(do ...)`
   MUST list every effect operation's effect in its `(effects ...)`
   clause. `IO` for `io/print_*`; `Diverge` for `diverge/*`.
4. **Tail correctness.** `(tail-app f x)` MUST appear in tail position
   — i.e. as the body of a fn, the last expression of a `(seq ...)`,
   the chosen arm of an `(if ...)` or `(match ...)`, or the body of
   a `(let ...)`. A `tail-app` outside a tail position is rejected.
5. **Linearity for own/borrow.** A parameter declared `(own T)` must
   be consumed exactly once on every reachable path; a `(borrow T)`
   must never be consumed. The diagnostic catalog has named codes
   for the typical violations.

## Pitfalls

LLMs without prior AILang exposure tend to make the following errors.
Reading these once before generating Form-A reduces re-roll cost
significantly.

- **Bare type names instead of `(con T)`.** Writing `Int` where a type
  is expected does NOT work — types live inside `(con ...)`. Only
  `TYVAR-NAME` (a single ident) parses as a type without parens, and
  it is interpreted as a type variable. So `(fn-type (params Int) ...)`
  parses as "function with one type-variable parameter named Int",
  which is almost certainly not what was meant.
- **Forgetting mode annotations.** `(fn-type (params (con List)) ...)`
  is accepted by the parser but rejected by the checker. Wrap every
  `(fn ...)` parameter in `(own ...)` or `(borrow ...)`.
- **Using `app` for constructors.** Constructors are NOT first-class
  functions. `(app Cons 1 Nil)` is interpreted as "apply variable
  `Cons` to ...", which then fails because `Cons` is not a fn.
- **Forgetting `tail-`.** A non-tail call in tail position works, but
  three million stack frames will overflow. For recursive fns where
  the recursive call is the final action, use `tail-app`.
- **Wrong arity in `(case (pat-ctor C f1 f2 ...) ...)`.** The number
  of pattern fields must equal the constructor's declared arity. The
  checker catches this but the message is clearer if you do too.
- **Strings inside `(suppress (because ...))` must be non-empty.** Empty
  is an error. Whitespace-only is an error. Write a real reason.

## Few-shot corpus

These four modules are real `examples/*.ail` content. Each one is
parseable and typechecks clean. Pattern-match against them when
generating new code.

### 1 — `hello.ail`: minimal IO program

```
(module hello
  (fn main
    (type (fn-type (params) (ret (con Unit)) (effects IO)))
    (params)
    (body (do io/print_str "Hello, AILang."))))
```

### 2 — `borrow_own_demo.ail`: mode annotations on a recursive list

```
(module borrow_own_demo

  (data List
    (doc "Monomorphic singly-linked Int list — boxed, recursive.")
    (ctor Nil)
    (ctor Cons (con Int) (con List)))

  (fn list_length
    (doc "Borrow xs, count its elements.")
    (type
      (fn-type
        (params (borrow (con List)))
        (ret (con Int))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Nil) 0)
        (case (pat-ctor Cons h t)
          (app + 1 (app list_length t))))))

  (fn sum_list
    (doc "Consume xs, sum its elements.")
    (type
      (fn-type
        (params (own (con List)))
        (ret (con Int))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Nil) 0)
        (case (pat-ctor Cons h t)
          (app + h (app sum_list t))))))

  (fn main
    (type (fn-type (params) (ret (con Unit)) (effects IO)))
    (params)
    (body
      (let xs
        (term-ctor List Cons 1
          (term-ctor List Cons 2
            (term-ctor List Cons 3
              (term-ctor List Nil))))
        (seq
          (do io/print_int (app list_length xs))
          (do io/print_int (app sum_list xs)))))))
```

### 3 — `lit_pat.ail`: literal patterns and nested ctor patterns

```
(module lit_pat

  (data IntList
    (ctor Nil)
    (ctor Cons (con Int) (con IntList)))

  (fn classify
    (type (fn-type (params (con Int)) (ret (con Int))))
    (params n)
    (body
      (match n
        (case (pat-lit 0) 100)
        (case (pat-lit 1) 200)
        (case _ 999))))

  (fn categorize_first
    (type (fn-type (params (own (con IntList))) (ret (con Int))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Nil) -1)
        (case (pat-ctor Cons (pat-lit 0) _) 0)
        (case (pat-ctor Cons h _) h)))))
```

### 4 — Tail-recursive sum (the canonical big-N pattern)

```
(module sum_demo
  (data IntList
    (ctor INil)
    (ctor ICons (con Int) (con IntList)))

  (fn sum_acc
    (doc "Tail-recursive accumulator.")
    (type
      (fn-type
        (params (own (con IntList)) (con Int))
        (ret (con Int))))
    (params xs acc)
    (body
      (match xs
        (case (pat-ctor INil) acc)
        (case (pat-ctor ICons h t)
          (tail-app sum_acc t (app + acc h))))))

  (fn sum_list
    (type
      (fn-type
        (params (own (con IntList)))
        (ret (con Int))))
    (params xs)
    (body
      (app sum_acc xs 0))))
```

Notice in (4): the recursive `sum_acc` call is `tail-app`, the addition
is plain `app`. The accumulator parameter is `(con Int)` (no mode —
`Int` is a primitive value type, not heap-shaped, so modes do not
apply to it).