Formal grammar
The grammar, token by token, kept in sync with the design document.
Notation.
::=defines a rule;?optional;*zero-or-more;+one-or-more;|alternative;( )groups;"…"is a literal terminal. Since the language uses{ } [ ] ( )as real tokens, they always appear inside quotes ("{","[") so they do not collide with the metasyntax.Newlineis a significant line break (see ASI, §1).Separators (central rule, from the design doc). The separator follows the kind of content, not the bracket. A value group (a positional, homogeneous list of values) separates with
,: function arguments, tuple elements, array/slice/collection literal elements, and the group-ish set members (error{A, B},Event{Send, Recv}, type argsMap[K, V]). A body of distinct members (each a named field, a case, or a statement) separates with;orNewline(combinable for readability): struct fields (in a declaration and in a struct literal), enum variants,matcharms, block statements. So a struct literal is distinct fields,Point{1; 2}, while an array literal is a value group,[]int{1, 2, 3}, even though both are delimited by{ }: the content decides, not the brace.Fidelity. The rules mirror the design doc section by section, kept in sync with it.
[decision]marks the few points where the grammar had to choose because the doc was silent (e.g., the disambiguation of{}in §6).
1. Lexicon (tokens)
Section titled “1. Lexicon (tokens)”Program ::= ModuleDecl? Item* (* ModuleDecl, if present, is the 1st thing in the file *)
Ident ::= (Letter | "_") (Letter | Digit | "_")*Letter ::= "a"…"z" | "A"…"Z"Digit ::= "0"…"9"HexDigit ::= Digit | "a"…"f" | "A"…"F"OctDigit ::= "0"…"7"BinDigit ::= "0" | "1"
(* Reserved keywords, never an Ident. The 32 from §27: *)Keyword ::= "fn" | "let" | "var" | "mut" | "const" | "decl" | "alias" | "union" | "module" | "use" | "if" | "else" | "match" | "loop" | "in" | "break" | "continue" | "return" | "defer" | "catch" | "yield" | "spawn" | "timeout" | "comptime" | "unsafe" | "assert" | "assume" | "pub" | "priv" | "as" | "true" | "false"
(* --- literals --- *)Literal ::= IntLit | FloatLit | DurationLit | SizeLit | StringLit | CharLit | BoolLitIntLit ::= DecInt | HexInt | OctInt | BinInt (* 4 bases + separator '_' *)DecInt ::= Digit (Digit | "_")*HexInt ::= "0x" HexDigit (HexDigit | "_")*OctInt ::= "0o" OctDigit (OctDigit | "_")*BinInt ::= "0b" BinDigit (BinDigit | "_")*FloatLit ::= DecInt "." DecInt (("e" | "E") ("+" | "-")? DecInt)?DurationLit ::= DecInt DurationUnit (* lexer converts → Duration, no import *)DurationUnit ::= "ns" | "ms" | "s" | "m" | "h" | "d" (* §14, see note *)SizeLit ::= DecInt SizeUnit (* lexer converts → usize in BYTES, no import (§14) *)SizeUnit ::= "b" | "kb" | "kib" | "mb" | "mib" | "gb" | "gib" | "tb" | "tib" (* b=byte; 'i'=base-2, only with prefix *)StringLit ::= '"' (StringChar | Interpolation)* '"'Interpolation ::= "{{" Expr "}}" (* §16, interpolation via Display *)CharLit ::= "'" Grapheme "'" (* one grapheme cluster; resolves to codepoint/byte/grapheme by context *)BoolLit ::= "true" | "false"
BuiltinValue ::= "none" | … (* 'none' = empty Optional AND @mm strategy; it is a builtin VALUE, not a keyword (§5) *)
Comment ::= "//" (up to Newline)
(* --- operators (tokens) --- *)ArithOp ::= "+" | "-" | "*" | "/" | "%" | "+%" | "-%" | "*%" (* wrapping add/sub/mul: +/-/* trap on overflow, the %-suffixed forms wrap (§4) *)BitwiseOp ::= "&" | "|" | "^" | "~" | "<<" | ">>" (* ~ is unary (complement); the rest binary *)CompareOp ::= "==" | "!=" | "<" | ">" | "<=" | ">="LogicalOp ::= "&&" | "||" | "!"CompoundAssign ::= "+=" | "-=" | "*=" | "/=" | "%=" (* arithmetic with '=' *) | "&=" | "|=" | "^=" | "<<=" | ">>=" (* bitwise with '=' *)ChannelArrow ::= "<-" | "->" | "<->" (* channel type AND send/receive operators (§4) *)Duration units. There are 6 (ns ms s m h d), as in §14 of the design doc (5s, 300ms, 10ns, 6m, 7h, 18d).
ASI (Newline only). The statement separator is the line break (Go style); the lexer closes the statement at the end of the line. The explicit ; exists for one-line cases (C-style loop clauses; inline arms/statements like unsafe { a; b }), but automatic insertion is triggered only by Newline.
2. Top-level items and declarations
Section titled “2. Top-level items and declarations”Item ::= Decorator* ItemBodyItemBody ::= FnDecl | MethodDecl | TypeDecl | AliasDecl | UnionDecl | Binding | UseDecl
(* --- function --- *)FnDecl ::= Visibility? "comptime"? "unsafe"? "fn" Ident GenericParams? "(" ParamList? ")" ("->" ReturnType)? BlockVisibility ::= "pub" | "priv"ParamList ::= Param ("," Param)* (* group in '()' → comma *)Param ::= Decorator* Ident ":" ParamType ("=" Expr)? (* "= Expr" = default value *)ParamType ::= "mut"? Type (* 'mut' = write-back passing (§6) *) | "..." Type (* variadic, '...' is a PREFIX (§7/§13) *)ReturnType ::= Type "==" Expr (* terse postcondition: -> u8 == cond (§5) *) | "(" NamedReturn ("," NamedReturn)+ ")" (* named tuple: -> (lo: u8, hi: u8): return ONLY; labels for @ensures (§5/§14) *) | Type (* includes tuple (a,b), Result[…], error{…} *)NamedReturn ::= Ident ":" Type
MethodDecl ::= "fn" "(" (Ident ":")? Type ")" Ident "(" ParamList? ")" ("->" ReturnType)? Block (* binding present = method; absent = associated function (§2) *)
(* --- decl: struct | enum | interface (the body disambiguates; §2) --- *)TypeDecl ::= "decl" Ident GenericParams? ("->" Kind)? "{" DeclBody "}" (* '-> Kind' optional, default '-> type'; '-> prop' = a proposition family (§21, D2) *)DeclBody ::= FieldList (* fields 'name: type' → struct *) | VariantList (* variants 'Name'/'Name(…)' → enum *) | SigList (* signatures 'fn …' → interface *)FieldList ::= Field (MemberSep Field)* MemberSep?Field ::= Decorator* Visibility? Ident ":" Type Decorator* (* @embeds after the type (§2) *)VariantList ::= Variant (MemberSep Variant)* MemberSep?Variant ::= Ident ("(" TypeList ")")? (* Name OR Name(payload) *) | Ident ":" ResultVariant (* index-refining variant, ONLY under a dependent head (§21, D3) *)ResultVariant ::= Type (* nullary constructor's result: Nil: Vec[T, 0] *) | "fn" GenericParams? "(" ParamList? ")" "->" Type (* Cons: fn[m: usize](head: T, tail: Vec[T, m]) -> Vec[T, m + 1] *)SigList ::= MethodSig (MemberSep MethodSig)* MemberSep?MethodSig ::= "fn" Ident "(" ParamList? ")" ("->" ReturnType)?Kind ::= "type" | "prop" (* the universe a decl produces: 'type' (default, the kind of §10) | 'prop' (a proposition, §21) *)
(* --- alias / union --- *)AliasDecl ::= "alias" Ident GenericParams? "=" RefinedType (* transparent synonym; parameterized with GenericParams (§10, e.g. alias StringTrie[V] = Trie[byte, V]); RefinedType allows a trailing @where refinement (§21); takes '=' (§2) *)UnionDecl ::= "unsafe"? "union" Ident "{" FieldList "}" (* union is always unsafe (§2/§5) *)RefinedType ::= Type Decorator* (* reference-by-type: i64 @where(i64 >= 0) — the value is named by its type, like @ensures(u8 > 0) (§21) *) | "(" Ident ":" Type ")" Decorator* (* named slot: (xs: List[T]) @where(xs.len > 0) — binds the value's name, like a named return -> (lo: u8) (§21) *)
MemberSep ::= ";" | Newline (* body in '{}' → ';' or Newline; NEVER ',' *)decl State { Idle; Running; Done } · decl Point { x: int; y: int } · decl Shape { Circle(int); Square }: members separated by ; (or Newline when multiline). Contrast with fn f(a: int, b: int), where the arguments in () separate with ,.
3. Bindings (value declaration)
Section titled “3. Bindings (value declaration)”Binding ::= BindKw? BindTarget BindRhsBindKw ::= "let" | "var" | "const" (* absent = immutable shortcut (':=') *)BindTarget ::= BindNames (* a, b (no parentheses) *) | "(" BindNames ")" (* (a, b) (with parentheses) *)BindNames ::= BindName ("," BindName)* (* names = group-ish → comma *)BindName ::= Ident | "_" (* '_' discards (§14) *)BindRhs ::= ":=" ExprList (* inferred: x := v | a, b := 0, 1 *) | ":" Type "=" Expr (* typed (Odin style): x: T = v (§6/§14) *)ExprList ::= Expr ("," Expr)*Semantics (annotated): := (or : T =) declares; a bare = only assigns to a var. _ := Expr is the only way to discard. const x := v ≡ comptime let. a, b := f() ≡ (a, b) := f() (matched by position).
4. Types
Section titled “4. Types”Type ::= PointerType | ManyPtrType | SliceType | ArrayType | TupleType | FunctionType | ChannelType | ErrorSetType | VariantSetType | GenericType | QualifiedType | NamedType
PointerType ::= "*" Type (* a single pointer; no *const/*mut (§6) *)ManyPtrType ::= "[" "*" "]" Type (* [*]T, many-pointer: N contiguous, no length; indexing is unsafe (§6) *)SliceType ::= "[" "]" Type (* []T = [*]T + length (§6) *)ArrayType ::= "[" (Expr | "_") "]" Type (* [N]T (N comptime) | [_]T (size inferred from the literal, §6) *)TupleType ::= "(" Type ("," Type)+ ")" (* (a, b): group in '()' → comma (§7) *)FunctionType ::= "fn" "(" TypeList? ")" ("->" Type)? (* fn(A) -> B (§9/§10) *)ChannelType ::= "Channel" "[" ChannelDir ("," ChannelDir)* "]"ChannelDir ::= "<-" Type | "->" Type | Type (* <-T send, ->T receive (§4) *)
ErrorSetType ::= "error" ("{" SetMembers "}")? (* 'error' = OPEN; 'error{…}' = CLOSED (§7) *)VariantSetType ::= NamedType "{" SetMembers "}" (* Event{Send, Receive}, in TYPE POSITION (§7) *)SetMembers ::= (SetMember ("," SetMember)*)? (* group-ish → comma; EMPTY = empty closed set = uninhabited: error{} = "does not err" (§7) *)SetMember ::= Ident (* a variant / tag *) | Ident "..." (* spread, '…' is POSTFIX: 'name...' (§7) *)
GenericType ::= (QualifiedType | NamedType) "[" TypeArg ("," TypeArg)* "]" (* List[int], Result[(int,int), E], box.Box[int] — a module-qualified base too (§15) *)TypeArg ::= Type | Expr (* type OR comptime value (e.g.: [N]) *)QualifiedType ::= Ident ("." Ident)+ (* c.gcc.int, module.Type; instantiate a qualified generic as QualifiedType "[" … "]" *)NamedType ::= Ident | PrimitiveTypeTypeList ::= Type ("," Type)*
PrimitiveType ::= IntType | FloatType | "bool" | "string" | "byte" | "bit" | "codepoint" | "grapheme" | "char" (* byte=u8, bit=u1, char=grapheme: builtin aliases (§14/§16) *) | "int" | "uint" | "isize" | "usize" | "type" (* the kind, a compile-time value (§10) *) | "noreturn" (* bottom type, divergence; fits any context (§14) *)IntType ::= ("i" | "u") DecInt (* iN/uN, N ∈ 1..65535 (§14) *)FloatType ::= "f16" | "bf16" | "f32" | "f64" | "f128" | "f256" | "float"Disambiguation Name{…} (§7). In type position, Name{…} is a VariantSetType (Event{Send}). In value position, it is a StructLit (Vec2{1; 2}). Position separates; the kind reinforces. error{…} is always an ErrorSetType (error is a contextual keyword: it names the builtin error domain in a type position and in error.Tag construction, but is not otherwise reserved). Note the set forms are type-position group-ish and separate their members with commas (error{A, B}, Event{Send, Recv}), like an array literal []int{1, 2, 3} (a value group), and unlike a struct literal Vec2{1; 2} (distinct fields, ;): the content decides the separator, not the brace (§1).
Builtins that are not keywords (they live here, §27): Result[T,E], Optional[T], Ptr, RawPtr, Generator[T], Duration.
5. Statements
Section titled “5. Statements”Block ::= "{" (Stmt MemberSep)* Stmt? "}"Stmt ::= Binding | ComptimeStmt | Assignment | LoopStmt | IfStmt | MatchStmt | ReturnStmt | BreakStmt | ContinueStmt | YieldStmt | DeferStmt | SpawnStmt | UnsafeStmt | StandaloneDecorator | FnDecl (* NESTED function: scope only, no capture (§14) *) | ExprStmt
ComptimeStmt ::= "comptime" (Binding | Block | IfStmt | LoopStmt | MatchStmt) (* comptime orthogonal over binding/block/if/loop/match; comptime fn is in FnDecl (§10) *)
(* --- assignment (≠ binding: bare '=', only for var) --- *)Assignment ::= LValue AssignOp Expr | LValueList "=" ExprList (* a, b = b, a: swap/parallel (§14) *)AssignOp ::= "=" | CompoundAssign (* = | += -= *= /= %= &= |= ^= <<= >>= *)LValue ::= Ident | LValue "." Ident | LValue "[" Expr "]" | "*" LValueLValueList ::= LValue ("," LValue)*
ReturnStmt ::= "return" Expr? | "return" MatchExpr (* distributed 'return' (§14); `if` is statement-only, use the ternary for a value *)BreakStmt ::= "break" Ident? (* optional LOOP LABEL, never a value (§14); a loop delivers via return *)ContinueStmt ::= "continue" Ident? (* optional loop label *)YieldStmt ::= "yield" Expr (* generators (§11) *)DeferStmt ::= "defer" Expr (* LIFO cleanup (§14) *)
(* --- unified loop (§14) --- *)LoopStmt ::= (Ident ":")? "loop" LoopHeader? Block (* optional Go-style label; also usable in value position (Primary), delivering via return *)LoopHeader ::= Expr (* boolean condition → while *) | Ident "in" Expr (* IDENT in iterable/range → for-each *) | Binding ";" Expr ";" SimpleStmt (* C-style; explicit ';' delimits the 3 parts *)SimpleStmt ::= Assignment | ExprStmtRangeExpr ::= Expr ".." Expr | Expr "..=" Expr (* '..' exclusive, '..=' inclusive *)
IfStmt ::= IfExprIfExpr ::= "if" Expr Block ("else" (IfExpr | Block))?
SpawnStmt ::= "spawn" (CallExpr | Block) ErrorTrailer? (* spawn f(x) catch|e|{} | spawn { … } *)UnsafeStmt ::= "unsafe" Block (AssertTrailer | AssumeTrailer)? (* 'unsafe expr' appears as Unary in Expr *)StandaloneDecorator ::= Decorator (Binding | Block)? (* @mm(arena), @state x := v, @effect { … } *)ExprStmt ::= ExprMatchStmt ::= MatchExpr6. Expressions and precedence
Section titled “6. Expressions and precedence”Precedence from highest (binds strongest) to lowest. Adopted from Go, the most common among Zig/Go/Odin/Erlang/Gleam (Odin and Erlang agree on the bitwise grouping; only Zig separates them). A universal property across the 5: comparison sits below bitwise.
Level Operators1 postfix/access x.y x.f() x() x[i] x as T x@decorator2 unary (prefix) -x !x ~x *x(deref) &x(addr)3 multiplicative * / % << >> &4 additive + - | ^5 comparison == != < > <= >=6 logical AND &&7 logical OR ||8 ternary (lowest) ? : (assignment is a statement, off the expression ladder)Expr ::= TernaryTernary ::= LogicalOr ("?" Expr ":" Expr)? (* cond ? a : b (§14) *)LogicalOr ::= LogicalAnd ("||" LogicalAnd)*LogicalAnd ::= Comparison ("&&" Comparison)*Comparison ::= Additive (CompareOp Additive)* (* string uses these byte-by-byte; Unicode semantics via method (§16) *)Additive ::= Multiplicative (("+" | "-" | "|" | "^") Multiplicative)* (* '+' concatenates string *)Multiplicative ::= Unary (("*" | "/" | "%" | "<<" | ">>" | "&") Unary)*Unary ::= UnaryPrefix* PostfixUnaryPrefix ::= "-" | "!" | "~" | "*" | "&" (* *deref; &addr *)Postfix ::= Primary PostfixOp*PostfixOp ::= "." Ident (* field / method without args *) | "." Ident "(" ArgList? ")" (* method via UFCS: x.f(y) ≡ f(x, y) (§14) *) | "(" ArgList? ")" (* call *) | "[" Expr "]" (* indexing *) | "[" Expr? (".." | "..=") Expr? "]" (* slice VIEW, aliases the backing; bounds optional (§6) *) | "[" Expr? ":" Expr? "]" (* slice COPY, independent O(n); bounds optional (§6) *) | "[" TypeArg ("," TypeArg)* "]" (* comptime args: collect[List]() (§10) *) | "as" Type (* conversion (§2/§16) *) | ValueDecorator (* result @transfer (§5) *) | ErrorTrailer (* catch|e| / match|e| / assert / assume (§5/§7) *) | ChannelTrailer (* <- / <-> with timeout (§4) *)
Primary ::= Literal | BuiltinValue | Ident | EnumShorthandLit (* .Variant: enum inferred from the expected type (§7, §16) *) | "(" Expr ")" (* grouping *) | TupleLit | StructLit | ArrayLit | MatchExpr | LoopStmt | RangeExpr (* match and loop are value forms (deliver via return); `if` is NOT here: statement-only, its value form is the ternary `c ? a : b` (§14). `Lambda` is NOT here either: it is reachable ONLY from `Arg`, which is what makes "only as a direct argument" (§6/§14) a GRAMMAR fact rather than a checker rule *) | ReceiveExpr
EnumShorthandLit ::= "." Ident (* leading-dot enum literal: `.Red`, `.semantic`; enum inferred from context (Zig-style). Only at expr start; `x.field` is a PostfixOp. Un-inferrable = error. *)
TupleLit ::= "(" Expr ("," Expr)+ ")" (* (a, b): group in '()' → comma *)StructLit ::= StructHead "{" (FieldInits | FieldVals)? "}" (* Vec2{x: 1; y: 2} | Vec2{1; 2}: distinct fields → MemberSep (§1) *)StructHead ::= (QualifiedType | NamedType) ("[" TypeArg ("," TypeArg)* "]")? (* Vec2 | Box[int] | box.Point | box.Box[int]: local or module-qualified, plain or generic (§15) *)FieldInits ::= FieldInit (MemberSep FieldInit)*FieldVals ::= Expr (MemberSep Expr)* (* positional struct literal: distinct fields, not a value group *)FieldInit ::= Ident ":" ExprArrayLit ::= (SliceType | ArrayType) "{" (Expr ("," Expr)*)? "}" (* []int{1, 2, 3} | [3]int{1, 2, 3} | [_]int{1, 2, 3}: elements are a VALUE GROUP → comma (§1) *)ArgList ::= Arg ("," Arg)*Arg ::= "mut"? Expr | Lambda (* 'mut' at the call site (§6); lambda as arg *)
Lambda ::= "fn" "(" ParamList? ")" ("=>" Expr | Block) (* ONLY as a direct argument (§14) *)
(* --- channels (§4) --- *)ReceiveExpr ::= "->" Expr (* receive: data := -> chan (prefix, value position) *)ChannelTrailer ::= "<-" Expr (* send: chan <- data *) | "<->" Expr "timeout" "(" Expr ")" (* sync req-reply; timeout REQUIRED *)ValueDecorator ::= "@" ("transfer" | "pin" | "unpin") | "@" "promote" "(" DecoratorArgs ")" (* node @promote(gc, deep) *)[decision: resolved] Separator by content, not by bracket. A struct literal is a body of distinct fields, so it separates by ; or Newline (Vec2{1; 2} or the multi-line form). An array/slice literal is a value group of homogeneous elements, so it separates by , ([]int{1, 2, 3}), the same as the other value groups (arguments, tuples, set members). Both are delimited by { }, but the content decides the separator, not the brace: distinct members (fields, variants, arms, statements) take ;/Newline; a positional value group takes ,. (This refines an earlier “all { } bodies use ;” phrasing, which was too coarse: array elements are not distinct fields.)
7. Match and patterns
Section titled “7. Match and patterns”MatchExpr ::= "match" Expr "{" MatchArms "}" (* WITH subject → switch/pattern (§14) *) | "match" "{" SelectArms "}" TimeoutTrailer? (* WITHOUT subject → select (§4) *)
ErrorTrailer ::= "match" "|" Ident "|" "{" MatchArms "}" (* op match |e| { }, branches (§7) *) | "catch" "|" Ident "|" Block (* op catch |e| { }, error as a unit (§7) *) | AssertTrailer | AssumeTrailerAssertTrailer ::= "assert" "(" Expr ")" (* checks: runtime verifies, panics if false (§5) *)AssumeTrailer ::= "assume" StringLit (* trusts: asserts without a check and without a license for UB (§5) *)
MatchArms ::= MatchArm (MemberSep MatchArm)* MemberSep?MatchArm ::= Pattern "=>" ArmBodyArmBody ::= Block | ReturnStmt | BreakStmt | ContinueStmt | ExprStmtSelectArms ::= SelectArm (MemberSep SelectArm)* MemberSep?SelectArm ::= (BindName ":=")? ReceiveExpr "=>" ArmBody (* data := -> chan_a => handle(data) *)TimeoutTrailer ::= "timeout" "(" Expr ")" Block (* } timeout(5s) { … }; absent=infinite; timeout(0)=poll *)
Pattern ::= SubPattern ("|" SubPattern)* (* or-pattern 'A | B' (§14) *)SubPattern ::= "_" (* wildcard, ONLY open domain (§7/§14) *) | Literal | "Ok" "(" Pattern ")" | "Err" "(" Pattern ")" | VariantPattern | Ident (* binding, or variant without payload *)VariantPattern ::= QualName ("(" PatternList ")")? (* error.NotFound | Send(m) | Click(x, y) *)QualName ::= Ident ("." Ident)*PatternList ::= Pattern ("," Pattern)*The arms of match/select use MemberSep (; or Newline), the same {} rule as declarations. Never a comma. Exhaustiveness: a closed domain (enum, error{…}, set of variants, whitelist) requires all the variants the type admits and forbids _; an open domain (int, string, bare error) requires _.
8. Decorators (sigil @)
Section titled “8. Decorators (sigil @)”Decorator ::= "@" Ident ("(" DecoratorArgs ")")? (* with args → '()'; pure tag → without (§14) *)DecoratorArgs ::= DecoratorArg ("," DecoratorArg)* (* args = group in '()' → comma *)DecoratorArg ::= Ident ":" Expr (* named: strategy: rest_for_one *) | Expr (* positional: arena, gc, none, 16mb, x86 *)Positions (from §5/§14/§20). Declaration prefix (@repr(c) decl …, @component fn …, @test fn …, @supervisor(cfg) spawn …); value postfix (result @transfer, node @promote(gc, deep)); standalone statement / reactive binding (@mm(arena), @state x := v, @effect { … }); on a parameter/field (value: *Record @mm(c), motor: Motor @embeds(methods)).
@generator is an ordinary decorator. It can come above the function (on its own line) or inline before the fn, like any other decorator, captured by Decorator* in Item. There is no fixed slot in the FnDecl header (the order pub? comptime? @generator? unsafe? fn in the doc is just a writing convention).
9. Modules (§14/§15)
Section titled “9. Modules (§14/§15)”ModuleDecl ::= "module" ModulePath (* at the TOP of the file, Go/Odin 'package' style *)UseDecl ::= "use" ModulePath (* use json → json.parse(…) *) | "use" ModulePath "." "{" Ident ("," Ident)* "}" (* use json.{parse, decode} *) | "use" ModulePath "as" Ident (* use json as j *) | "use" ModulePath "." Ident "(" ArgList? ")" (* inline: use json.parse(data) *)ModulePath ::= Ident ("." Ident)*
GenericParams ::= "[" GenericParam ("," GenericParam)* "]"GenericParam ::= TypeParam | ValueParam (* a type parameter OR a comptime value parameter *)TypeParam ::= Ident HKTParams? ConstraintSpec? (* T | T: {…} | T + I | C[_] | C[_: {…}]: {…} + I *)ValueParam ::= Ident ":" Type (* a comptime value of ANY type: [n: usize], [flag: bool], [p: Point] (§10). The Type may name an EARLIER type-param → dependent value-param, e.g. [A, x: A] (§21, D1). Disambiguation: ':' then '{' is a whitelist on a TypeParam; ':' then a Type is a ValueParam. *)HKTParams ::= "[" "_" ConstraintSpec? "]" (* C[_] unapplied; ConstraintSpec here = constraint on the ELEMENT (§10) *)ConstraintSpec ::= Whitelist ("+" Interface)* (* strict rule §10: ':' is ONLY whitelist (membership), *) | ("+" Interface)+ (* '+' is ONLY interface (implementation): the name does not say which, hence 2 symbols *)Whitelist ::= ":" "{" TypeList "}" (* ': {List, Set}': belongs to the set *)Interface ::= NamedType (* '+ Writeable', implements the interface *)module path declares, at the top of the file, which module the file belongs to (like Go’s package). The resolution system (tree, paths, visibility) is in §15 of the design doc.
10. Notes and decisions
Section titled “10. Notes and decisions”Resolved in this round (all confirmed by you):
- Numeric literals: 4 bases (
0b/0o/0x/decimal) + separator_. - Separators (by content, not bracket): value groups
,(args, tuples, set members, array/slice literals[]int{1, 2, 3}); bodies of distinct members;/Newline (declbodies, enum variants,matcharms, blocks, struct literalsVec2{1; 2}). Both literals use{ }; the content decides (§1). - Boolean operators:
&&||!(symbol spelling). - Precedence: Go’s (the most common).
- Bitwise + compound:
& | ^ ~ << >>; compound+= -= *= /= %= &= |= ^= <<= >>=. none: builtin value (empty Optional +@mmstrategy), not a keyword.@generator: ordinary decorator (above or inline), no fixed slot.module: declaration at the top of the file (Go’spackagestyle).- ASI: triggered only by Newline; explicit
;for one-line cases. ->receive vs->return type: same glyph, disambiguated by position (channel expression vs signature).
Also resolved in this round:
++/--: removed. Increment/decrement do not enter the language (use+= 1/-= 1), aligned with the 5 references and with the doc’s explicitness.- Separators in the design doc: synced. The
declbodies (andunion) switched to;, and the §14 note was adjusted; grammar and doc match again. @generatorin the doc: decorator note added (above or inline, no fixed slot).- Duration units: the 6 confirmed (
ns ms s m h d).
Resolved in this round (post-feedback review):
- Strict constraint rule:
:introduces only a whitelist{…}(membership);+introduces only an interface (implementation).T: DisplaybecameT + Display. HKT: element constraint inside[_ …], container constraint after]; all forms derive fromGenericParam ::= Ident HKTParams? ConstraintSpec?. Reason: a name does not distinguish “is the type Foo” from “implements Foo”, so two symbols. assume(new keyword, 32 total):assertis now only the checkable formassert (cond)(checks, panics if false); the weak form (asserting without checking, without a license for UB) becameassume "reason". Two distinct trailers (AssertTrailer/AssumeTrailer).- Operators on string: allowed byte-by-byte:
==/!=(byte equality),</>/<=/>=(lexicographic order). Onlys[i]remains banned (ambiguous unit); Unicode semantics (normalization, collation) via method. - Named tuple in the return:
-> (lo: u8, hi: u8)is valid only in return position (slot labels for@ensures), not as a general named tuple-type. - Extension syntax stays out of this grammar: this grammar describes only the core (
.mko). A compiler extension (section 20 of the design doc) may bring its own grammar for the file types it registers (e.g., the markup of.mkoui) and define its own decorators; none of that goes here. The core is closed; what each extension adds is specified by it.
11. Verification layer (§21 of the design)
Section titled “11. Verification layer (§21 of the design)”The core verification constructs. Most of the layer is ordinary decorators, captured by Decorator* with no new production: @must_consume/@consume_once (type-level ownership on a decl), @pure/@total (fences), @proof (the soundness fence over a dependent family or function). What adds grammar is threefold, and it all reuses existing shapes: refinements (RefinedType, §2), the dependent-type deltas (ValueParam in GenericParam, the decl-head Kind, and the index-refining Variant/ResultVariant, all §2), and session protocols (below).
(* --- session protocols: the @protocol decorator selects a step-body for the decl (§21) --- *)ProtocolDecl ::= "@protocol" "decl" Ident GenericParams? "{" ProtoBody "}" (* @protocol makes the '{}' a ProtoBody, not a DeclBody *)ProtoBody ::= ProtoStep (MemberSep ProtoStep)* MemberSep?ProtoStep ::= Type ("@sends" | "@receives") (* postfix: Credentials @sends, Token @receives (prefix '@sends Type' also accepted) *) | ("@sends" | "@receives") "match" "{" ProtoArms "}" (* @sends match = I choose (internal choice); @receives match = peer chooses (external) *) | "loop" "{" ProtoBody "}" (* recursion *) | "continue" (* back to the enclosing loop *) | "_" (* end of the protocol *)ProtoArms ::= ProtoArm (MemberSep ProtoArm)* MemberSep?ProtoArm ::= Ident "=>" (("{" ProtoBody "}") | ProtoStep | "_")
(* --- dual: the mirror endpoint; a comptime type-operator, joins the Type forms --- *)DualType ::= "dual" Type (* Channel[dual Auth]: swaps every @sends ↔ @receives, including @sends match ↔ @receives match (§21) *)DualType is an additional alternative of Type (a prefix type-operator, like a builtin over types), so dual Auth is legal wherever a type is expected — most usefully Channel[dual Auth], where the spawn contract (§4 of the design) checks the two endpoints are complements.
No keyword grows. The whole layer reuses match, loop, continue, _ and fn, plus the @-namespace for its decorators; the 32-keyword set (§7 above) is unchanged. type gains the sibling universe prop in Kind (both lowercase builtins, like int/bool), not a new keyword.
@by is a deferred core delta, not yet grammar’d here. The tactic block @by { … } (§21) is a decorator-gated goal-threading block — new block semantics, so a core delta, but realized only in the self-hosting era (when use compiler exposes the AST as a library type). It is named here so it is not forgotten; its production is added when it lands.
Model checking is an extension, so its grammar is out. @spec and the spec.* temporal library (§21) belong to the model-checking extension, and by the closing note of §10 above, an extension’s grammar is not part of the core and does not appear in this document.
Resolved in this round (the verification layer, §21 of the design):
- Ownership
@must_consume/@consume_once: type-level decorators ondecl, no new production. - Refinement
@where:RefinedTypeon analiasRHS (and via the trailing/leadingDecorator*on a field/param) — reference-by-type or a named slot(x: T), reusing the named-return device of §14. No magic binder. - Value-params, generalized (D1):
GenericParam ::= TypeParam | ValueParam; aValueParamis a comptime value of any type, whose type may name an earlier type-param (dependent). This also closes a prior gap — value-params were used in the design doc but were not in the production. - Decl-head kind (D2):
("->" Kind)?onTypeDecl;Kind ::= "type" | "prop".->reuses “produces”;:keeps meaning field/param binding only. - Index-refining variant (D3):
VariantgainsIdent ":" ResultVariant(nullary result type, or afn[…](…) -> …constructor), valid only under a dependent head. - Sessions:
@protocol declwith aProtoBodyof@sends/@receivessteps,matchfor choice (direction = who chooses),loop/continue/_;dualas a type-operator. Only aChanneltyped by a protocol is walked as a session. - Definitional equality (D4) and Σ/Π (D5) are checker/typing powers, not surface grammar; they add no productions.