AILang/design/models/0001-authoring-surface.md

Authoring surface — notation rationale whitepaper

Candidate notations (same map encoded in each)

The reference target — the polymorphic map from examples/list_map_poly.ail.json:

data List a where Nil | Cons a (List a)
fn map : forall a b. ((a) -> b, List a) -> List b
       = \f xs. match xs of Nil -> Nil
                          | Cons h t -> Cons(f(h), map(f, t))

(A) S-expression with fully-tagged AST nodes

(module list_map_poly

  (data List (vars a)
    (ctor Nil)
    (ctor Cons a (con List a)))

  (fn inc
    (type (fn-type (params (con Int)) (ret (con Int))))
    (params x)
    (body (app + x 1)))

  (fn map
    (type
      (forall (vars a b)
        (fn-type
          (params (fn-type (params a) (ret b)) (con List a))
          (ret (con List b)))))
    (params f xs)
    (body
      (match xs
        (case (pat-ctor Nil) (term-ctor List Nil))
        (case (pat-ctor Cons h t)
          (term-ctor List Cons
            (app f h)
            (app map f t)))))))

Grammar core (3-rule lexical layer + ~25 named-form productions):

sexpr  ::= atom | "(" sexpr* ")"
atom   ::= integer | string | ident
ident  ::= any maximal non-whitespace, non-paren run that is not
           a recognised integer or string literal.

The lexer recognises one delimiter (( / )) and whitespace. Every other maximal token is classified post-hoc:

• All-digit run with optional leading - → integer atom.
• "-delimited run → string atom.
• Otherwise → ident.

Consequence: arithmetic operators like + / - / * / / / %, qualified names like io/print_str, and cross-module references like std_list.map are all single ident tokens with no special lex rule. The only token delimiters are (, ), and whitespace.

One character is reserved within a token: $. Any identifier token containing $ is rejected by the lexer (LexError::ReservedDollar in crates/ailang-surface/src/lex.rs), because $ is reserved for the compiler's synthetic namespace (match-scrutinee, lifted-let-rec, and shadow-rename binders). Making $ unauthorable keeps that synthetic namespace collision-free by construction. The reservation is on the Form-(A) authoring surface only — $ inside a string literal or a comment is unaffected, and the canonical .ail.json deserialization path is intentionally not guarded. Bool literals (true, false) and unit ((lit-unit)) are disambiguated by parser context, not by lex. Comparison and equality are class methods (eq / compare) and named fns (float_eq / float_lt / etc.), not operators — see Prelude classes.

Every AST node form has a unique head keyword (module, data, fn, forall, fn-type, con, var, app, lam, match, case, pat-ctor, term-ctor, do, seq, ...). A bare atom in a positional slot (e.g. inside (con List a) second position) is a name reference whose sort is determined by the parent slot:

• inside (con NAME args...) second-and-later positions → type expression. Bare atom there ⇒ Type::Var { name }.
• inside (app HEAD args...) first position ⇒ Term::Var.
• inside (pat-ctor CTOR fields...) field positions ⇒ Pattern::Var.
• inside (case PAT BODY) second position ⇒ term.

There is no lexical case rule. To construct a value with a ctor, write (term-ctor TypeName CtorName args...). To match against one, write (pat-ctor CtorName fields...). Capitalised identifiers carry no special meaning to the parser. This rules out a class of silent errors ("I forgot to capitalise Cons and it parsed as a function call").

Pros: smallest formal grammar of any candidate (the lexical core is 3 rules; the named-form productions are uniform — every node a tagged list). Foreign-LLM bar lowest. Round-trip with the existing pretty-printer is a refactor of pretty.rs to emit this tagged form, plus a new parser.

Cons: paren density is high. (forall (vars a b) (fn-type ...)) has more visual nesting than the current pretty-printer's forall a. (...) -> .... Verbosity is ~2× JSON for the same node when measured in characters, but ~8× shorter in lines (the existing JSON box.ail.json of 160 lines becomes ~20 lines in this form).

(B) Indented record-style with explicit terminators

module std_list

data List(a):
  Nil
  Cons(a, List(a))
end

fn map:
  type: forall a b. fn(fn(a) -> b, List(a)) -> List(b)
  params: f, xs
  body:
    match xs:
      Nil          => Nil
      Cons(h, t)   => Cons(f(h), map(f, t))
    end
end

Grammar core (~20–30 productions): module-level (def/data/end), type sub-grammar (forall, fn, con, var), term sub-grammar (lam, match, ctor, app, lit, var, seq), pattern sub-grammar.

Pros: higher information density per line, closer to mainstream ML/Haskell shape. Cons: four sub-grammars instead of one. forall a b. fn(...) keeps a pseudo-precedence (-> binds tighter than the outer fn(...) wrapper). Foreign-LLM bar higher.

(C) Pretty-printer-as-source

Use exactly the format pretty::module already emits, plus a parser that accepts it. The existing pretty-printer's quirks (:: for type-of, [params] for fn-params, <a> for type-args, forall a. ..., !IO, () ambiguous between unit-arg-list and empty-form) become the spec.

Pros: zero churn — the existing pretty-printer is already the spec; only the inverse is missing. Round-trip is the identity by construction. Cons: the existing format mixes four mini-dialects (s-expr at term level, ML-shape at type level, square brackets for params, <> for type args). Formalising it crisply is harder than designing a uniform form from scratch.

The chosen form is (A), shipped as the ailang-surface crate (see authoring surface); the canonical JSON-AST it round-trips against is documented in Data model, and the round-trip property itself in Roundtrip Invariant.

For the prose projection used for human review (Form B), see prose projection.