Grammar

This page is the formal grammar of Faber, written as EBNF productions. A production is one rule: it names a piece of the language and says what it is built from, for example that a loop is a keyword, a binding, and a block. Quoted words are the words you write, shown in this locale's spellings; uppercase names are lexical tokens. You do not need to read any of this to write Faber, because the cheat sheet and the language pages teach each form by example. The productions are here for tools, models, and anyone checking an edge case against the parser's own definition.

This file is generated from docs/grammar/source.fg, its sidecar.en.toml and its prose.en.md, and docs/grammar/glossary.vi.toml; hand edits fail the locale-render gate. Production IDs are the grammar's stable snake_case spine and their anchors are derived from those IDs.

Grammar#

The grammar below is the identity rendering of the validated source. Normative detail is kept in prose.en.md beside this file and rendered as documentation; the source remains the syntax authority.

# [001] fab_file
fab_file ::= frontmatter? program
# [002] frontmatter
frontmatter ::= FRONTMATTER_DELIMITER NEWLINE TOML_LINES FRONTMATTER_DELIMITER NEWLINE?
# [003] program
program ::= regio_decl? statement*
# [004] regio_decl
regio_decl ::= 'vùng' IDENTIFIER
# [005] statement
statement ::= annotation* statement_core | ad_handler_decl
# [006] ad_handler_decl
ad_handler_decl ::= annotation* ad_annotation annotation* functio_decl
# [007] statement_core
statement_core ::= importa_decl | binding_decl | functio_decl | genus_decl | implendum_decl | typus_decl | ordo_decl | discretio_decl | schema_decl | si_stmt | dum_stmt | itera_stmt | elige_stmt | discerne_stmt | custodi_stmt | fac_stmt | redde_stmt | reddet_stmt | tacebit_stmt | cede_stmt | rumpe_stmt | perge_stmt | tacet_stmt | iace_stmt | adfirma_stmt | requirit_stmt | reice_stmt | nota_stmt | incipit_stmt | incipiet_stmt | ex_stmt | probandum_decl | proba_stmt | block_stmt | inc_dec_stmt | expr_stmt
# [008] binding_decl
binding_decl ::= fixum_decl | sit_decl | array_destruct | object_destruct | figendum_decl
# [009] expr_stmt
expr_stmt ::= expression
# [010] block_stmt
block_stmt ::= '{' statement* '}'
# [011] const_init
const_init ::= insere_expr | expression
# [012] insere_expr
insere_expr ::= 'nhúng' STRING
# [013] fixum_decl
fixum_decl ::= ('hằng' | 'biến') type_annotation IDENTIFIER (('←' expression) | ('=' const_init) | ('↤' assignment inline_default?) | ('↢' expression))?
# [014] figendum_decl
figendum_decl ::= ('đợi_hằng' | 'đợi_biến') type_annotation IDENTIFIER '←' expression
# [015] sit_decl
sit_decl ::= 'đặt' IDENTIFIER (('←' | '↢') expression)?
# [016] array_destruct
array_destruct ::= ('hằng' | 'biến') array_pattern '←' expression
# [017] object_destruct
object_destruct ::= ('hằng' | 'biến') object_pattern '←' expression
# [018] functio_decl
functio_decl ::= 'hàm' IDENTIFIER generic_params? '(' param_list ')' func_modifier* callable_posture? return_clause? alternate_exit_clause? block_stmt
# [019] param_list
param_list ::= (parameter (',' parameter)*)?
# [020] generic_params
generic_params ::= '<' (type_param_list (',' size_param_list)? | size_param_list) '>'
# [021] type_param_list
type_param_list ::= generic_param (',' generic_param)*
# [022] size_param_list
size_param_list ::= size_param (',' size_param)*
# [023] generic_param
generic_param ::= IDENTIFIER generic_bound? generic_type_default?
# [024] size_param
size_param ::= 'kích_thước' IDENTIFIER generic_size_default?
# [025] generic_bound
generic_bound ::= 'thực_thi' contract_ref ('∩' contract_ref)*
# [026] contract_ref
contract_ref ::= IDENTIFIER ('<' type_annotation (',' type_annotation)* '>')?
# [027] generic_type_default
generic_type_default ::= '=' type_annotation
# [028] generic_size_default
generic_size_default ::= '=' NATURAL
# [029] call_type_args
call_type_args ::= '<' type_annotation (',' type_annotation)* '>'
# [030] parameter
parameter ::= 'còn_lại'? type_annotation IDENTIFIER 'tự_nguyện'? ('như' IDENTIFIER)? ('hoặc_nếu_rỗng' expression)?
# [031] func_modifier
func_modifier ::= 'đối_số' IDENTIFIER | 'lỗi' IDENTIFIER | 'thoát' (IDENTIFIER | NATURAL) | 'bất_biến' | 'ném_lỗi' | 'lựa_chọn' IDENTIFIER
# [032] callable_posture
callable_posture ::= 'async' | 'sinh' | 'async_sinh'
# [033] return_clause
return_clause ::= '→' type_annotation
# [034] alternate_exit_clause
alternate_exit_clause ::= '⇥' type_annotation
# [035] ergo_joint
ergo_joint ::= 'do_đó'
# [036] clausura_joint
clausura_joint ::= '∴'
# [037] clausura_expr
clausura_expr ::= compact_clausura_expr | clausura_legacy_expr
# [038] compact_clausura_expr
compact_clausura_expr ::= clausura_signature clausura_joint (expression | fac_block)
# [039] clausura_signature
clausura_signature ::= (clausura_param | '(' clausura_params? ')') closure_modifier? return_clause? alternate_exit_clause?
# [040] closure_modifier
closure_modifier ::= 'tự_do' | 'hạt_nhân'
# [041] fac_block
fac_block ::= 'làm' block_stmt cape_clause?
# [042] clausura_legacy_expr
clausura_legacy_expr ::= 'đóng' clausura_params? closure_modifier? ('→' type_annotation)? (':' expression | block_stmt)
# [043] clausura_params
clausura_params ::= clausura_param (',' clausura_param)*
# [044] clausura_param
clausura_param ::= type_annotation IDENTIFIER
# [045] genus_decl
genus_decl ::= 'kiểu' IDENTIFIER generic_params? ('thực_thi' contract_ref ((',' | '∩') contract_ref)*)? '{' genus_member* '}'
# [046] genus_member
genus_member ::= annotation* (genus_field_decl | functio_method_decl)
# [047] genus_field_decl
genus_field_decl ::= ('hằng' | 'biến' | 'tĩnh') type_annotation IDENTIFIER 'tự_nguyện'? ('=' const_init)?
# [048] field_decl
field_decl ::= ('hằng' | 'biến' | 'tĩnh')? type_annotation IDENTIFIER 'tự_nguyện'? ('=' const_init)?
# [049] functio_method_decl
functio_method_decl ::= 'hàm' IDENTIFIER generic_params? '(' param_list ')' func_modifier* callable_posture? return_clause? alternate_exit_clause? block_stmt
# [050] annotation
annotation ::= nucleum_annotation | radix_annotation | braced_annotation | annotation_sugar
# [051] annotation_name
annotation_name ::= ANNOTATION_NAME
# [052] braced_annotation
braced_annotation ::= '@' annotation_name '{' annotation_field_list? '}'
# [053] annotation_field_list
annotation_field_list ::= annotation_field (',' annotation_field)*
# [054] annotation_field
annotation_field ::= ANNOTATION_FIELD_NAME '=' (expression | concrete_type)
# [055] annotation_sugar
annotation_sugar ::= '@' annotation_name NON_NEWLINE_TOKEN* NEWLINE
# [056] nucleum_annotation
nucleum_annotation ::= nucleum_sugar | nucleum_braced
# [057] nucleum_sugar
nucleum_sugar ::= '@' 'hạt_nhân' nucleum_modifier? NEWLINE
# [058] nucleum_braced
nucleum_braced ::= '@' 'hạt_nhân' '{' nucleum_field_list? '}'
# [059] nucleum_modifier
nucleum_modifier ::= 'mảnh'
# [060] nucleum_field_list
nucleum_field_list ::= nucleum_field (',' nucleum_field)*
# [061] nucleum_field
nucleum_field ::= 'mảnh' '=' ('đúng' | 'sai')
# [062] radix_annotation
radix_annotation ::= '@' 'radix' radix_directive NEWLINE
# [063] radix_directive
radix_directive ::= 'làn' STRING | 'backward' STRING | 'contract' STRING | 'kiểu_tên' IDENTIFIER 'vào' concrete_type+
# [064] ad_annotation
ad_annotation ::= '@' 'gọi' ASCII_STRING NEWLINE
# [065] implendum_decl
implendum_decl ::= 'giao_ước' IDENTIFIER generic_params? '{' implendum_method_decl* '}'
# [066] implendum_method_decl
implendum_method_decl ::= annotation* 'hàm' IDENTIFIER '(' param_list ')' func_modifier* callable_posture? return_clause? alternate_exit_clause?
# [067] typus_decl
typus_decl ::= 'kiểu_tên' IDENTIFIER generic_params? '=' type_annotation
# [068] ordo_decl
ordo_decl ::= 'liệt_kê' IDENTIFIER '{' enum_member (',' enum_member)* '}'
# [069] enum_member
enum_member ::= IDENTIFIER ('=' ('-'? NUMBER | STRING))?
# [070] discretio_decl
discretio_decl ::= 'hợp_nhất' IDENTIFIER generic_params? '{' union_fields? variant (',' variant)* '}'
# [071] union_fields
union_fields ::= annotation+ field_decl union_member*
# [072] union_member
union_member ::= annotation* field_decl
# [073] variant
variant ::= IDENTIFIER ('{' variant_fields '}')?
# [074] variant_fields
variant_fields ::= (type_annotation IDENTIFIER)*
# [075] schema_decl
schema_decl ::= 'lược_đồ' IDENTIFIER '{' (schema_column (NEWLINE schema_column)*)? '}'
# [076] schema_column
schema_column ::= 'cột' type_annotation IDENTIFIER (':' IDENTIFIER)?
# [077] importa_decl
importa_decl ::= importa_record | importa_sugar
# [078] importa_record
importa_record ::= 'nhập' '{' import_field_list '}'
# [079] import_field_list
import_field_list ::= import_field (',' import_field)*
# [080] import_field
import_field ::= ex_field | visibilitas_field | nomen_field | ut_field | omnia_field
# [081] ex_field
ex_field ::= 'từ' '=' STRING
# [082] visibilitas_field
visibilitas_field ::= 'visibilitas' '=' publica
# [083] nomen_field
nomen_field ::= 'tên' '=' IDENTIFIER
# [084] ut_field
ut_field ::= 'như' '=' IDENTIFIER
# [085] omnia_field
omnia_field ::= 'mọi' '=' IDENTIFIER
# [086] importa_sugar
importa_sugar ::= 'nhập' 'từ' STRING publica? (named_import | wildcard_import | selective_import)?
# [087] publica
publica ::= 'công_khai'
# [088] named_import
named_import ::= IDENTIFIER ('như' IDENTIFIER)?
# [089] wildcard_import
wildcard_import ::= '*' 'như' IDENTIFIER
# [090] selective_import
selective_import ::= 'hằng' import_value_binding (',' import_value_binding)*
# [091] import_value_binding
import_value_binding ::= IDENTIFIER ('như' IDENTIFIER)?
# [092] type_annotation
type_annotation ::= union_hole_type | concrete_type
# [093] concrete_type
concrete_type ::= intersection_type ('∪' intersection_type)*
# [094] union_hole_type
union_hole_type ::= ('ra' | 'vào' | 'sở_hữu' | 'sao_chép')? '∪'
# [095] intersection_type
intersection_type ::= owned_type ('∩' owned_type)*
# [096] owned_type
owned_type ::= ('ra' | 'vào' | 'sở_hữu' | 'sao_chép')? base_type
# [097] base_type
base_type ::= hole_type | function_type | width_type_sugar | ratio_type | failable_promissum_type | qualified_type type_arguments?
# [098] failable_promissum_type
failable_promissum_type ::= IDENTIFIER '<' type_annotation alternate_exit_clause '>'
# [099] ratio_type
ratio_type ::= 'ratio' '<' labeled_type_argument (',' labeled_type_argument)* '>'
# [100] hole_type
hole_type ::= '_'
# [101] qualified_type
qualified_type ::= type_head ('.' IDENTIFIER)*
# [102] type_head
type_head ::= IDENTIFIER | 'môđun'
# [103] type_arguments
type_arguments ::= '<' type_argument (',' type_argument)* '>'
# [104] type_argument
type_argument ::= labeled_type_argument | type_annotation | NATURAL | '[' figura_list? ']'
# [105] labeled_type_argument
labeled_type_argument ::= IDENTIFIER ':' type_annotation
# [106] width_type_sugar
width_type_sugar ::= WIDTH_MARKER | LISTA_WIDTH_SUGAR | (TENSOR_WIDTH_SUGAR | SPARSA_WIDTH_SUGAR | VECTOR_WIDTH_SUGAR) shape_suffix? | MATRIX_WIDTH_SUGAR shape_suffix
# [107] shape_suffix
shape_suffix ::= '[' figura_list? ']'
# [108] figura
figura ::= '_' | NATURAL | IDENTIFIER | '[' figura_list? ']'
# [109] figura_list
figura_list ::= figura (',' figura)*
# [110] function_type
function_type ::= '(' type_list? ')' '→' type_annotation alternate_exit_clause?
# [111] type_list
type_list ::= type_annotation (',' type_annotation)*
# [112] si_stmt
si_stmt ::= 'nếu' si_tail
# [113] si_tail
si_tail ::= expression arm ('nếukhôngthì' si_tail | secus_clause)?
# [114] secus_clause
secus_clause ::= 'khác' else_arm
# [115] arm
arm ::= (block_stmt | ergo_joint statement) cape_clause?
# [116] else_arm
else_arm ::= (block_stmt | ergo_joint statement) cape_clause?
# [117] dum_stmt
dum_stmt ::= 'trong_khi' expression (block_stmt | ergo_joint statement) cape_clause?
# [118] itera_stmt
itera_stmt ::= 'lặp' ('từ' expression (',' expression)* | 'ra' expression | 'khoảng' expression (',' expression)*) apud_clause? ('hằng' | 'biến') itera_binding (block_stmt | ergo_joint statement) cape_clause?
# [119] itera_binding
itera_binding ::= array_pattern | object_pattern | IDENTIFIER (',' IDENTIFIER)*
# [120] apud_clause
apud_clause ::= 'tại' '[' IDENTIFIER (',' IDENTIFIER)* ']'
# [121] elige_stmt
elige_stmt ::= 'chọn' expression '{' casu_elige_clause* ceterum_clause? '}' cape_clause?
# [122] casu_elige_clause
casu_elige_clause ::= 'trường_hợp' expression (block_stmt | ergo_joint statement)
# [123] ceterum_clause
ceterum_clause ::= 'mặc_định' (block_stmt | ergo_joint statement)
# [124] discerne_stmt
discerne_stmt ::= 'phân_tích' 'mọi'? discriminants '{' casu_variant_clause* ceterum_clause? '}'
# [125] discriminants
discriminants ::= subject_path ('và' subject_path)*
# [126] subject_path
subject_path ::= IDENTIFIER ('.' IDENTIFIER)*
# [127] casu_variant_clause
casu_variant_clause ::= 'trường_hợp' patterns (block_stmt | ergo_joint statement)
# [128] patterns
patterns ::= pattern ('và' pattern)*
# [129] pattern
pattern ::= pattern_atom ('hoặc' pattern_atom)*
# [130] pattern_atom
pattern_atom ::= '_' | negated_number | literal | type_pattern | (IDENTIFIER ut_pattern?)
# [131] negated_number
negated_number ::= '-' NUMBER
# [132] type_pattern
type_pattern ::= IDENTIFIER type_arguments? ut_pattern?
# [133] ut_pattern
ut_pattern ::= ('như' IDENTIFIER) | (('hằng' | 'biến') pattern_binding (',' pattern_binding)*)
# [134] pattern_binding
pattern_binding ::= IDENTIFIER ('như' IDENTIFIER)?
# [135] custodi_stmt
custodi_stmt ::= 'canh_gác' '{' si_guard_clause+ '}'
# [136] si_guard_clause
si_guard_clause ::= 'nếu' expression (block_stmt | ergo_joint statement)
# [137] ex_stmt
ex_stmt ::= 'từ' expression ('hằng' | 'biến') extract_fields
# [138] extract_fields
extract_fields ::= extract_field (',' extract_field)* (',' ceteri_field)? | ceteri_field
# [139] extract_field
extract_field ::= IDENTIFIER ('như' IDENTIFIER)?
# [140] ceteri_field
ceteri_field ::= 'còn_lại' IDENTIFIER
# [141] redde_stmt
redde_stmt ::= 'trả' expression?
# [142] reddet_stmt
reddet_stmt ::= 'đợi_trả' expression
# [143] tacebit_stmt
tacebit_stmt ::= 'đợi_bỏ' expression
# [144] cede_stmt
cede_stmt ::= 'nhường' expression
# [145] rumpe_stmt
rumpe_stmt ::= 'dừng'
# [146] perge_stmt
perge_stmt ::= 'tiếp'
# [147] tacet_stmt
tacet_stmt ::= 'im_lặng'
# [148] iace_stmt
iace_stmt ::= iace_expr | iace_guarded_expr
# [149] iace_expr
iace_expr ::= ('ném' | 'chết') expression
# [150] iace_guarded_expr
iace_guarded_expr ::= ('ném' | 'chết') expression NO_NEWLINE 'nếu' expression
# [151] cape_clause
cape_clause ::= 'bắt' IDENTIFIER block_stmt
# [152] adfirma_stmt
adfirma_stmt ::= 'khẳng_định' expression ('chết' expression)?
# [153] requirit_stmt
requirit_stmt ::= 'yêu_cầu' expression 'ném' expression
# [154] reice_stmt
reice_stmt ::= 'từ_chối' expression 'ném' expression
# [155] expression
expression ::= assignment
# [156] transfer
transfer ::= ternary ('⇇' ternary)*
# [157] assignment
assignment ::= transfer ('←' assignment | '↤' assignment inline_default?)?
# [158] inc_dec_stmt
inc_dec_stmt ::= place ('↑' | '↓')
# [159] place
place ::= call_expr
# [160] ternary
ternary ::= aut_expr ('✓' expression '✗' aut_expr)?
# [161] aut_expr
aut_expr ::= et_expr (('hoặc') et_expr)*
# [162] et_expr
et_expr ::= equality (('và') equality)*
# [163] equality
equality ::= comparison equality_tail*
# [164] equality_tail
equality_tail ::= ('≡' | '≢' | '≠' | '≅' | '≇' | '≈' | '≉') comparison | ('là' | 'không' 'là') type_annotation
# [165] comparison
comparison ::= format_expr (('≺' | '≻' | '≤' | '≥' | '∈' | '∉') format_expr)*
# [166] format_expr
format_expr ::= bitwise_or_expr ('¶' STRING)?
# [167] bitwise_or_expr
bitwise_or_expr ::= bitwise_xor_expr ('∨' bitwise_xor_expr)*
# [168] bitwise_xor_expr
bitwise_xor_expr ::= bitwise_and_expr ('⊻' bitwise_and_expr)*
# [169] bitwise_and_expr
bitwise_and_expr ::= shift_expr ('∧' shift_expr)*
# [170] shift_expr
shift_expr ::= range_expr (('⇐' | '⇒') range_expr)*
# [171] range_expr
range_expr ::= additive_expr range_tail?
# [172] range_tail
range_tail ::= ('‥' | '…' | 'trước' | 'tới') additive_expr ('qua' additive_expr)?
# [173] additive_expr
additive_expr ::= multiplicative_expr (('+' | '-' | '⤒' | '⤓') multiplicative_expr)*
# [174] multiplicative_expr
multiplicative_expr ::= vel_expr (('*' | '/' | '÷' | '%' | '·' | '×' | '⊗' | '⊙' | '⊘') vel_expr)*
# [175] vel_expr
vel_expr ::= unary_expr ('hoặc_nếu_rỗng' vel_rhs)*
# [176] vel_rhs
vel_rhs ::= unary_expr vel_range_tail?
# [177] vel_range_tail
vel_range_tail ::= ('‥' | '…' | 'trước' | 'tới') unary_expr ('qua' unary_expr)?
# [178] unary_expr
unary_expr ::= ('-' | '¬' | 'không') unary_expr | finge_expr | cast_expr
# [179] gradient_expr
gradient_expr ::= call_expr ('∇' gradient_selection?)?
# [180] gradient_selection
gradient_selection ::= '[' gradient_place (',' gradient_place)* ']'
# [181] gradient_place
gradient_place ::= expression
# [182] cast_expr
cast_expr ::= gradient_expr ('∷' type_annotation | conversio_expr)* inline_default?
# [183] conversio_expr
conversio_expr ::= '↦' (type_annotation | interval_target) via_clause? inline_default?
# [184] interval_target
interval_target ::= range_expr
# [185] via_clause
via_clause ::= 'thông_qua' IDENTIFIER
# [186] inline_default
inline_default ::= '⊥' unary_expr
# [187] call_expr
call_expr ::= primary (call_suffix | member_suffix | transpose_suffix | optional_suffix | non_null_suffix)*
# [188] call_suffix
call_suffix ::= call_type_args? '(' argument_list ')'
# [189] member_suffix
member_suffix ::= '.' IDENTIFIER | '[' expression ']'
# [190] transpose_suffix
transpose_suffix ::= 'ᵀ'
# [191] optional_suffix
optional_suffix ::= '?.' IDENTIFIER | '?[' expression ']' | '?(' argument_list ')'
# [192] non_null_suffix
non_null_suffix ::= '!.' IDENTIFIER | '![' expression ']' | '!(' argument_list ')'
# [193] argument_list
argument_list ::= (argument (',' argument)*)?
# [194] argument
argument ::= template_argument | 'rải'? expression
# [195] template_argument
template_argument ::= 'rải'? IDENTIFIER ':' expression
# [196] literal
literal ::= NUMBER | STRING | ASCII_STRING | BACKTICK_STRING | OCTETI_STRING | 'đúng' | 'sai' | 'không_gì' | '∞' | 'nan'
# [197] primary
primary ::= IDENTIFIER | literal | 'tôi' | array_literal | json_literal | typed_constructor | iuncta_expr | ad_expr | clausura_expr | praefixum_expr | scriptum_expr | lege_expr | first_match_expr | summa_expr | extrema_expr | capta_expr | '(' expression ')'
# [198] ad_expr
ad_expr ::= 'gọi' ASCII_STRING ad_opener?
# [199] ad_opener
ad_opener ::= '(' expression ')'
# [200] array_literal
array_literal ::= '[' argument_list? ']'
# [201] iuncta_expr
iuncta_expr ::= 'bộ' type_arguments '[' argument_list? ']'
# [202] json_literal
json_literal ::= '{' (json_member (',' json_member)*)? '}'
# [203] json_member
json_member ::= STRING ':' json_value
# [204] typed_constructor
typed_constructor ::= type_annotation '{' field_list? '}' construction_source?
# [205] field_list
field_list ::= field_init (',' field_init)*
# [206] field_init
field_init ::= (field_key '=' expression) | IDENTIFIER
# [207] field_key
field_key ::= IDENTIFIER | STRING | '[' expression ']'
# [208] construction_source
construction_source ::= 'từ' call_expr
# [209] json_value
json_value ::= json_object | json_array | json_string | json_number | 'true' | 'false' | 'null'
# [210] json_object
json_object ::= '{' (json_member (',' json_member)*)? '}'
# [211] json_array
json_array ::= '[' (json_value (',' json_value)*)? ']'
# [212] json_string
json_string ::= STRING
# [213] json_number
json_number ::= NUMBER
# [214] finge_expr
finge_expr ::= 'tạo' qualified_ident ('{' field_list? '}')? ('∷' type_annotation)?
# [215] qualified_ident
qualified_ident ::= IDENTIFIER ('.' IDENTIFIER)*
# [216] praefixum_expr
praefixum_expr ::= 'tiền_tố' block_stmt
# [217] scriptum_expr
scriptum_expr ::= 'văn_bản_hóa' '(' STRING (',' expression)* ')'
# [218] lege_expr
lege_expr ::= 'đọc' 'dòng'?
# [219] first_match_expr
first_match_expr ::= 'khớp_đầu_tiên' '(' expression apud_clause? ',' 'nơi' IDENTIFIER block_stmt ')'
# [220] summa_expr
summa_expr ::= 'tổng' 'từ' expression apud_clause? filum_clause? ('hằng' | 'biến') IDENTIFIER block_stmt
# [221] filum_clause
filum_clause ::= 'sợi' IDENTIFIER
# [222] extrema_expr
extrema_expr ::= ('lớn_nhất' | 'nhỏ_nhất') 'từ' expression apud_clause? extrema_identity?
# [223] extrema_identity
extrema_identity ::= 'hoặc_nếu_rỗng' expression
# [224] capta_expr
capta_expr ::= 'bẫy' block_stmt
# [225] object_pattern
object_pattern ::= '{' pattern_property (',' pattern_property)* '}'
# [226] pattern_property
pattern_property ::= 'còn_lại'? IDENTIFIER ('như' IDENTIFIER)?
# [227] array_pattern
array_pattern ::= '[' array_pattern_element (',' array_pattern_element)* ']'
# [228] array_pattern_element
array_pattern_element ::= '_' | 'còn_lại'? IDENTIFIER
# [229] nota_stmt
nota_stmt ::= ('ghi_chú' | 'xem' | 'cảnh_báo' | 'viết') expression (',' expression)*
# [230] entry_header
entry_header ::= ('đối_số' IDENTIFIER)? ('thoát' expression)?
# [231] incipit_stmt
incipit_stmt ::= 'bắt_đầu' entry_header block_stmt
# [232] incipiet_stmt
incipiet_stmt ::= 'bắt_đầu_bất_đồng_bộ' entry_header block_stmt
# [233] probandum_decl
probandum_decl ::= 'đối_tượng_kiểm_thử' STRING proba_modifier* '{' probandum_body '}'
# [234] probandum_body
probandum_body ::= (praepara_block | probandum_decl | proba_stmt)*
# [235] proba_stmt
proba_stmt ::= 'kiểm_thử' STRING proba_modifier* block_stmt
# [236] proba_modifier
proba_modifier ::= 'mong_đợi_thất_bại' | 'bỏ_qua' STRING | 'việc_cần_làm' STRING | 'chỉ' | 'nhãn' STRING | 'thời_gian' NATURAL | 'đo_lường' | 'lặp_lại' NATURAL | 'mong_manh' NATURAL | 'chỉ_trong' STRING
# [237] praepara_block
praepara_block ::= ('chuẩn_bị' | 'sẽ_chuẩn_bị' | 'sau_chuẩn_bị' | 'sẽ_sau_chuẩn_bị') 'mọi'? block_stmt
# [238] fac_stmt
fac_stmt ::= 'làm' block_stmt cape_clause? ('trong_khi' expression)?
# [239] IDENTIFIER
IDENTIFIER ::=
# [240] NUMBER
NUMBER ::=
# [241] NATURAL
NATURAL ::=
# [242] STRING
STRING ::=
# [243] ASCII_STRING
ASCII_STRING ::=
# [244] BACKTICK_STRING
BACKTICK_STRING ::=
# [245] OCTETI_STRING
OCTETI_STRING ::=
# [246] NEWLINE
NEWLINE ::=
# [247] WIDTH_MARKER
WIDTH_MARKER ::=
# [248] LISTA_WIDTH_SUGAR
LISTA_WIDTH_SUGAR ::=
# [249] TENSOR_WIDTH_SUGAR
TENSOR_WIDTH_SUGAR ::=
# [250] SPARSA_WIDTH_SUGAR
SPARSA_WIDTH_SUGAR ::=
# [251] VECTOR_WIDTH_SUGAR
VECTOR_WIDTH_SUGAR ::=
# [252] MATRIX_WIDTH_SUGAR
MATRIX_WIDTH_SUGAR ::=
# [253] FRONTMATTER_DELIMITER
FRONTMATTER_DELIMITER ::=
# [254] TOML_LINES
TOML_LINES ::=
# [255] ANNOTATION_NAME
ANNOTATION_NAME ::=
# [256] ANNOTATION_FIELD_NAME
ANNOTATION_FIELD_NAME ::=
# [257] NON_NEWLINE_TOKEN
NON_NEWLINE_TOKEN ::=
# [258] NO_NEWLINE
NO_NEWLINE ::=

Production Index#

Lexicon Appendix#

The lexical tier is descriptive and remains owned by the live lexer and driver. capture-pending rows intentionally carry no invented token shape.

Keyword Reference#

This table is derived from the quoted Latin literals in the source productions. It is not a second keyword authority.

Comma Separator Table#

Optional commas are forbidden. The source currently has no ','? positions; every comma-bearing production is either required or absent.

Normative Language Notes#

Formal grammar for the Faber programming language. This file is the canonical grammar and spec-commentary surface for the public language; the compiler (Radix) implements it. The rendered, localized grammar is published on the documentation site.

Documentation contract: runnable language reference programs live in the public frontmatter (term, syntax, related, …); the generated manifest is explain` loads the exempla reference pack from disk. Prefer the language corpus + EBNF for new reference work.

---

Program Structure#

Faber source files are raw text peeled by the driver before lexing. Optional TOML frontmatter is not part of the token grammar. Within Faber syntax, spaces, tabs, and newlines are trivia unless a production explicitly names NEWLINE. Canonical forms are safe to compress onto one line. Any line-sensitive syntax is explicitly sugar; a compressor must expand it when a lossless canonical mapping exists, and otherwise preserve its boundary or reject compression. Line comments remain line-oriented trivia and must be removed or relocated safely by a compressor.

Uppercase names are lexical terminals. FRONTMATTER_DELIMITER is a line whose trimmed content is exactly +++; TOML_LINES is the possibly empty sequence of complete TOML lines before the closing delimiter. NON_NEWLINE_TOKEN means one ordinary source token other than a newline. ANNOTATION_NAME and ANNOTATION_FIELD_NAME are identifier spellings in annotation-owned contexts; they include spellings that are keywords in other contexts. NO_NEWLINE is a zero-width constraint requiring adjacent grammar parts to remain on the same logical line.

File frontmatter (+++)#

When present, frontmatter must open on line 1 with exactly +++. A later line that trims to exactly +++ ends the block. Bytes after the closing delimiter are the Faber program. An empty body (whitespace only) is a valid empty program.

Frontmatter is parsed as a generic TOML document in the compiler driver — not parsed as Faber statements. Authors may attach arbitrary metadata keys; tooling reads known keys such as group, sectio, and [probanda] via accessors. faber package tooling consumes those package keys. Package authority for [package], [paths], and [build] remains faber.toml; conflicting frontmatter values are rejected in package mode.

Example:

+++
group = "exempla.directiva"
sectio = "smoke"
+++

incipit {}

Line-start § file directives were removed. Put file metadata in +++ frontmatter instead. Inside quoted strings, § remains the string-template hole (see Call and Member Access below).

Comma separator law#

Every comma position is either required or forbidden. Optional commas do not exist.

Item lists — homogeneous entries inside a bounded header (lista literals, call arguments, parameters, type argument lists, figura lists, field-init lists, liệt_kê members, hợp_nhất variant lists, JSON members and array elements, annotation / import / nucleum fields, output statement lists) — require a comma between adjacent items and forbid one after the last.

Declaration blocks — self-annotating declarations (statements, kiểu members, giao_ước methods, hợp_nhất payload fields) — contain no commas. Entries are trivia-delimited.

---

Declarations#

Declarations are top-level. A hàm and the type declarations (kiểu, giao_ước, kiểu_tên, liệt_kê, hợp_nhất, lược_đồ) may not appear inside a block; the parser rejects them there (declaration_not_top_level). Methods live in kiểu bodies. For a local function, bind a closure; for recursion, use a top-level function.

Variables#

• hằng = immutable binding (write-once): it may be declared without an initializer and assigned exactly once later, then frozen. biến = mutable binding (reassignable), like let.
• đợi_hằng / đợi_biến await a promissum<T> or promissum<T ⇥ E>, bind the resolved T, and propagate a compatible alternate E.
• ↢ is the await-directed initializer for an ordinary declaration: hằng T name ↢ future, biến T name ↢ future, or đặt name ↢ future. It has the same await and alternate-propagation semantics as đợi_hằng T name ← future, but it is not a general expression operator and cannot target an existing place.
• Use _ as the type annotation when the initializer determines the type: hằng _ name ← value
• đặt name ← value is sugar for hằng _ name ← value (inferred immutable local)
• đặt name (no initializer) is sugar for hằng _ name — the inferred deferred immutable. Assign exactly once before any read.
• Typed hằng/biến initializers accept ↤ (hằng numerus x ↤ "42"): the written type is the conversion destination, then the binding is initialized. đợi_hằng/đợi_biến keep ←; hằng _, đặt, and untyped destructuring reject ↤ (no concrete destination type).
• hằng T x = e (D5.10) declares a typed constant; at the top of a file the same declaration is the module-level constant (next section). = states a compile-time fact, so e is evaluated while compiling (literals, arithmetic and the other operators on scalars, module constants, earlier constants) and must fit T whatever T's overflow policy: hằng u8 d = 300 is a compile error even for saturating<u8>. hằng _ x = 10 infers int. The result is an ordinary immutable local of type T. biến never takes = (varia_compile_time_initializer), and a value that is not known at compile time is stored with ← (constant_initializer_not_constant, SEM060).
• Deferred init: hằng numerus x or đặt x declares an uninitialized immutable slot that must be assigned exactly once before any read; a second assignment is rejected. The definite-assignment pass (semantic Phase 3a) enforces this.

Module-level constants#

A module declares values only as compile-time constants: hằng T X = e at the top of a file (en const T X = e), for example hằng numerus LIMES = 4096 (D5.8, st1 R1). It is the same declaration as the block-level constant above, with = stating a compile-time fact, and it is the only top-level value declaration. Module-level mutable state does not exist (D5.7): a top-level biến, đặt, destructuring, or a runtime initializer (←, ↤, ↢) is a compile error, SEM062 top_level_binding — a runtime value belongs in a function. biến T X = e stays varia_compile_time_initializer, and a top-level declaration with no initializer is SEM008 top_level_initializer. hằng _ X = 10 infers int as it does for a local.

Retired spelling. The module-level static tĩnh T X = e (en static T X = e) no longer exists. A statement-initial tĩnh followed by an identifier or (, at the top level or in a block, parses as the old declaration whole and is reported as PARSE010 static_decl_retired (args keyword, the spelling written, and name; the help names the hằng spelling); there is no alias period, and the diagnostic stays. tĩnh followed by anything else is an ordinary identifier. tĩnh survives only as the kiểu field modifier (see Classes).

Constants are immutable and initialized with `=` only (D5.9), never ←. The initializer must be evaluable at compile time: literals; arithmetic, comparison, bit, and logical operators on numerus, fractus, and bivalens scalars, plus textus concatenation; references to other constants (evaluated in dependency order, so a constant may be used before its declaration — a cycle is constant_cycle, SEM007); and collection literals (lista, tuples, map construction) whose elements are constants (only their scalar leaves fold). Anything else is constant_initializer_not_constant (SEM060). Decimal widths and môđun<W>/saturatus<W> values are not folded, so arithmetic on them is not a compile-time constant today. Compile-time integer arithmetic is checked (overflow and division by zero are compile errors: constant_arithmetic_overflow, constant_division_by_zero), matching the runner's checked runtime semantics. A value that needs computation takes a tiền_tố { … } block (en comptime { … }), which runs during the build; it is legal as the whole initializer of an = constant, at module level or at block level (inside any function, method, closure or entry body), and as a kiểu field default under any modifier. Anywhere else it is SEM064 praefixum_outside_constant. The body stands alone: it may read module constants but not a parameter or local of the enclosing body (praefixum_captures_local), and inside a generic function, method or genus it may not mention a type parameter (praefixum_type_parameter). A block-level body is evaluated like a module constant; an inner tiền_tố constant runs before the one that contains it, and a cycle through a site is constant_cycle.

Build-time file embed, `nhúng` (en `embed`, D8.10). An = constant at module level or block level, or a kiểu field default under any modifier (tĩnh, hằng, biến), may take nhúng "path" as its initializer instead of an ordinary expression: hằng textus LICENSE = nhúng "LICENSE.txt". nhúng is contextual (the parser claims it in expression position when directly followed by a string literal; any other use of the spelling is an ordinary identifier). Lowering admits it only as the whole initializer of such a constant or field default; anywhere else (x ← nhúng "p", a call argument, a trả value) it is SEM061 insere_outside_constant. The path is package-relative, resolved against the nearest ancestor faber.toml (or the source file's own directory when none exists); an absolute path or a .. escape is rejected, and a missing file is a compile error. The file is read once, at build time — it is a build input, like the source itself. The declared type decides how the bytes land: textus requires valid UTF-8 and fails to build otherwise; octeti reads the raw bytes unconditionally. The result type follows the slot: a _ slot, or no slot, is SEM061 insere_type_required, and any other concrete slot type is insere_type_invalid.

Functions#

• Generic parameter lists put type parameters first and kích_thước (en size) parameters after them (<T, U, kích_thước N>); a type parameter after a size parameter is type_param_after_magnitudo. Once one parameter has a default (= numerus, kích_thước N = 3), every later parameter needs one (generic_default_not_trailing).
• The thoát function modifier takes an identifier or a non-negative integer literal; the entry-point thoát (below) takes an expression.

Capture-free closures#

tự_do is the canonical Latin spelling of the closure_modifier; the English reader spelling is free. The modifier follows the parameter list in both compact and legacy đóng forms, before any → return or ⇥ alternate-exit clause. It declares a checked capture-free contract: the closure may use its own parameters, body locals, and module-level items, but it must not reference a local or parameter from an enclosing function. Such a capture is rejected by the compiler.

sit summa ← (numerus a, numerus b) libera ∴ a + b
clausura numerus x libera: x * 2

hạt_nhân is the second spelling of the closure_modifier; the English reader spelling is kernel. The alternative is locale-sealed and singular: at most one modifier may occupy the slot, each reader pack admits only its declared spelling, and stacked spellings such as free kernel are rejected as a duplicate modifier. A kernel closure requires everything free requires — no reference to an enclosing function's local or parameter, while its own parameters, body locals, and module-level items stay legal — plus the device-safe subset used by kernel functions: typed tensors and scalars, glyphs, structured control, and calls to other device functions. Host allocation, I/O, bags, dynamic calls, ⇥ clauses, ném throws, and bắt recovery are rejected in the kernel contract; trả returns only the closure's own → result. Declaration annotations @ hạt_nhân (@ kernel in the English reader) are unchanged: they remain the role marker for named functions, and the closure modifier is their expression-form twin.

The body joint keeps the existing closure law: ∴ followed by one expression, or ∴ làm { ... } (do in the English reader); bare { ... } is not a closure body. A kernel closure is usable only as a local immutable binding in its enclosing function and only called there, or invoked immediately in the same expression; it is not a first-class value and cannot escape into a field, list element, return value, or ordinary-function argument. The compiler lowers it to a private synthetic kernel with a stable identity: one launch when its host caller invokes it, direct composition with no surviving device-to-device runtime call when a kernel caller invokes it, and never a public launch entry or ABI row. The modifier does not request fusion; two local kernel closures remain two launches unless a later cross-launch pass fuses them.

fixum _ duplica ← (tensor<f32, [8]> x) nucleum ∴ x + x
fixum _ dup ← duplica(xs)

• Return syntax: → declares the normal success type. A bodyful function with no → is effect-only (vacuum) and must not contain trả. A statement-bodied closure (làm { ... } or legacy block body) must also spell → T before it can use trả; expression-bodied closures may infer their result from the expression.
• Recoverable alternate-exit syntax: ⇥ declares the error-channel type. It can appear after → T or alone on an effect-only failable function or closure. A closure body that uses an escaping ném must declare its own ⇥ E; it cannot inherit the enclosing function's error channel. A local làm { ... } bắt err { ... } may catch ném without an enclosing ⇥. A failable function call (→ T ⇥ E) inside a ⇥-declaring function propagates to the function's alternate exit without a làm/bắt wrapper, mirroring how bare ↦ conversio and ném throws already behave; the call lowers to Rust ?. A closure must still declare its own ⇥ to propagate a failable call — the enclosing function's error channel does not cross the closure boundary.
• In a signature, ⇥ only ever names an error type (→ T ⇥ E). It never carries a value.
• Parameter access markers live in the type position: ra/ref (read), vào/mut (mutate), sở_hữu (consume), and sao_chép (duplicate then own). The retired parameter-prefix slot is not part of the grammar; từ/from remains the import/iteration/extraction token identity.
• Post-name marker: tự_nguyện (voluntary/optional provision)
• còn_lại marks rest parameter
• Ordinary hàm declarations and genus methods require bodies. Signature-only methods belong in giao_ước.
• lỗi NAME is a legacy runtime-injected ignotum local, and ném_lỗi is a legacy marker with no current semantic effect. Neither declares the typed alternate-exit contract. New failable APIs should use ⇥ E; whether either legacy modifier should survive is unresolved.
• do_đó is the compact statement-body joint only (one-statement nếu/trong_khi/trường_hợp/… arms).
• ∴ is the compact clausura joint only. The two are not aliases.
• Compact closure block bodies must use làm { ... }; a closure-local làm body may attach bắt, but cannot use postfix trong_khi.

Classes#

A kiểu is a struct with methods. It holds data, its methods act on that data, and it satisfies contracts through thực_thi. It is not a self-contained object that owns its own construction and process: a value is built with a construction literal (Genus { field = value }).

• No class inheritance. Inheritance was removed: there is no sub (extends) clause and no abstractus genus. Shared behaviour comes from contracts (giao_ước + thực_thi) and from composition — a field holding another value. The old spellings are rejected with a migration diagnostic.

• No static methods. A kiểu declares instance methods only. A function about a type is a top-level function in the type's file, reached through the import alias. tĩnh marks a type-level field, never a method.
• A newtype is a one-field `kiểu`. There is no separate newtype declaration. Units that need arithmetic wait on operator overloading.
• No macros and no user derive. What you read is what runs. Code generation, when a project needs it, is an external step before the build.
• No extension methods and no retroactive conformance, for now. A type's methods and its thực_thi contracts are declared on the type itself. Code elsewhere cannot add either. Allowing it would need coherence rules, and is revisited together with the contract features that are deferred.
• Contract bounds on type parameters (D1.1-D1.3). hàm maior<T thực_thi Orderable<T>>(T a, T b) → T bounds a callable's type parameter to witnesses that declare that contract. Several bounds on one parameter join with ∩ only (<T thực_thi Orderable<T> ∩ Equatable<T>> — never a comma there; a comma starts the next parameter). The bound is checked, and its methods become callable inside the bounded body, only on a hàm/method type parameter (generic_bound); the same clause parses on a kiểu/kiểu_tên/hợp_nhất/ giao_ước type parameter but is rejected there (implet_bound_on_type_declaration) — those declarations state contracts through the genus's own thực_thi clause instead (below). Every generic contract is written with its type arguments in full — Orderable<Persona>, Orderable<T> — never a bare name (implet_contract_arity on a mismatched count). Satisfaction stays nominal (D1.3): a witness must declare the bound itself.

• Copy with changes (D15.1-D15.3, D6). Genus { field = value, … } từ source builds a new value: the braced fields override, and every other field copies shallowly from source (a collection field is shared with the source, not deep-cloned; private fields copy across too). từ must start on the closing }'s line — a line-leading từ is instead the extraction statement (từ p hằng x, y). Exactly one source is legal (construction_source_repeated on a second same-line từ); the source must be the same genus type as the constructor. rải was removed from construction literals (D15.4); it stays for lists and calls.

Annotations#

@ hạt_nhân mảnh is a modifier on the hạt_nhân annotation (sugar or braced mảnh = đúng / sai), not a fused annotation name and not the graphics @ mảnh stage. Standalone @ mảnh is unchanged.

The làn clause of the hạt_nhân annotation (@ hạt_nhân làn "x", braced @ hạt_nhân { làn = "x" }) was removed (K7): the compiler rejects it with nucleum_lane_removed, and mảnh is the only modifier or field. @ radix làn is a different annotation and is unaffected.

Braced annotation records (@ futura { }, @ optio { binding = verbose, ... }) are canonical and compression-safe. Unbraced annotations are line-sensitive, non-compression-safe sugar that consumes through NEWLINE; the newline is part of this sugar grammar, not a general Faber statement separator. A compressor may rewrite promoted families only when their named-field mapping is known. It must otherwise preserve the line break or reject compression. Promoted sugar and braced forms lower to the same HirAnnotation records. Unpromoted positional families preserve raw arguments and do not yet have a lossless braced expansion.

The current Radix parser still accepts only a fixed token subset in unbraced payloads and ends them with declaration-boundary heuristics rather than NEWLINE. Those are implementation mismatches with this specification, not alternate language rules.

Annotation contracts: @ annotatio (optionally @ annotatio { target = hàm }) marks a top-level kiểu as a compile-time annotation contract. Ordinary genera are not annotation schemas. Applications use @ ContractName { field = constant } and resolve through local declarations or imported file-interface exports. Resolved applications lower to HirAnnotation with contract_id: Some(DefId) and constant field values. v1 attachment target is hàm only; payload scalars are textus, numerus, fractus, and bivalens (optional via tự_nguyện or T ∪ nihil). Web, HTTP, controller, and framework route families are not compiler-owned; they are built as libraries, from annotation contracts or on top of @ gọi. The one exception is @ gọi itself: it is the compiler-owned serving half of gọi (see Capability Calls).

User annotations are metadata. Their consumers are tools, such as product packaging. They never change compilation, and Faber code never reads them at run time. An annotation that changes compilation is compiler-owned (@ json, @ gọi, @ radix).

JSON genera: @ json on a kiểu is a compiler-owned data-model contract, not a generic annotation schema. Fields must be JSON-safe (textus, ascii, numerus, fractus, bivalens, instans, nihil, lista<T>, tabula<textus, T>, nullable T ∪ nihil, or another @ json kiểu). Field metadata @ json { tên = "wire_name" } changes the emitted object key used by value ↦ valor, value ↦ json, and json ↦ Genus; JSON text remains a Norma wire operation such as json.pange(value ↦ json).

• @ radix is compiler-reserved: every form under it is compiler-owned metadata, not an application surface, and may change with the compiler. The historical morphology-stem meaning is retired; morphology remains a source naming discipline, not compiler-generated conjugation. The family (radix_annotation plus the braced records) is:
• @ radix làn "air" / "mir" / "hir-direct" (braced @ radix { làn = "air" }) on top-level functions for explicit compiler-lane routing; unsupported lane/target combinations reject with diagnostics instead of being ignored.
• @ radix backward "name" on an air-lane function names the generated reverse-mode gradient companion; it is valid only paired with làn "air".
• @ radix kiểu_tên T vào A B … (braced @ radix { param = T, allowed = A, … }) restricts the type parameter T of the annotated declaration to the listed domain. Any other directive after @ radix is rejected (unknown_directive).
• @ verte defines codegen transformation (method name or template)
• @ nondum [TARGET] ["REASON"] marks a declaration as present in an interface but unavailable for the target
• @ cli "NAME" marks an bắt_đầu entry as a CLI program
• @ imperium "NAME" marks a function as a CLI command entry point
• @ optio NAME ... defines a CLI option; use kiểu_tên bivalens for boolean flags
• @ operandus [còn_lại] TYPE NAME ... defines a CLI positional argument
• @ futura marks a function as async (legacy — prefer async posture word)
• @ cursor marks a function as generator (legacy — prefer sinh posture word)
• Callable posture words (async/sinh/async_sinh) are recognized in the signature slot after modifiers and before →/⇥/body; bare means synchronous finite (sinh T is a synchronous generator: a call to it has type cursor<T>, not lista<T>; collect with gen() ↦ lista<T>)
• @ công_khai marks a declaration for the file's importable (export) surface; @ interna marks it package-internal (same-package importable only); @ privata is an explicit module-private marker. Unmarked top-level declarations are module-private by default; a declaration mixing distinct visibility tiers is rejected with SEM019 (conflicting_visibility)
• @ protecta is reserved and rejected with a semantic diagnostic; it has no package, subclass, or sibling-file visibility meaning
• @ doc is not an annotation. Comments are the documentation: a line comment attaches forward to the declaration it precedes, and there is no doc marker.

• thực_thi = implements (conformance to an giao_ước contract), written with the contract's type arguments in full (kiểu Persona thực_thi Orderable<Persona>, D1.2).
• Every kiểu field declares exactly one of hằng / biến / tĩnh (D16.1); there is no default — an unmarked field is a parse error: PARSE010 field_modifier_missing (D5c). The hợp_nhất shared-field position (union_member) keeps today's unmarked form (fork F7 held). hằng T x: per instance, set only in a construction literal (Genus { field = value }), never reassigned; Genus { … } từ p copies it unchanged (D16.3), independent of visibility (@ privata + hằng is legal). biến T x: per instance, reassignable. tĩnh T X = …: one per type, compile-time (the only remaining tĩnh position). A write to a hằng field outside a construction literal is SEM020 (assignment_to_fixum_field). The former nexum field modifier is removed and rejected with a migration diagnostic.
• kiểu members are public by default (D5.2). @ privata on a member restricts it to the type's own methods: only code inside the type's own function bodies may read, write, or call it (D5.3); @ interna restricts it to code in the declaring package. A construction literal may still set a private field, from any file, and Genus { … } từ p copies it unchanged (D5.4). Reading, writing, or calling an inaccessible member from outside its allowed scope is SEM063 (member_private_read/_write/_call, or member_interna_read/_write/_call); @ công_khai on a member is a redundant-annotation warning WARN028 (redundant_member_publica), an error when warnings are denied.
• A type may refer to itself: hợp_nhất Expr { Adde { Expr sinister, Expr dexter } } and kiểu Nodus { Nodus ∪ nihil next } need no keyword and no box type. Values have reference semantics, so the indirection is implied; a backend that stores fields inline inserts it on the fields that close a type cycle.

Interfaces#

giao_ước is the contract construct: signature-only methods for thực_thi (gerundive of implere — that which must be fulfilled). Import namespaces are .fab file boundaries; exported declarations live at file top level.

A contract has no default method bodies. Default bodies would make a contract an abstract base class without fields. Behaviour shared by every implementer is a top-level function that takes the contract type. Contract inheritance (a contract that requires another), associated types, and retroactive conformance are deferred.

The one ordering contract, `Orderable<T>` (D1.4). Norma declares it (norma:order) as an ordinary giao_ước with one method, compare(T other) → numerus: negative, zero, or positive when self sorts before, with, or after other. A kiểu opts in by naming itself (thực_thi Orderable<Persona>, D1.1-D1.3); satisfaction stays nominal. The compiler recognizes the contract by a mark on its declaration, never by its name: @ radix contract "ordering" (C2). That mark is what lets the contract drive language-level behaviour a plain giao_ước cannot: `≺ ≻ ≤ ≥` on a conforming type call its one `compare`, so the glyphs and compare can never disagree; `numerus`, `fractus`, `textus`, and `instans` conform without any code (integers by value, floats by IEEE 754 totalOrder so NaN sorts above every number — the bare comparison glyphs on fractus stay IEEE, where NaN compares sai; text by Unicode code point; instants by time); and tuples order lexicographically when every element conforms. There is no contract tower and no default method (D1.10): a bound generic uses the contract the same way, hàm maior<T thực_thi Orderable<T>>(T a, T b) → T. @ radix stays reserved for compiler-owned metadata; an application must not write it, and today "ordering" is the only recognized role.

Type Aliases#

Enums#

liệt_kê (an enum) and hợp_nhất (a tagged union) are data only (D9.1): a hàm member inside either body is a parse error (sum_type_function, recovered so parsing resumes at the next member), and an thực_thi clause on either header is a parse error (sum_type_implements) before the body is even read. Shared behavior over an liệt_kê/hợp_nhất value is an ordinary top-level function that takes the type, the same posture giao_ước already uses for contract default bodies.

An liệt_kê converts without user code (D9.4). A member's discriminant is the authored number, or the previous member's number plus one; the first member defaults to 0. A string-valued member has no discriminant.

• Ordo ↦ numerus — the member's discriminant; infallible.
• numerus ↦ Ordo — the first member whose discriminant equals the value; failable when none matches (⊥ default, or textus propagation).
• Ordo ↦ textus — the member's name; infallible.

Other conversion pairs involving an liệt_kê fall through to the ordinary unsupported_conversio rejection.

A registered @ conversio (A, B) also serves a ↦ B for a program's own error types (see Annotations): a direct (source, destination) pair only, never auto-composed into a chain, and a missing row fails closed.

Tagged Unions#

Shared fields come first, before every variant. The first shared field must open with an annotation — @ commune (en @ shared) in practice — and the fields after it join the same region with or without one; a bare T name before any annotation reads as a variant. A variant may not redeclare a shared field (union_variant_redeclares_shared_field).

Variant lists are an item list: comma required between variants, forbidden after the last. Payload fields inside a variant are a declaration block (genus-style, no commas).

Union overlap access (D9.2): a call, read, or write on a field/method name through a union (hợp_nhất or ∪) value type-checks when every constituent exposes it with the same declared type, then dispatches per the value's actual member at runtime — access is not restricted to a common supertype shape. A constituent that lacks the name is union_member_not_common; when every constituent has it but the declared types disagree, it is union_member_differs (each constituent's type is named in the diagnostic).

Relational Schemas (experimental)#

Experimental — owned by the census-types goal; the surface may change. lược_đồ Name { cột T name … } declares an application-owned relational heading for database results. It names only the columns the application reads; extra source columns stay invisible. Each cột row takes a type (use T ∪ nihil for a nullable column) and a name, with an optional : sourceName alias mapping the public column to a source column (absent means identity). Column rows are a declaration block (no commas), and each row starts on its own line (a second cột on the same line is schema_nested_column). A schema has no methods (schema_method), no thực_thi (schema_inheritance), and no nested columns (schema_nested_column); each is rejected at parse time.

Identifier Naming#

Faber has no globally reserved words. Keyword ownership is contextual per spelling: a keyword claims only its owning grammar slot. Every user-chosen name slot accepts every keyword spelling — declaration names, parameters, members, binding targets (hằng/biến/đặt patterns and captures), import aliases, and loop/iteration bindings. Type-name slots stay out.

Outside a spelling's owning contexts, that spelling may be an IDENTIFIER. An owning context may itself be effectively global when its production applies everywhere a statement or expression may begin. Builtin claims (đọc/dòng/văn_bản_hóa/vacua, and the scribe family in statement-initial position) are defaults, not reservations: a user binding of the same surface spelling wins.

Radix still emits globally reserved tokens for some spellings and selectively reinterprets them as identifiers. That is transitional implementation behavior; it does not replace the contextual language rule above.

Mixed-case lower-initial names are syntactically accepted but not Faber-preferred for language, stdlib, host routes, or compiler-owned intrinsic APIs. Prefer one word. If one word cannot carry the meaning, use snake_case only in rare cases. If neither shape works, the method probably does not belong in the core surface unless it is critical. Stdlib encode/decode uses the mechanical verb trio pange / solve / tempta across modules — see docs/stdlib/stdlib-mechanical-verbs.md. The public text library is norma:chorda — see docs/stdlib/chorda-methods.md.

Modules (vùng)#

vùng NAME (en module NAME, D7.7) optionally names the file. It is legal only as the file's very first declaration, before any import or other statement, and at most once (a second vùng is module_declaration_duplicate; one that is not first is module_declaration_misplaced). The spelling is contextual: vùng is claimed only in that leading, statement-initial position immediately followed by an identifier, so it stays an ordinary identifier everywhere else (a field, a local, a parameter named vùng).

The declared name does two jobs. It is the file's default import name: nhập từ "library:geo" binds geometria when that file declares vùng geometria, instead of the last path segment. Two imports that would default to the same name are a compile error; alias one with như. There is no warning when the declared name differs from the file's own name — the name is never visible on the import line — but an explicit alias (nhập từ "library:geo" geo) is always available.

It is also the module doc anchor (D7.3, D7.6): the comment block directly above vùng (with no blank line between) is the file's module documentation, replacing the older "first block in the file" rule. A file without vùng keeps today's behaviour on both counts: the default import name is the last path segment, and the leading comment block attaches forward to whatever follows it.

Imports#

Example:

importa ex "hono" Hono
importa ex "hono" Context
# No marker: no re-export.
importa ex "norma:chorda"
importa { ex = "norma:json/solve", ut = solve_mod }
importa ex "norma:consolum" consolum
# Kernel manifest glob.
importa ex "faber:*" faber
importa ex "lodash" * ut _
# Re-export.
importa ex "./types" publica User
# Selective imports (values and types).
importa ex "norma:consolum" fixum dic ut output

A record import needs its từ = "…" source (missing_import_source), and mọi cannot be combined with tên or như (mixed_wildcard_and_named_import).

The privata import marker was removed (VM-U3); an import without a marker does not re-export, and công_khai is the re-export marker. Missing named binding defaults to the last import path segment when it is a valid, non-conflicting identifier. If the inferred name is invalid or collides with an existing top-level binding, spell an explicit tên or như binding.

Selective imports create ordinary immutable local bindings: nhập từ "norma:consolum" hằng dic như output, funde như output_bytes imports one exported member per hằng local. The pre-như identifier names an exported member in the imported file; the post-như identifier is the caller-owned local binding; the imported file interface supplies the complete type. A member may be a value (a function or constant) or a type declaration; the syntax is the same for both. The bindings obey ordinary local-binding rules (duplicates, shadowing, lints), are locale-resolved through the imported module, and are never re-exports. Wildcard members cannot mix into the list. The current parser tolerates one trailing comma after the final member; the canonical spine keeps every comma required.

nhập từ "faber:*" faber is kernel-specific sugar: the glob lives inside the import path string and expands the released binary's kernel manifest into faber.<module>.<verb> calls. It is not a wildcard re-export and does not create a runtime aggregate value.

---

Types#

• Declaration parameters (genericParams) and applied arguments (typeArguments) are distinct grammar categories. Applied arguments admit nested types and static figura values. typeArguments still admits NATURAL.
• Applied NATURAL arguments are kích_thước capacity facts, not width markers. Shipped bounded forms use that slot: lista<T, N>, queue<T, N>, stack<T, N>, textus<N>, ascii<N>, octeti<N>. Width markers such as i32 and f32 stay the separate widthTypeSugar production below.
• Convert hints are not type arguments (D11.9). A hint (Hex / Bin / Oct / Be / Le / Bits / Code) is a thông_qua clause on the ↦ conversion, never a further argument of the target type (see Runtime conversion). The retired spellings are parse errors with a pointer at the clause: a hint as a further type argument of a scalar head (ascii<N, Hex>, littera<Code>; the wrapped numeric heads numerus<W, Hex> and fractus<f64, Bits> are rejected whole as numeric_wrapper_retired, see Sized primitives) is conversio_hint_type_argument, and a bracketed hint tail after the target (octeti<16><Le>, vector<u32, 4><Be>) is conversio_hint_tail_argument. Only scalar heads are checked, so a user type named like a hint stays a legal argument of a collection target (↦ lista<Code>).
• Type arguments admit the hole forms: lista<∪> infers a heterogeneous element union and tabula<K, ∪> a heterogeneous value union; lista<_> keeps the monomorphic single-inhabitant hole.
• Explicit generic call-site lists use the same typeArguments production: id<_>(x) is a type hole (equivalent to omitted id(x) for a one-param callee), and mixed lists such as both<_, textus>(a, b) are legal. Arity stays exact (both<_> is still one argument). ∪ in that list is rejected (explicit_union_type_arg_unsupported): a callee type param is a monomorphic witness slot.
• labeledTypeArgument is the optional label prefix on bộ type arguments only (bộ<gx: f32, T>; mixed labeled/unlabeled legal). A label in a non-bộ list (f<gx: T>(x), lista<gx: T>) is a parse error. Absence is the only unlabeled form; there is no _: T spelling. Keyword spellings are legal labels under the contextual law (bộ<hằng: A>).
• Labels are unique within one tuple type.
• The tuple type is spelled bộ<…>, not (K1, K2). Parentheses already mean grouping, function types, parameters, and calls. Every other compound type is name<args>, and tuple labels come from the same type-argument machinery.
• Labels are erased from type identity: bộ<gx: A, B> ≡ bộ<A, B> for assignment, ≡/↦, unify, and every emitter.
• Bracket index on a tuple requires a literal integer (i[0]); every element is reachable by position, labeled or not. Non-literal index expressions stay rejected. Positions are brackets only — no .0.
• Member-by-label (i.gx) requires that label to be present on the receiver's bộ annotation.
• bộ element slots admit _ (monomorphic hole, solved element-wise from the single position witness) and reject ∪. A wanted union element is declared with binary cup (bộ<f32, textus ∪ nihil>). lista<∪> / tabula<K, ∪> keep heterogeneous-union behavior. Labels compose with holes (bộ<loss: _, T>).
• ratio type arguments require a label for every element, labels are unique, _ is admitted as a monomorphic element hole, and ∪ is rejected in an element slot. A ratio has no positional or bracket access, and it has no structural equivalence with another ratio or a genus; fields are accessed by label only.
• Arrays are written lista<T> (unbounded, shipped). Postfix T[] is not accepted. lista<T, N> is the shipped bounded form; see Generic Collections.
• ra/vào/sở_hữu/sao_chép mark ownership on the type they prefix: one union member, or a standalone ∪ hole. There is no grouping parenthesis in type position — ( opens a function type and nothing else, so (A ∪ B) is a parse error (PARSE001); write the marker on the member (ra A ∪ B).
• Two hole kinds share the holeType production. _ is the monomorphic hole ("infer exactly one inhabitant type"); the standalone ∪ is the union hole ("infer a finite multi-member union"). Both are legal wherever a base type is: bindings, returns, params, fields, and type arguments (lista<∪>, tabula<K, ∪>, → ∪).
• Lone-`∪` rule: a ∪ hole consumes the whole type expression — any following ∪ is a parse error (A ∪ ∪, ∪ B rejected, issue unexpected_cup_after_union_hole). _ keeps today's behavior and may still appear as a binary-cup member (_ ∪ B).
• Binary-cup disambiguation: ∪ between two non-hole types remains the inline value-union operator (A ∪ B, nullable T ∪ nihil); the hole reading applies only when ∪ stands alone in a base-type position.
• Inline union T ∪ U (cup) for ad-hoc value unions; T ∪ nihil is the canonical nullable type form (lowers to Option<T>).
• Inline intersection T ∩ U (cap) is the nominal type intersection: type Reversible = Readable ∩ Seekable names the conjunction, and the implements clause accepts ∩ as the same separator as the comma (class A implements Readable ∩ Seekable ≡ the comma list). ∩ binds tighter than ∪ (A ∩ B ∪ C is (A ∩ B) ∪ C); nested intersections flatten like unions. Intersection operands are nominal-only (interfaces/structs; aliases resolve through) — primitive operands are rejected at lowering. Implements slots admit ∩ only: ∪ or a hole in an implements position is a parse error (disjunctive conformance is not a checkable contract).
• Signature clauses stay explicit: _ and a standalone ∪ are rejected in return (→ _) and error-channel (⇥ _) positions; both holes stay legal in local binding slots (const _ v, const ∪ v).
• Unions are parsed as a flat member list; duplicates and nihil-only cases are diagnosed in semantic lowering.
• tự_nguyện is a declaration marker (post-name on params/fields), never a prefix on types.
• Qualified type paths such as terminus.Terminus name a type through an imported namespace binding. The prefix must resolve to a namespace; the final segment must resolve to a type-bearing declaration.
• There is no runtime reflection. Types are compile-time facts. Serialization goes through conversion (↦ json, ↦ valor).

Function types enable higher-order function signatures:

functio filtrata((T) → bivalens pred) → lista<T>
functio compose((A) → B f, (B) → C g) → (A) → C
functio apply((numerus) → numerus ⇥ textus op, numerus n) → numerus ⇥ textus

Primitive Types#

Bare textus / ascii / octeti remain the unbounded productions. The shipped forms textus<N>, ascii<N>, and octeti<N> take one kích_thước / NATURAL applied argument. That N is capacity, not a width marker and not a language-wide default. _ in that slot (ascii<_>, textus<_>, octeti<_>, lista<T, _>) is a capacity hole: the form stays bounded, and N is inferred from a same-family bounded witness. Bare ascii is not a hole.

Capacities and extents are buffer bounds, so a capacity or extent value may arrive at compile time or at run time (kích_thước means one thing everywhere; gpu-reset rule 11). Admitted, scheduled (FLD K14), not shipped: today every capacity and extent must be a compile-time value or inferred from a witness. Under K14 the same syntax accepts a run-time-origin size, a _ in a capacity or extent position means inferred if possible and otherwise bound at run time, and a size relation that cannot be proven statically is checked at the call boundary as a recoverable error, never a silent reshape. Type parameters, element types, numeric widths, tensor rank and layout, vector and matrix register shapes, and atomic<T> stay compile-time; a whole-shape _ must still resolve its rank at compile time.

**octeti ≡ lista<octetus> is a type-identity fact (D10.4), not mutual assignability**: the two names denote the same type for checking, ↦, and every emitter, while octeti keeps its byte-buffer runtime representation (no element-boxing regression). ascii<1> is an ordinary ASCII string of length one (the type of 'x'), not a separate character type; it widens implicitly ascii<1> → littera → textus (D10.5), so s[i] ≡ '\n' keeps working across the chain.

A sized numeric type is written as its bare width marker (not a user type parameter): i8, i16, i32, i64, u8, u16, u32, u64, d64, inf (the integer family) and f16, bf16, f32, f64 (the float family). The three policy words wrap a marker and keep their <W> argument:

Bare numerus / fractus remain shorthand for i64 / f64. The bare marker (i32, f32, d64, inf) is the canonical spelling of a sized numeric type. The wrapped spelling numerus<W> / fractus<W> (en int<W> / float<W>, and the same words of every locale pack) is rejected at parse time with numeric_wrapper_retired (PARSE040), which names the form written and the bare replacement. This covers family-correct forms (numerus<i32>), wrong-family forms (numerus<f32>, fractus<i32>), numerus<d64> and numerus<inf>, the removed numerus<d32>, extra arguments, and the marker holes numerus<_> / fractus<_> (write bare numerus / fractus, or a bare marker). inf is the one marker with no range: it is integer-only (not a float width), and an unbounded integer has no word to wrap or clamp at, so môđun<inf> and saturatus<inf> are accepted and change nothing.

d64 is the one decimal width, for money and accounting (there is no narrower decimal width). A decimal literal in a decimal context (`d64 a ← 4.2) keeps its digit text, and d64 is the scaled integer i64` × 10⁻⁸: eight fraction digits and a range of ±92,233,720,368.54775807, so 4.2 + 0.1 is exactly 4.3. Arithmetic is exact until the store, the same model as integers: + and - are exact, * is exact and its scale grows (scale 8 × scale 8 is exact at scale 16), and / rounds half-even to the larger operand scale, all in a wide intermediate bounded by a 128-bit carrier at its scale (past it the operation traps). The d64 slot applies its policy where the value lands: it rounds half-even to scale 8 and traps when the value leaves the range, so amount * rate * (1 + tax) rounds once, at the store; per-step rounding is written as separate stores. d64 takes only the trapping policy (saturating<d64> and wrapping<d64> are rejected: a clamped money amount is silently wrong). The d marker is integer-family only: d64 is not a float width. Integer literals in a decimal context are rejected (decimal_integer_literal_rejected); write 1.0 or convert explicitly with ↦, as for every crossing between number families. A decimal literal with more than eight fraction digits into d64 is a compile error: a written literal is never silently changed, while a computed value is rounded by the slot. Display (D2.6): with a ¶ spec the value prints exactly as the spec says (`12.5 ¶ ".2" is 12.50`, rounding half-even when the spec cuts digits); without one (print, § holes) it prints the shortest form with trailing zeros dropped, 12.5 and 12, never 12.50 or 12.0. A decimal stores its value only, with no per-value scale. môđun<_>, saturatus<_>, and instans<_> are marker holes: the family stays identity and only the width/precision is inferred from a same-family witness (exact marker, no lattice widening). Unsolved _ is an error, never the bare default. The wrapped holes numerus<_> and fractus<_> are retired with the wrapped numeric spelling (numeric_wrapper_retired). A convert hint is never a type argument, so there is no hint hole; hints are thông_qua clauses.

Numeric model#

The numeric rules below are D11.1–D11.8 and the operator rulings of 2026-09-29/30 (delivery spec d11-6-widening-delivery.md §3). They apply to scalars on the host; tensors and kernels follow the same store rule per element, with the device profile of ruling 18.

Exact values, checked stores. Integer arithmetic computes the exact mathematical result; an expression is a number, not a container. Every intermediate of bounded operands must lie in one 64-bit range, [−2⁶³, 2⁶⁴ − 1] (it fits some 64-bit integer, signed or unsigned); outside it the operation traps. The only way past that cap is an operand typed inf, the opt-in unbounded integer (see The unbounded integer inf). Overflow is therefore observed only where a value **lands in a typed slot**, and every such store applies the slot's policy: declaration, assignment, ↑/↓, field, argument, trả, nhường, collection element, and the other store positions of the spec (a print, a § hole, a ¶, a comparison or a condition has no slot and never traps for size). x * 3 / 2 with x: u8 = 100 computes 150 and fits; with 200 it computes 300, which traps at the store, not at the multiply. A check is omitted only where the compiler proves the value fits. A value known at compile time is checked at compile time.

Slot policies. The policy lives in the type, read once at the declaration:

saturating<u8> with x = 250 and x + 200 - 100 stores 255, not the 155 that clamping each step would give; per-step clamping is written as separate stores into saturating slots. This departs from Rust Saturating<T> deliberately. môđun reduces only at the store too (operator ruling 2026-10-02: math happens in the ether): (a + b) / 2 with wrapping<u8> 200 and 100 is 300 / 2 = 150, a + b ≡ 44 is falsum and print a + b prints 300. For + - * ⇐ ∧ ∨ ⊻ ¬ that feed a store directly, reducing once at the end equals reducing each step, so a backend may keep per-operation modular arithmetic there, where no one can observe the difference; the operand of ⇒, /, % and a comparison is read, so it is exact. Ported hash and crypto code keeps its results by storing into a wrapping<W> slot before dividing, shifting right or comparing. Within one policy family a store into a narrower width applies the slot's policy (wrapping<u32> into wrapping<u8> reduces); crossing policy families needs ↦. A constant stored with ← follows the slot's policy (saturating<u8> w ← 300 is 255, wrapping<u8> w ← -1 is 255, and a trapping slot's certain trap is a compile error); a constant in an = position (a hằng T X = e constant at module level or in a block, tĩnh, field default, enum member) must fit W whatever the policy. Literals in môđun<W> and saturatus<W> slots must fit W. The unbounded integer inf (D11.5) is a type (see its subsection below), so a bounded expression still obeys the 64-bit range above and an inf slot never applies a size policy.

The D11.8 naming frame puts the policy outside and the representation inside: en trapping<W>, wrapping<W>, saturating<W>; la exactus<W>, môđun<W>, saturatus<W>. A bare marker takes its domain's default policy (u8 is trapping<u8>; integers and d64 trap, floats follow IEEE).

Shipped (N7a, N7e): the trapping policy word (exactus<W> / en trapping<W>, integer widths and d64), bare markers in every type position, and signed widths on môđun<W> — wrapping<i8> reduces into the signed range, so 100 + 100 stored into it is −56. Admitted, not shipped: the float cells (exactus<f32> is rejected as trapping_float_not_implemented; môđun and saturatus take no float width). Shipped (N7c/N7d): the retirement of the long forms: the canonical emitter writes the bare marker and the parser rejects numerus<W>/fractus<W> (en int<W>/float<W>) with numeric_wrapper_retired; the policy words keep their <W>.

Implicit and explicit failure differ. A failed implicit store is a trap of its own identity: it never enters the ⇥ channel, even inside làm … bắt, and its message names the value, the destination type and the slot (for an inferred slot, the expression the type came from). Only an explicit ↦ is recoverable (⇥, ⊥, bẫy). ⊥ never catches a trap.

Expression types: the range rule. The type of a trapping integer expression is the smallest integer type that holds every possible result, computed by interval arithmetic from the operands' declared types and never from the destination. With u8 operands a + b and a * b are u16, a - b, -a and ¬a are i16, and a / b, a % b, a ⇒ n, a ∧ b and a ∨ b are u8. Only trapping types grow. A môđun<W> or saturatus<W> operand takes part by its declared width and gives the same range-rule type: the word reduces or clamps only where a value is stored into a slot, never mid-expression. Growth stops at the 64-bit containers: past them the type keeps the sign of the range (i64 if it can be negative, else u64), so u64 - u64 is i64 (operator ruling 2026-09-30: it does not become inf; write a ↦ inf - b for the exact difference). _ slots take the expression's type (hằng _ t ← a + b with u8 operands is u16); a collection literal with no declared element type, a ✓ ✗ conditional and tổng take theirs from the same rule. The one exception to the growth cap is an operand typed inf: see The unbounded integer inf.

Untyped constants. A literal, or an expression made only of literals, is an exact number with no type. Beside a typed operand its value joins that operand's range; in an annotated slot it takes the slot's type and must fit at compile time (hằng u8 d ← 10 - 100 is a compile error); otherwise it defaults to int. A constant of any length is an exact number: an integer literal has no upper bound (see The unbounded integer inf), and where it may land is decided by the slot. Beside a float operand it is checked once: an integer constant must be exactly representable (x + 1 with x: f64 is legal, 2⁵³ + 1 is a compile error), a constant beyond the float's finite range is a compile error, and a decimal literal rounds to the nearest float.

Implicit widening is lossless only. Integer widenings that hold every value stay implicit (u8 → i16); u64 has no bounded target and requires ↦, and its one implicit target is inf (every integer width widens into inf, which widens into nothing). Crossing number families (integer, d64, float) always needs ↦, in arithmetic and at stores: hằng fractus f ← n with n: i32 needs n ↦ f64. u64 with a typed signed operand is a compile error in every join (arithmetic, ✓ ✗ branches, ∧ ∨ ⊻, collection literals, tổng): u64_signed_arithmetic_requires_conversion, fixed with ↦ (to i64 or to inf). Untyped constants are exempt (x - 1 with x: u64 is fine).

Division. / is the programmer's division and ÷ the mathematician's. On integers a / b is ⌊a / b⌋ and a % b is a − b·⌊a / b⌋, which takes the divisor's sign: 7 / 2 is 3, -7 / 2 is −4, -7 % 2 is 1, 7 % -2 is −1. The only failure is a zero divisor. Floor is the mathematical division (x % 2 ≡ 1 holds for every odd x, and / agrees with ⇒); code ported from C, Java, Rust or Go changes its results on negative operands. / on floats is IEEE division. An operation's type is fixed by its operands, never by the destination: hằng fractus avg ← a / b with integer operands is a compile error (integer_quotient_to_float_requires_true_division) whose help points at ÷.

a ÷ b is real division and never yields an integer, including between constants. On floats and d64 it equals /. On integers the result is the smallest float that represents every value of both operand types exactly, never below f32:

Mixed widths use the wider operand (i8 ÷ i32 is f64). Operand types are the range-rule types ((a + b) ÷ c with u8 operands keys on u16); an untyped constant joins by value (u8 ÷ 2 is f32) or defaults to int alone (7 ÷ 2 is f64, 3.5). f16 is never chosen implicitly. ÷ has /'s precedence and associativity and the same glyph in every locale. It is not exact: 1 ÷ 3 rounds, and i64/u64 values above 2⁵³ round even in f64. An integer zero divisor traps; float operands keep IEEE (x ÷ 0.0 is ∞). It has no method twin. The same result type applies per element on tensors.

Bit operations and shifts are pure math. ∧ ∨ ⊻ ¬ and unary - compute the exact value on infinite two's-complement integers, so ¬x is -x - 1 (¬250 is −251, which traps when stored into an unsigned slot; flags ∧ ¬mask still works). Fixed-width complement is what wrapping<W> is for (¬x on wrapping<u8> 250, stored into a wrapping<u8> slot, is 5). x ⇐ n is x * 2ⁿ and x ⇒ n is ⌊x / 2ⁿ⌋. The count is not masked to a receiver width: x ⇒ n past the value's size is 0 (or −1 for a negative x) and never traps, x ⇐ n traps only past the 64-bit range (never on an inf operand), on wrapping<W> it wraps at the store, and a negative count is an error (a compile error for a constant). The count may be any integer type.

Comparisons are exact across families. ≺ ≻ ≤ ≥ ≅ ≇ accept operands from different number families with no ↦ and compare the true mathematical values (i64 ≺ f64 is exact even above 2⁵³; NaN compares false). ≈/≉ compute in the float operand's width. ≡/≠ stay structural and exact-type, so 1 ≡ 1.0 is rejected. A comparison stores nothing, so the family-crossing rule does not reach it.

Conversion. ↦ is the checked, recoverable form (D1.11: ∷ states only what the compiler can prove, and ↦ is a check). Into a trapping integer type it is a magnitude-checked narrowing that fails through ⇥, ⊥ or bẫy. Into a wrapping<W> type it reduces the exact source value modulo 2^W, and into a saturating<W> type it clamps it; neither can fail and neither takes a ⊥ (integer and d64 sources). fractus ↦ an integer width W saturates at the target width, NaN converting to 0 (the cross-tier Rust as status quo); integer W arithmetic traps on overflow while float→integer conversion clamps. Overflow policy lives in the type. There are no per-operation checked, wrapping, or saturating method families. To ask "does this fit?" of untrusted input, convert it to the narrow type with ↦ and handle the failure through the error channel. The inf rows are in The unbounded integer inf.

AIR. AIR (@ radix làn "air") has no representation for a trap, so in an AIR-lane function an integer store is admitted only when the range rule proves it fits, and an operation whose exact intermediate could leave the 64-bit range is rejected the same way. A store that would need a runtime check is a compile error naming the store; declare a wider slot, or write ↦ with a ⊥ default. There is no exemption. An inf type is rejected in an AIR-lane function outright (air_unbounded_integer): AIR has no representation for a heap value.

**The unbounded integer inf (D11.5; F9 rulings 32–50, operator-ruled 2026-09-30).** inf is the opt-in integer with no range: every integer is a value, ∞ and NaN are not (inf has no upper bound; ∞ is not one of its values). It is never a default and is never inferred from bounded operands; an author writes inf in a slot or converts with ↦ inf. Its rules in full:

• Spelling. inf is a width marker in the numerus family, written the same in every locale: it is not a keyword and has no glossary word, and, like u8, it is reserved in type position only. inf, trapping<inf>, wrapping<inf> and saturating<inf> (la exactus<inf>, môđun<inf>, saturatus<inf>) are one type; the policy words are accepted and never produce a wrapping or saturating word. faber format keeps the author's spelling among them. ∞ remains the IEEE float literal and is never an inf value (hằng inf x ← ∞ is a compile error); a float ∞ prints as inf, the same three letters, by the long-standing float print rule.
• Literals. An integer literal may have any number of digits in decimal, 0x, 0o and 0b forms. A literal, or an expression made only of literals, is an exact untyped constant whatever its size, folded exactly. It lands where its exact value fits: in an inf slot, or beside an inf operand, always; in a bounded slot, beside a bounded operand, or as the default int, only if it fits that range, else numerus_literal_out_of_range (so hằng _ x ← 18446744073709551616 is a compile error and hằng inf x ← 18446744073709551616 is legal). A trường_hợp constant pattern on an inf subject takes a big literal. A position that names a size or a code rather than a value (capacity, tensor extent, thoát code, kiểm_thử count, enum member value) keeps the u64 range: a longer literal there is a parse error.
• Join. An operand typed inf makes the result inf for every integer operator (+ - * / % ⇐ ⇒ ∧ ∨ ⊻, unary - ¬, potentia, tổng, ✓ ✗ branches, collection literals). An untyped constant beside an inf operand joins by exact value. Nothing else changes: bounded operands keep the 64-bit cap, and u64 - u64 stays i64 (it does not become inf).
• Widening. Every integer width, u64 included, widens implicitly into inf (hằng inf x ← u needs no ↦); inf widens into nothing. Crossing families (float, d64) still needs ↦.
• Arithmetic. Exact and never a size trap: + - * do not trap; / is floor and % the floor remainder; ∧ ∨ ⊻ ¬ act on infinite two's complement; x ⇐ n is x · 2ⁿ and x ⇒ n is ⌊x / 2ⁿ⌋ with no cap; potentia is exact; ÷ is true division in f64. The only failures are a zero divisor, a negative shift count or exponent (the existing traps), and exhaustion of memory, which is a resource fault: fatal, never the ⇥ channel, never caught by bắt. The language sets no upper bound; an implementation may (the MIR runner has a configurable bit-length ceiling).
• Comparison and keys. ≺ ≻ ≤ ≥ ≅ ≇ compare exact mathematical values against any integer width, d64 or float (±∞ order beyond every integer); ≡ ≠ stay exact-type (inf ≡ i64 is rejected). An inf value is hashable and totally ordered, so it is a valid tabula key and copia element.
• Stores. A store into an inf slot is total and emits no check. A store from an inf value into a bounded trapping slot is an implicit checked narrowing: it traps (implicit_store_out_of_range, never ⇥), unless a constant is proven to fit. inf is in the trapping family, so a store into a wrapping<W> or saturating<W> slot needs ↦, which reduces or clamps the exact value and cannot fail. saturating<u64> hi; hi ↑ at the bound still traps; the clamp is written ((hi ↦ inf) + 1) ↦ saturating<u64>.
• Conversion `↦`. Any bounded integer, including a word, converts to inf and never fails. inf ↦ a trapping width is a magnitude-checked narrowing and is failable (a handler is required except for a proven constant); into wrapping<W> / saturating<W> it reduces / clamps and cannot fail. inf ↦ a float rounds to nearest-even and yields ±∞ beyond the float's finite range (a constant beyond it is a compile error); a float ↦ inf truncates toward zero and fails only for NaN and ±∞. inf ↦ d64 is range-checked and failable; d64 ↦ inf truncates and cannot fail. textus/ascii ↦ inf accepts an optional sign and digits of any length (failable on malformed input; thông_qua Hex|Bin|Oct as for other integers); inf ↦ textus writes the decimal digits. inf ↔ octeti thông_qua Be|Le is the minimal two's-complement encoding and its exact inverse. inf ↦ … thông_qua Bits is rejected (no fixed width), and inf ↦ littera thông_qua Code is not a row (write x ↦ u32 ↦ littera thông_qua Code). inf ↔ valor/json carries the integer exactly.
• Host only. inf has no device layout. tensor, sparsa, vector and matrix reject an inf element (tensor_element_unbounded; use lista<inf>), a kernel rejects an inf parameter, return, local or field (nucleum_host_type), and an AIR-lane function rejects every inf type (air_unbounded_integer).
• Collections and loops. lista<inf>, tabula<inf, V>, copia<inf>, tuples, inf ∪ nihil, genus fields, variant payloads and generic instantiation at inf are ordinary. In lặp khoảng a‥b the binder takes the join of the bounds (an inf bound gives an inf binder).
• Display. print, a § hole in a template and a composite print show the decimal digits with a leading - for a negative, with no grouping or suffix; the ¶ integer specs apply as for int.

What is shipped. inf is shipped; every rule above is checked at compile time and computed exactly at run time. The front end accepts the type in all four spellings, the host-only rejections, big literals and their slot rule, the join, widening, store and conversion typing rules, and comparisons. Literal-only float expressions fold exactly before the slot rounds them. Run-time semantics are carried per target, on an unbounded integer of the target's own:

• Supported. The MIR runner (the oracle), Rust, TypeScript, Go and Python run the arithmetic, comparison, conversion and display rules above; the runner also runs the lặp binder over inf bounds. The runner, Rust and TypeScript also carry the octeti thông_qua Be|Le and valor/json rows with every digit; Go carries valor ↦ inf and octeti thông_qua Be|Le. The Racket (sexp) target carries the arithmetic and comparison rows.
• Named gaps. Python has no ↦ valor and no octeti route; the Racket target lacks formatted display, genus printing and ↦ valor (as it does for every type); Go fails closed on a few container and intrinsic constructs holding an inf; TypeScript keeps bounded int and u64 as numbers, so a bounded u64 slot past 2⁵³ still traps there. Each gap is a named compile-time diagnostic or a documented trap, never a bounded substitute.
• Fail closed. Swift, Haskell, LLVM and Wasm have no unbounded carrier and reject inf with a named diagnostic (inf_target_unsupported on Swift and Haskell, llvm_target_inf_unsupported, mir_wasm_unsupported). The language does not change to fit them. Metal, WGSL and AIR never carry inf: it is host only, rejected by language rule before emission.

The per-target rows with their open gaps are kept in the target capability matrix and the numeric model; this file states only the language.

Generic Collections#

A figura is _, a natural number, a size identifier, or a bracketed list of nested figura values; empty [] is rank-0. Bare tensor<T> is incomplete — use tensor<T, []> for rank-0 or tensor<T, _> to infer shape.

Extents follow the same binding-time rule as capacities (see the capacity paragraph above): shipped, every extent is a compile-time value and a _ extent infers from a witness; admitted, scheduled (K14), not shipped: [H, W] accepts compile-time and run-time extents alike (one syntax, no separate run-time marker), and an unresolved _ extent is bound at run time instead of being an error. Rank and layout stay static.

vacua for tensor<T, []> produces a rank-0 tensor (one default-initialized element slot). vacua for sparsa<T, Figura> (any shape) produces an all-zero sparse tensor with no stored entries. matrix<T, Figura> requires exactly two dimensions; bare matrix<T> and one- or three-axis matrix shapes are rejected. atomic<T> requires T to be i32 or u32 in v1. Atomic cells are not interchangeable with their element type; use load, store, exchange, and compare_exchange receiver methods. Construct multi-dimensional tensors via crea / structa / ↦. Type(...) is not a construction form: vector<f32, 4>(...), matrix<f32, [2, 2]>(...), tensor<f32, [2, 2]>(...), and scalar forms such as numerus("42") are rejected. Use value ↦ Type, named library constructors, or Genus { field = value } records.

Tensor index/shape intrinsic slots (accipe, ponde, forma, crea, structa) accept integer lists that fit the canonical lista<numerus> / &[i64] runtime boundary at call sites (e.g. lista<u32> for GPU thread ids; not lista<u64>). This is a structural exception scoped to those slots — it does not widen the signed↔unsigned numeric lattice (see Index vector parameter policy in tensor-intrinsics.md).

Value unions use inline T ∪ U (nullable: T ∪ nihil). The standalone ∪ hole infers a multi-member union; _ infers a single inhabitant (see docs/design/type-hole-union.md). Tagged unions use hợp_nhất. copia.unio() is a set method, not a type constructor.

Type Sugar#

The bare width marker (u32, f32, d64, inf) is the canonical spelling of a sized numeric type, and lista<u32> is the canonical collection form. The wrapped numerus<W> / fractus<W> form is rejected (numeric_wrapper_retired). Type sugar (lu32, tf32, …) is an ergonomic alternate spelling for collection types. It is type-position only and semantically identical to the long form — the compiler treats both the same. This is the single canonical reference for sugar; the rest of the specification uses the long collection form.

Sugar combines a width marker with an optional one-letter family prefix. Width markers are i8/i16/i32/i64 (signed), u8/u16/u32/u64 (unsigned), and f16/f32/f64 (float); inf (the unbounded integer) is a bare marker only. A bare width marker (no prefix) sugars the scalar numeric type; a family prefix sugars a collection of that width. In the grammar, WIDTH_MARKER is a bare marker; LISTA_WIDTH_SUGAR, TENSOR_WIDTH_SUGAR, SPARSA_WIDTH_SUGAR, VECTOR_WIDTH_SUGAR, and MATRIX_WIDTH_SUGAR are that marker prefixed with l, t, s, v, and m, respectively.

Bracket shapes: [] is rank-0, [2, 3] is a fixed shape, and no bracket infers the shape (_). Matrix requires exactly two dimensions. Sugar never uses <>. For non-width element types (e.g. tensor<textus, [3]>), use the full form.

Sugar is reserved in type syntax only — value identifiers named tf32, lf32, etc. are unchanged. inf takes no prefix: linf, tinf, sinf, vinf and minf are not sugar and stay ordinary identifiers (sinf and linf are common names, and a tensor, sparsa, vector or matrix element may not be inf).

môđun<W>, saturatus<W> and exactus<W> have no sugar; write môđun<u32> / saturatus<i16> / exactus<u8> in full (the bare marker u8 already is the trapping u8).

Spelling preference (author convention, not grammar): general Faber code tends toward the long collection form (lista<u32>) for readability; numeric/tensor-primary modules may prefer sugar. Choose per module or file.

---

Control Flow#

Conditionals#

• nếu = if, nếukhôngthì = else-if, khác = else. nếukhôngthì takes its condition directly (nếu a { … } nếukhôngthì b { … } khác { … }); nếukhôngthì nếu b and khác nếu b are parse errors.
• c ✓ a ✗ b is the one value conditional: a when c holds, else b. ✓ (U+2713 CHECK MARK) and ✗ (U+2717 BALLOT X) are the same in every locale and have no word twin. It is one level only: a ✓ ✗ inside the condition or either branch is rejected (conditional_nested); choose among more values with a function whose nếu arms each trả. The branches narrow exactly like nếu branches (after r là numerus, r is numerus in the ✓ branch).
• c ? a : b and c sic a khác b (en c yields a else b) were removed and are rejected with a migration diagnostic; write c ✓ a ✗ b. sic stays a reserved word only to carry that diagnostic. The look-alikes ✔ and ✘ are rejected with a "did you mean" hint.
• do_đó for one-statement bodies, including do_đó trả, do_đó ném, do_đó chết, and do_đó im_lặng (∴ is not accepted here)
• im_lặng for explicit no-op (from musical notation: "it is silent")

Loops#

• trong_khi = while
• lặp từ...hằng/lặp từ...biến = for-of (values)
• lặp ra...hằng/lặp ra...biến = for-in (keys)
• lặp khoảng range hằng/biến i = range iteration (e.g. lặp khoảng 0‥10 qua 2 hằng i { ghi_chú i }; qua belongs to the range expression)

Range step and direction (`range_tail`, `qua`). The bounds alone pick the direction of a range: a‥b and a…b count up when a <= b and count down when a > b. The optional qua step is a positive stride applied in whatever direction the range moves, so 10‥0 qua 2 yields 10 8 6 4 2, `0‥10 qua 2 yields 0 2 4 6 8, and 10…0 qua 5 yields 10 5 0`. A step is never signed: a zero or negative step is an error, a compile error (range_step_not_positive) when the step is a literal and a run-time trap otherwise. Equal bounds walk the ascending way (5‥5 is empty, 5…5 is the single value 5). The step never changes which endpoint a range includes: … includes its end only when the progression reaches it.

A range binder declared biến is a fresh per-iteration copy of the walk's counter. A write to it inside the body (lặp khoảng 0‥6 biến i { i ← i + 1 }) changes only the body's copy and never steers the loop, so the example visits 0 1 2 3 4 5. In an lặp khoảng product each binder is refreshed once per iteration of its own axis.

Iteration order. A type whose order is part of its value iterates in that order. lista iterates by index. textus iterates its characters in order. tensor, vector, and matrix iterate by index, outer axis first (row-major). Two equal values always iterate identically.

copia and tabula iterate in unspecified order. The order is not promised and not deliberately random; backends may differ. When order matters, sort explicitly. ≡ on these types stays structural and does not depend on order. A map or set that promises an order is a separate library type, not a mode of tabula or copia.

There is no iteration interface. lặp từ works on the built-in iterable types and on cursors. A user type that should be iterable exposes an ordinary method that returns a cursor (lặp từ arbor.nodi() hằng n); nothing is called implicitly.

Switch/Match#

phân_tích is a statement, not an expression. A value chosen by a match comes from a function whose arms each trả. The compiler checks exhaustiveness and definite return, and the function can be tested on its own.

Coverage is checked as a pattern matrix. Each scrutinee has a space: the variants of an liệt_kê or hợp_nhất, the members of a union, and bivalens as the closed set {đúng, sai}. A match over several scrutinees is checked over their product, so phân_tích a và b over two bivalens values needs all four combinations or a mặc_định. A missing variant or combination is an error that names one uncovered case. The multi-subject form parses today — subjects are comma-separated, and an arm's patterns are separated by , or và (trường_hợp đúng và sai) — and its coverage is checked over the product, but its lowering is admitted, not shipped (D22.4, the dms unit): the Rust emitter lowers it, while the MIR runner, TypeScript, Go and Haskell reject it (for example `unsupported MIR lowering: multi-subject phân_tích before switch MIR lowering). Open types (numerus, textus`, …) are complete only with a catch-all arm. When coverage cannot be computed for a pattern kind, the compiler warns that it was not checked; it is never silent. chọn keeps its switch meaning: over an open domain, a missing mặc_định is an implicit no-op default, while a closed domain is checked.

Pattern Matching#

Patterns are flat. A trường_hợp arm names one variant and binds its fields, or names one literal value; it does not match inside those fields. Nested patterns are left out for simplicity, not because they cannot be checked: a phân_tích inside an arm is two flat exhaustive switches.

A negative number pattern is written with a leading minus (trường_hợp -1, trường_hợp -∞). The lexer never signs a number, so the pattern claims the sign; - before anything else is not pattern syntax.

phân_tích matches a closed set and nothing else: the variants of an liệt_kê or hợp_nhất, or the members of a union (trường_hợp numerus hằng n over numerus ∪ textus). It is not a generic "match this thing" keyword. A type pattern that is not a member of the scrutinee's closed set is rejected (SEM010 discerne_pattern_not_in_closed_set). That covers numeric-width patterns (trường_hợp u32 over a numerus) and length-shaped patterns (`trường_hợp lista<numerus, 4> over a lista<numerus>; bounded textus, ascii` and octeti; tensor figures). Ask an integer's width or range with an là test, and ask a length with .longitudo() in a nếu.

There are no range patterns (trường_hợp 1‥5). Test the range with nếu inside the arm.

A NaN pattern is rejected. NaN never equals itself, so it could never match; test for NaN with nếu instead.

Guards#

Match arms have no guards. phân_tích is one arm per variant, and a guard would split one variant's logic across several arms. Nest a nếu in the arm instead.

Destructuring Extraction#

Destructuring is flat. A nested pattern such as [[a, b], c] is rejected; destructure the outer value, then the inner one on another line.

Parameters are not destructured. A pattern in a parameter slot would hide the parameter's type from a type-first signature. Destructure in the body.

Control Transfer#

dừng and tiếp take no label. They apply to the nearest enclosing loop. A nested search that needs an early exit from an outer loop becomes a function that trảs.

• đợi_trả awaits a compatible promise and returns its success value from a async function.
• đợi_bỏ awaits a compatible promise to completion and discards any success value.
• nhường is statement-initial yield from sinh / async_sinh; it is not an expression-form await.

---

Error Handling#

• bắt attaches to the structured forms whose productions name catchClause: conditional arms, trong_khi, lặp, chọn, and làm. It does not attach to arbitrary bare blocks.
• Use the explicit do block when a standalone block needs a handler: làm { ... } bắt err { ... }.
• ném = throw (recoverable), chết = panic (fatal).
• A same-line nếu <expr> guard on ném and chết is line-sensitive parser sugar: ném val nếu cond desugars to nếu cond { ném val } at parse time. Its canonical, compression-safe spelling is the expanded nếu block. A source compressor must expand this sugar before removing line breaks; the guarded shorthand remains under language review.
• khẳng_định is a runtime invariant check. It desugars conceptually to chết "msg" nếu !cond, with the positive condition kept in source form and the inversion applied during lowering. The optional particle is chết (en panic): khẳng_định cond chết msg / assert cond panic msg. Bare khẳng_định cond stays legal. An khẳng_định failure is fatal and uncatchable by bắt (it lowers to a panic, not a Result-channel error); in test context the harness isolates each kiểm_thử so a failed assertion ends that test without ending the suite.
• yêu_cầu is the recoverable require statement (en surface require … throw …), the typed-error-channel twin of khẳng_định. yêu_cầu cond ném err desugars to nếu không (cond) { ném err } at lowering; the thrown value enters the function's ⇥ E channel and is catchable by bắt/làm, unlike khẳng_định (fatal). A yêu_cầu statement in a ⇥-less function is a compile error, same as ném. The particle is ném (en throw) and is required.

• từ_chối is the reject statement (en surface reject … throw …), the boolean opposite of yêu_cầu. từ_chối cond ném err desugars to nếu (cond) { ném err } at lowering — it throws when the condition holds, where yêu_cầu throws when it fails. The thrown value enters the function's ⇥ E channel and is catchable by bắt/làm. A từ_chối statement in a ⇥-less function is a compile error, same as ném. The particle is ném (en throw) and is required.
• @ conversio (en @ conversion) on a top-level hàm declares an admitted error conversion: the parameter's type is the source error, the return type is the destination, and the compiler enrolls that ordered pair so a propagating ⇥ E failure converts at the boundary instead of needing a per-caller wrapper. The marker is bare and the conversion is an ordinary function outside any union body; only a direct (source, destination) row is admitted — a missing row fails closed and is never auto-composed into a chain. The earlier union-arm form (the marker carrying a payload inside a hợp_nhất body) is retracted. ---

Expressions#

Operators (by precedence, lowest to highest)#

Postfix tensor transpose (`ᵀ`, U+1D40): valueᵀ is rank-2-only sugar for the existing transpone intrinsic and Transpose plan entry. It maps [M,N] to [N,M]; rank-1 is a permanent decline because there is no row/column distinction, while rank-3+ waits for a batched-transpose consumer. The precedence interaction with parse-only gradient selection is settled law, not an open fork: a · bᵀ ∇ [x] parses (a · bᵀ) ∇ [x], so the transpose suffix is consumed before the selection suffix. ⊤ remains unspent.

Hadamard divide (`⊘`): a ⊘ b is element-wise division, the divide companion of ⊙. It binds at the multiplicative tier with * and the other glyph products, left-associative.

Tensor lifting (FLD K4, K5): the scalar operators lift to tensors elementwise with no grammar change. Shipped: + and - (binary and unary) against a scalar or an equal-shape tensor, * by a scalar, / and % by a scalar, ÷ on any shape (with the per-element result widths of the Numeric model), ⤒/⤓ tensor against tensor, the comparisons ≺ ≻ ≤ ≥ ≡ ≠ ≅ ≇ (each yields a tensor<bivalens>), the logic words và / hoặc / không on tensor<bivalens>, the ✓ ✗ select with a tensor<bivalens> condition, and hoặc_nếu_rỗng when the elements are nullable (tensor_coalesce_element_nullable_required otherwise). The math methods abs sqrt exp ln log10 nếukhôngthì cos tan (Latin absolutum radix exponentia logarithmus logarithmus_decimalis sinus cosinus tangens) lift the same way; the float functions need float elements, and a user function is never lifted (tensor_function_not_lifted). Tensor ≈/≉ are deferred (tensor_approx_comparison_deferred), and tensor * tensor is still rejected (numeric_operands_required; its ruling is FLD K10, not shipped). Lifting runs on the MIR runner (the math methods also lower on Rust); every other emitter fails closed (tensor_lift_unsupported_on_target).

Division (`/` and `÷`): both bind at the multiplicative tier with *, left-associative. / floors on integers and % takes the divisor's sign; ÷ is true division and yields a float (f32 for 8- and 16-bit integer operands, f64 otherwise). See Numeric model.

Extrema (`⤒` / `⤓`): a ⤒ b is the maximum and a ⤓ b the minimum of two values. They are pure arithmetic operators at the additive tier with + and -, left-associative: a ⤒ b ⤓ c is (a ⤒ b) ⤓ c.

Exact-output transfer (`⇇`): sink ⇇ payload invokes a callable sink value — one argument, vacuum result — once per payload. The operator performs no formatting, adds no separators or terminator, selects no channel, and runs no conversions: the bound value owns destination and behavior, and the compiler holds no console knowledge. A chain sink ⇇ a ⇇ b evaluates the sink expression once, each payload once left-to-right, and invokes the sink once per payload left-to-right; the chain result is vacuum. ⇇ binds above assignment and below ternary, so postfix calls, conversions, and string-constructor applications finish before transfer; formatting is explicit on the right (`output ⇇ "§ § "(a, b)`). Combined with selective value imports it replaces compiler-owned output statements with ordinary typed values.

Conversion-directed assignment (`↤` / conversio-assign): place ↤ value evaluates the right side, converts it to the statically known type of the left place through the existing ↦ route, then assigns. It binds at the same precedence as ← and is right-associative; the ⊥ default (inline_default) is legal only on `↤` — a ⊥ after ordinary ← is rejected, and in a right-associated ↤ chain the default attaches to the nearest ↤. The operator is preserved verbatim through syntax and emission; it is never rewritten to ← or ↦. Typed hằng/biến initializers accept ↤ (convert to the written type, then initialize); hằng _, đặt, and untyped destructuring have no concrete destination and are rejected.

là and không là are a type test: the right-hand side is always a type — including a declared or imported one — and the result is a runtime variant/type test on the value. They never convert and never compare values; a value spelling on the right is rejected in the reader's own words (SEM011:est_value_rhs), pointing at the equality family. The null type is the one type spelling that also names a literal slot: x là nihil tests the null type, while the null value is không_gì (null in the English reader). Use ≡ / ≠ (or ≢) for structural value equality, ≅ / ≇ for promoted exact equality (same value after numeric widths join), ≈ / ≉ for fuzzy equality (tolerance match with Python-isclose defaults: rel_tol 1e-09, abs_tol 0.0), and ↦ for runtime conversion.

Retired predicate keywords are not prefix unary syntax. Use expr ≡ đúng, expr ≡ sai, expr ≡ không_gì, expr là nihil (the null type test), expr ≺ 0, or expr ≻ 0.

The legacy ASCII spellings < and > are not productions of this grammar — both remain generic delimiters — though the shipped parser still accepts them as comparisons during the glyph migration; prefer the canonical ≺ and ≻.

Ordering comparisons (≺, ≻, ≤, ≥) between two textus values compare the whole strings in Unicode code-point order. They do not use locale collation.

Membership (`∈`, `∉`). x ∈ xs tests whether x is an element of the right operand and x ∉ xs is its first-class negation (not sugar over không); both sit in the comparison tier with ≺ ≻ ≤ ≥. One operator covers two meanings, chosen by the type of the right operand: a collection (key membership for a tabula) or a range. The glyphs have no ASCII spelling, and they never apply to text: a textus right operand is rejected with a diagnostic that points to the contains method. The former keywords intra and inter are retired from the grammar.

Format operator (`¶`, U+00B6, D2.1–D2.5, D2.7): value ¶ "spec" renders a built-in value as textus. It pairs with §: § marks where a value goes, ¶ says how it is shown — "Summa: §"(pretium ¶ ".2"). ¶ is an operator, not an arrow, because it cannot fail (D2.4): it is a pure computation like + or ≡, with no state change, no control flow, and no failure path. A malformed spec, or a spec that does not fit the left side's type, is a compile error (pass 1 checks only that a literal is present; pass 2 validates the spec against the left side's type) — a computed spec is rejected. ¶ binds looser than arithmetic and tighter than comparison (a + b ¶ ".2" ≤ 100 ¶ ".2" is (a + b ¶ ".2") ≤ (100 ¶ ".2")) and does not chain (a second ¶ is format_chained). ¶ stays closed to built-in types (numbers, textus, instans); a user type formats through an ordinary function. Holes (§, §N, and the named form) stay pure substitution and gain no spec slot.

The spec vocabulary is one fixed pattern for every type, each type accepting only the parts that make sense: [fill][align][sign][0][width][.precision][kind].

• Numbers: .2 precision (12.50; integers pad too, so 42 ¶ ".2" is 42.00 and integers/floats line up in one column); width ("5" → 42, right-aligned by default); 0 zero-pad ("05" → 00042); < > ^ align, with an optional fill character before the align ("*^7" → **42***); + always shows the sign; kinds x b o (hex, binary, octal) and e (scientific); combinable ("08x").
• `textus`: fill, align, width, and .N — truncate to N characters (littera), following C %.3s / Python {:.3} / Rust {:.3} ("Aurelia" ¶ ".3" = Aur). .N is precision on numbers, maximum length on text — the same split those languages use.
• `instans`: named presets only (iso, date, time); no strftime-style patterns (norma work, if ever).
• Left out on purpose: thousands separators (country-aware, so library work, not this operator) and computed specs (D2.2).
• Split from `↦`: ↦ ascii<N> thông_qua Hex is exact conversion — fixed width, fails if the value does not fit; ¶ is display — width is a minimum that grows to fit, and never fails.
• No word twin: ¶ is the same glyph in every locale, like ✓ ✗.
• d64 decimals print as decimal numbers (D2.6): with a spec, exactly what the spec says (12.5 ¶ ".2" is 12.50, digits cut below the carrier's scale round half-even); without one, the shortest form with trailing zeros dropped (12.5, 12).

Edge-case outputs (D2.7): NaN / ∞ / -∞ print as NaN, ∞, -∞ (precision does not apply); a negative number in hex/bin/oct prints sign plus digits (-42 ¶ "x" = -2a), not two's complement (↦ ascii<N> thông_qua Hex stays the strict tool and rejects negatives); textus width counts littera (characters), not screen columns (an emoji with a skin-tone modifier counts as 2; screen-width alignment is library work); instans outside years 0–9999 with "iso" uses ISO 8601's extended form (+10000-01-01).

Static type ascription (`∷` / verte):

The ∷ glyph (U+2237, "proportion") explicitly ascribes a target type to an expression. Use it when the source expression already exists and the compiler needs a static target shape:

• Primitive/alias → cast (no runtime effect): data ∷ textus → TypeScript: (data as string)
• Built-in collection → target-shaped collection value: [1, 2, 3] ∷ lista<numerus>
• Variant expression → enum/interface target ascription: tạo Click { x = 10 } ∷ Event

Prefer typed construction for ordinary kiểu values and vacua for ordinary empty collection values:

fixum _ point ← Point { x = 10 }
fixum lista<numerus> xs ← vacua

Only the ∷ glyph is accepted as the postfix static type-ascription operator. The Latin forms qua, innatum, and novum were aliases and have been removed (see verte-alias-clean-break).

Runtime conversion (`↦` / conversio):

The ↦ glyph (U+21A6, "rightwards arrow from bar") is the runtime value conversion operator. Unlike ∷ (compile-time cast), this performs actual parsing/conversion that can fail:

• "22" ↦ numerus → Rust: "22".parse::<i64>().unwrap()
• "bad" ↦ numerus ⊥ 0 → Rust: "bad".parse::<i64>().unwrap_or(0)
• 42 ↦ textus → Rust: 42.to_string()
• n ↦ ascii<N> thông_qua Hex|Bin|Oct — shipped; fixed-width lowercase digits, zero-padded to N, with overflow and negative sources rejected.
• n ↦ ascii<_> thông_qua Hex|Bin|Oct — shipped for const-foldable numerus sources; the hole is solved to the source digit count. Runtime sources leave the hole unsolved and require explicit N.

The `thông_qua` clause (D11.9). A convert hint is a clause on the conversion, not a type argument: "ff" ↦ i32 thông_qua Hex, 65 ↦ littera thông_qua Code, octeti[0‥2] ↦ u16 thông_qua Le ↦ f16 thông_qua Bits ↦ f32. The grammar is conversio_expr := '↦' type_annotation via_clause? inline_default? and via_clause := 'thông_qua' IDENTIFIER.

• thông_qua is contextual: it is claimed only on the conversion's own line, immediately after the target type. Everywhere else it is an ordinary identifier (radix corpora contain 186 real uses of thông_qua as an identifier: gradus 129, examples 29, inferentia 26, norma 2).
• The hint (Hex, Bin, Oct, Be, Le, Bits, Code) is a compile-time identifier that selects the conversion row. It is not part of the target type and it is not a keyword. The set is exactly those seven (there is no Radix hint). Hint spellings are the same short English identifiers in every locale; the word thông_qua itself is per-locale (thông_qua in en and la).
• The clause binds tighter than the ⊥ default: x ↦ u32 thông_qua Hex ⊥ 0 is (x ↦ u32 thông_qua Hex) ⊥ 0. Conversions chain, each hop with its own clause.
• Whether a hint is known, and whether the target takes one, is semantic (lowering), not grammar.

Retired spellings. Before D11.9 a hint was written as the second type argument of the ↦ target (ascii<N, Hex>, littera<Code>) or as a bracketed tail (octeti<16><Le>). Both are rejected at parse time (conversio_hint_type_argument, conversio_hint_tail_argument); the thông_qua clause is the only spelling.

The hint selects the conversion row. Hex / Bin / Oct / Be / Le / Bits / Code are convert hints in the thông_qua clause, not keywords and not new baseType productions. For ascii output, Hex / Bin / Oct select the lowercase fixed-width digit pack; the hint is not part of type identity. Target support is not a grammar production (see Target Support).

• "ff" ↦ i32 thông_qua Hex — shipped; text parse at radix 16 (Bin = 2, Oct = 8). Hex/Bin/Oct text parse is unchanged by endian hints.
• octeti[lo‥hi] ↦ W thông_qua Be / … ↦ W thông_qua Le — endian unpack of an exact-width window (W is i16 / i32 / i64 / u16 / u32 / u64; window length 2 / 4 / 8). Shipped on rust, the MIR runner, Go, and TypeScript. TypeScript i64/u64 stay fail-closed (JS number is not exact). octeti itself has no endian; bytes ↦ u32 without thông_qua Be / thông_qua Le stays rejected. A short window fails (no pad).
• octeti[lo‥hi] ↦ f32 thông_qua Be|Le / … ↦ f64 thông_qua Be|Le — shipped alongside the integer rows (float endian unpack of an exact-width window, 4 / 8 bytes; same fail rules: exact window required, a short window fails, thông_qua Be / thông_qua Le mandatory).
• n ↦ u32 thông_qua Bits / n ↦ u64 thông_qua Bits / n ↦ f32 thông_qua Bits / n ↦ f64 thông_qua Bits / n ↦ f16 thông_qua Bits — shipped; the Bits hint reinterprets between exact-width integer/float pairs (u32↔f32, u64↔f64, u16↔f16, u16↔bf16) bit-identically. It is reinterpretation, not value conversion; wrong-pair rows reject with the structured issue, and Bits is never a base or an ascii format hint. Bits is a thông_qua hint, not a keyword and not a baseType production.
• n ↦ octeti<N> thông_qua Be / … ↦ octeti<N> thông_qua Le — proposed (not shipped) for a scalar source (N ∈ {2, 4, 8}); the hint is a thông_qua clause, not a second capacity. Register targets take the clause today: v ↦ octeti<16> thông_qua Le, corpus[0‥16] ↦ vector<u32, 4> thông_qua Be.
• 'A' ↦ u32 thông_qua Code — shipped; the code point as a u32 (u32 holds every code point, as Rust's char as u32); the source must be littera. 65 ↦ littera thông_qua Code — shipped; builds the character for that code point, failing above U+10FFFF and on a surrogate. Code is a thông_qua hint like Hex/Bits; any other hint on these targets, or a source/target type other than littera/u32, is SEM016 (code_hint_pair_mismatch).
• n ↦ textus / n ↦ ascii / n ↦ littera — a number's digits (D10.6): 7 ↦ textus = "7", 7 ↦ ascii = "7", 7 ↦ littera = '7'; littera fails outside 0–9 (42 ↦ littera fails, two letters).
• littera ↦ numerus — parses the digit, failing otherwise (as "22" ↦ numerus parses).
• littera ↦ textus — the one-letter string; never fails.
• textus ↦ littera — the only letter; fails unless the text is exactly one letter.
• octeti ↦ textus — UTF-8 decode; can fail. octeti ↦ ascii — checks every byte is below 128, same bytes; can fail. octeti[i‥i+1] ↦ ascii — one byte through a window (mirrors octeti[lo‥hi] ↦ W thông_qua Be).

Explicit integer narrowing is magnitude-checked on every backend: n ↦ u8 converts a value that fits unchanged, and a value out of the target's range fails — it never wraps and never relabels. The failure takes the error channel, or the ⊥ default when one is written. Into môđun<W> and saturatus<W> targets ↦ reduces or clamps and cannot fail. Use môđun<W> for wrapping arithmetic.

Interval clamp (`↦ lo‥hi`). When the target of ↦ is a range instead of a type, the conversion clamps a number into that interval: 15 ↦ 0‥10 is 9 (the half-open ‥ excludes its end), 15 ↦ 0…10 is 10 (… includes it), wide ↦ 10…50 clamps one intervallum value into another range, and a stored intervallum value is a legal target too (x ↦ fines). The grammar production is conversio_expr := '↦' (type_annotation | interval_target) via_clause? inline_default? with interval_target := range_expr. The parser reads the operand as an interval, not a type, when it opens with a number literal or a non-type identifier; a capitalized name, a known type word, or a qualified ns.Type stays a type. A clamp is total, so it takes no thông_qua hint (conversio_via_target_takes_no_hint), no ⊥ default (intervallum_clamp_recovery_unsupported) and no qua step (intervallum_value_step_unsupported); these are semantic rejections of a shape the grammar still admits.

Default channel (`⊥`): ⊥ (U+22A5 UP TACK) supplies a value when a conversion or a failable call fails: hằng numerus n ← "abc" ↦ numerus ⊥ 0, or hằng numerus n ← risum() ⊥ 0 (X3, D17.7) when risum is failable. On a conversion it is written immediately after the conversio target (`↦ T ⊥ default) or after the value of a ↤` assignment; on a call it is written immediately after the complete call chain (f(x).m() ⊥ default).

• ⊥ catches only the ⇥ error channel. It never catches chết or traps (for example integer overflow).
• The default is evaluated only on failure.
• The default must type-check as the success type T.
• One expression either propagates (⇥ E) or defaults (⊥ v), never both; ⊥ v ⇥ … is rejected.
• ⊥ binds looser than ↦ T: x ↦ numerus ⊥ 0 is (x ↦ numerus) ⊥ 0. The unparenthesized default is a unary-precedence expression; parenthesize arithmetic, coalescing, ternary, or assignment defaults.
• ⊥ is legal on a conversion (↦ T, ↤) or on a call whose last postfix step is a call suffix (X3): f() ⊥ 0, f() ⊥ 0 + 1 parses as (f() ⊥ 0) + 1 — the default binds at the same postfix tier as the call. After any other expression — a bare identifier, a member or index access, a cast (∷), or a second ⊥ on the same expression (f() ⊥ 0 ⊥ 1) — it is rejected (default_requires_failable); ⊥ is not a general postfix operator.
• ⊥ is an operator between a failable expression and a value. It is not the type-theory "never" type (that is numquam).
• The glyph is the same in every locale. The look-alike ⟂ (U+27C2) is rejected with a "did you mean ⊥?" hint.

⇥ only ever names an error type. The retired inline recovery ↦ T ⇥ value (and ↤ … ⇥ value) is rejected with a migration diagnostic pointing at ⊥.

Using hoặc_nếu_rỗng as a conversio default is rejected with a migration diagnostic. hoặc_nếu_rỗng is local nullable elimination only (x hoặc_nếu_rỗng y, parameter defaults) — not logical hoặc. A parenthesized conversio result may still combine with hoặc_nếu_rỗng as ordinary defaulting.

Call and Member Access#

A call_expr may continue with the zero-argument transpose_suffix ᵀ (U+1D40) after its ordinary primary/member/index chain. This is postfix source sugar, not a method spelling: semantic analysis applies the rank-2-only law and lowers the admitted form through the existing transpone/ Transpose plan entry. a · bᵀ ∇ [x] is settled as (a · bᵀ) ∇ [x].

String And Template Literals#

Faber uses delimiter semantics: each quote form means a different source shape. They are not interchangeable synonyms.

§ (U+00A7) is a template hole in Unicode forms (", «, `). §{label} names a hole with an identifier label; the label is unique within its template and may use a keyword spelling under the contextual law. Named holes are not available in ascii literals, where § remains forbidden.

Rendered templates (textus): "..."(...) and «...»(...) lower to văn_bản_hóa("...", args...).

Captured templates (forma): ...(args) captures template text and parameters without rendering. Safe for bound SQL/URL payloads; do not use «...»(...) for that job.

Block textus uses guillemets «...». The heavy quotation-mark pair is retired (too visually close to " in many fonts).

Implementation status (2026-06-30):

• Shipped: "...", «...» block textus, '...' → ascii, ... → forma, |...| → octeti, { ... } → json, and text/ascii ↦ regex.
• Pending factory delivery: slash-delimited /.../ regex literals.

Inline block example:

fixum _ tag ← «inline»

Multiline block example (newline after opening «):

fixum _ blob ← «
    select id, email
    from accounts
»

Captured template example:

fixum _ q ← `select * from accounts where id = §`(accountId)

Octeti hex literal example:

fixum _ sig ← |de ad be ef|
fixum _ hello ← |48 65 6c 6c 6f|

Format-Template Application#

String literal call syntax is the canonical source form for format-template application:

"§{greet} world"(greet: "salve")
"status: § (§)"(sample_status(), "ok")
"status: §1 (§0)"("ok", sample_status())

The position law counts named and anonymous holes together in order of appearance: "§{greet} §" = [greet: 0, anonymous: 1]. Named labels are erased at lowering, so "§{greet} world"(greet: "salve") lowers identically to the positional form "§ world"("salve") and its canonical văn_bản_hóa("§ world", "salve") form.

This lowers to the compiler's văn_bản_hóa("...", args...) form. Use the string-template form in ordinary source; reserve văn_bản_hóa(...) for explicit desugaring examples and compiler-facing documentation.

For textus, bracket indexing is Unicode-scalar based:

# Produces "§".
"Salve, §!"[7]
# Produces "hello".
"hello world"[0‥5]
# Produces "hello world".
"hello world"[0 usque 10]
# Produces "ace".
"abcdef"[0‥6 per 2]

Text slices accept the full range form, including qua.

For lista<T>, bracket indexing is a single-element access. The index must be one integer; range slices are not accepted (use sectio(start, end) for a copied range):

# Element at position i.
xs[i]
# Write element at position i.
xs[i] ← v

Lista bracket access is plain, not nullable: it returns the bare element T and traps on out-of-bounds. A tensor bracket read is plain in the same way. For nullable list access, use xs.accipe(i) → T ∪ nihil with hoặc_nếu_rỗng.

For tensor<T, Figura>, a bracket read returns the bare element T and traps on a bad index, like a list index; a literal index that is provably out of range is a compile error. Bracket indexing is sugar over the tensor intrinsic surface (the nullable read is the accipe method, not the bracket):

# trapping vector.accipe([id])
vector[id]
# vector.ponde([id], v)
vector[id] ← v
# trapping grid.accipe([r, c])
grid[[r, c]]
# grid.ponde([r, c], v)
grid[[r, c]] ← v

Reads return T (no hoặc_nếu_rỗng is needed); use the accipe method for a nullable read. Rank-1 tensors accept scalar integer indices that fit the tensor i64 runtime boundary (u64 is rejected). Rank-N tensors use a list-shaped index expression such as [[r, c]] or a bound lista<integer> value. grid[r, c] is not syntax; memberSuffix still contains exactly one expression between brackets.

For octeti, bracket indexing is a byte or an exclusive window:

# One byte → u8. O(1). Traps on out-of-bounds.
buf[i]
# Exclusive window → octeti. Fully in bounds or fail (no short slice, no pad).
buf[lo‥hi]

The index must be an integer or a range. A compile-time-provable out-of-range index on an octeti literal (|ra gọi be ef|[0‥5]) is a structured reject. Runtime out-of-bounds traps — the same trapping model as lista bracket access, not textus short-slice. Lista [lo‥hi] stays rejected.

octeti is the endian host. Parse byte windows on the buffer (buf[lo‥hi] ↦ W thông_qua Be|Le). Cross to a list once, for element work, via octeti ↦ lista<u8> (representation change only; other element types fail closed). The reverse lista<u8> ↦ octeti is live. Do not detour through valor. Lists stay for element work, not endian windows.

Primary Expressions#

Non-finite literals are contextual floating-point values: ∞ is positive infinity and nan is NaN. The named form is nan in the Latin (la) pack and nan in every other shipped pack; it is claimed only in the literal slot, so a following ( keeps an ordinary nan(...) call. Their width follows a surrounding f32 or f64 context when present; bare fractus remains unsized, and neither form has a width suffix. A leading - is supplied by unary_expr, so -∞ is unary negation of ∞, not a separate token. A numerus context, inf included, rejects both forms (fail-closed); neither maps to an integer.

Capture boundary (`bẫy`): bẫy { … } (en trap) is an expression that runs its block and reifies the error channel into a value. The block's trailing expression is the success value; the result type is the union of the success type and every error type that can escape the body (failable calls and ném payloads), so a failure inside the block becomes a value instead of propagating. When the success and error types coincide the union cannot tell them apart, and the form is rejected. bẫy claims its spelling only in expression-primary position directly followed by {, so bẫy(…) calls and bare identifier uses keep their ordinary meaning. No bắt clause, trong_khi tail, or early-success form attaches to it — those belong to làm.

vacua is a contextual empty-collection marker (identifier form, not a reserved keyword). Use it with an explicit collection type: hằng lista<numerus> xs ← vacua or hằng tensor<f32, []> t ← vacua.

STRING includes short strings delimited by " and block strings delimited by « and ». '...' (ascii) and backtick ... (forma) are separate literal forms (see String And Template Literals above).

A bare { ... } now produces an object-rooted JSON document of type json: { "name": "Alice", "age": 30, "active": true }. Keys are quoted JSON strings separated by :; values are JSON constants only. Duplicate keys are an error (second occurrence). Ascribing to tabula<K,V> lowers a real constant map. Use ↦ valor for explicit widening to the broad dynamic carrier. Genus/variant construction Type { field = expr } uses the Faber = grammar unchanged. Construction literals do not spread: rải is not a field initializer (Genus { rải other } is rejected). rải stays for list literals and call arguments. Copy-with-changes is planned as Genus { … } từ source.

• Ratio construction uses ratioType '{' fieldInit (',' fieldInit)* '}' through typedConstructor; every field initializer is named, and the resulting fields remain accessible only by label.

Special Expressions#

khớp_đầu_tiên(source, nơi binder { predicate }) is the dedicated first-match selection expression over a statically bounded source: the predicate is evaluated for every candidate lane (total evaluation, no early exit), the first live match is selected, and a no-match or empty source yields nihil (the result type is T ∪ nihil). The nơi predicate tail is owned by this head and never shares the reduce/scan hằng/biến binder tail. khớp_đầu_tiên claims only the expression-head position immediately followed by (; elsewhere the spelling stays an ordinary identifier. An optional tại coordinate clause binds per-axis indices as in lặp từ.

tổng từ source tại [i] hằng s { trả term } is the sequential sum-reduce over a shaped source: one term per element (trả inside the body yields it) folded into a + accumulator seeded at zero. lớn_nhất từ source [tại [i]] [hoặc_nếu_rỗng identity] and nhỏ_nhất từ … (en max from / min from, with coalesce for hoặc_nếu_rỗng) are the extrema reductions: no binder and no body, and the optional hoặc_nếu_rỗng tail states the caller's identity for an empty source (a statically non-empty source needs none). Each head is claimed only in expression-head position immediately followed by từ; elsewhere the spelling stays an ordinary identifier, so lớn_nhất(a, b) remains a call. The distributed sợi clause of tổng is admitted only inside @ hạt_nhân kernels today. A general reducta thông_qua Op reduction that would retire tổng từ and max from / min from is admitted, not shipped (FLD K3).

văn_bản_hóa and đọc/dòng are builtin claims that resolve to a user binding when the surface spelling is bound in scope (parameter, local, function, or any in-scope definition); otherwise they are the builtin. The same binding-wins rule applies to văn_bản_hóa's paren-claimed form and to the vacua empty-collection marker: builtin claims are defaults, not reservations.

tạo variant construction accepts a qualified variant path (tạo pkg.Bonum { … }), so an imported union's variants construct through the import alias, and the ∷ cast is a full type annotation (∷ pkg.Exitus) exactly as the general postfix ascription (uvf-u3). A { right after a tạo path always opens its field list (empty braces are legal), so a tạo condition or scrutinee cannot be directly followed by a block: nếu tạo A { … } is a parse error, and nếu (tạo A) { … } is the parenthesized form.

∷ remains the general postfix ascription in cast. Rendered text templates (STRING '(' argumentList ')') and captured forma templates (BACKTICK_STRING '(' argumentList ')') use the ordinary call suffix. Regex construction uses the ordinary conversio grammar: `(STRING | ASCII_STRING) '↦' 'regex'`.

Slash-delimited regex literals are not active grammar yet. / lexes as the division operator, while // and /* ... */ are rejected as invalid comments. Use "..." ↦ regex for compiled regex values.

---

Patterns#

---

Diagnostics#

The scribe family (ghi_chú/xem/cảnh_báo/viết — en print/debug/warn/write) claims the statement-initial position only when not immediately followed by (. ghi_chú expr is the output statement; a statement-initial ghi_chú(...) is an expression statement whose callee is the identifier ghi_chú — a user function call, never the intrinsic.

• ghi_chú = neutral diagnostic note, xem = debug/inspect, cảnh_báo = warn
• viết is a diagnostic channel spelling; use current stdlib methods for real output

Comments#

Faber accepts line comments only: # through end of line. The # must be the first non-whitespace token on the logical line (optional leading ASCII spaces or tabs only — other Unicode space separators are not skipped by the lexer). A # that follows any other token on the same line is a lex error with the message # comments must start a line; move this comment above the code.

Valid line-start comments attach forward as leading_trivia on the following statement or declaration (see comment-preservation). # inside string literals, ascii literals, forma templates, and other delimited literals is not a comment.

---

Entry Points#

• bắt_đầu = sync entry, bắt_đầu_bất_đồng_bộ = async entry.
• đối_số binds parsed command-line arguments; thoát supplies the process exit expression. Their order is fixed by entryHeader.

---

Testing#

kiểm_thử modifiers include mong_đợi_thất_bại (en expect_failure): the case passes only when its body escapes through the error channel, and a case that completes cleanly fails (strict expected-failure). The other modifiers are bỏ_qua, việc_cần_làm, chỉ, chỉ_trong, nhãn, thời_gian, đo_lường, lặp_lại, and mong_manh. The counts of thời_gian, lặp_lại and mong_manh are non-negative integer literals; a float is test_modifier_integer.

---

CLI Framework#

CLI metadata uses the ordinary reachable annotation* statementCore grammar. The promoted cli, imperium, optio, and operandus families validate their own named-field schemas after parsing.

Faber supports building CLI applications with automatic argument parsing and help generation.

CLI Entry Point#

@ cli "faber"
@ optio verbose longum "verbose" typus bivalens
incipit argumenta args {
    # CLI framework automatically parses arguments
}

CLI Options and Arguments#

@ imperium "deploy"
@ optio target brevis "t" longum "target" typus textus descriptio "Deployment target"
@ optio verbose brevis "v" longum "verbose" typus bivalens descriptio "Enable verbose output"
@ operandus textus file descriptio "File to deploy"
functio deploy() argumenta args {
    # Arguments automatically parsed and passed
}

---

Capability Calls#

Expression-form gọi is the only supported gọi surface. Legacy typed gọi "route" (args) → T { } and statement-level stream blocks gọi 'route' { meus/tuus … } are rejected at parse time.

The active adExpr production is defined under Primary Expressions. Its ordinary postfix conversio materializes the resulting conversation handle.

• Route: ASCII_STRING ('chỉ:đọc'), not double-quoted STRING.
• Opener: optional single expression → Request data as valor.
• Expression `gọi`: blockless; evaluates to a sermo conversation handle. Use postfix ↦ T (materialization), assign to sermo, or open live directional views: s.meus<T>() (outbound da / fini) and s.tuus<T>() (inbound accipe / cursor / exhauri / fini). Iterate inbound content frames with s.tuus<T>().cursor(), not direct lặp từ s.tuus<T>().
• Removed (parse error): legacy typed gọi "route" and block meus/tuus arms.
• Types: compiler-owned scrinium, status; opaque sermo conversation handle.
• English reader spellings: sermo is channel, scrinium is frame, and the views meus<T> / tuus<T> are send<T> / recv<T> (s.send<T>(), s.recv<T>()). The Latin spellings are unchanged.
• sermo ↦ T materializes inbound frames into one value of type T using the type-directed collector for T.
• `sermo<O, R>` (D6.11, D6.12). A conversation carries its types: O is what the caller sends (the opener; nihil when the call sends none) and R is each item frame back. sermo (en channel) takes zero or exactly two type arguments — bare sermo means sermo<valor, valor>, the same rule as bare numerus meaning i64 (any other argument count is sermo_arity). For a route served by a Faber @ gọi handler visible to the caller's module (its own handlers plus its imports), the compiler fills O/R from that handler's own signature — its one parameter (or nihil) and its item type; every other route (a host route, or a handler outside that visibility) keeps bare sermo. s.tuus<T>(), s.meus<T>(), and postfix ↦ T are checked against, or infer, O/R. sermo<O, R> assigns to bare sermo; the reverse is an error. The type arguments are compile-time only — the wire is unchanged, and frames still carry loose data.

See docs/design/frame-stream-types.md.

Concurrency is conversations. Concurrent work is an gọi conversation with a route. There is no separate spawn, thread, or lock primitive family. Handlers that share nothing and exchange only frames are free of data races by construction.

Every gọi pays the conversation cost. It goes through the router with frames, even when both ends are local; there is no hidden fast path. The light path is an ordinary function call, and a swappable light path is a contract passed as a parameter.

gọi is the effect boundary. Effects reach the outside world through gọi conversations, which stay portable across backends.

@ gọi on a function is the compiler-owned serving half of gọi: it lets Faber code answer a route. @ gọi 'prefix:name' (en @ call) on a top-level, non-generic, bodied hàm serves that route.

• Routes are exact: prefix:name or prefix/name. Pattern routes are deferred.
• The annotation must be followed — directly, or after further stacked annotations — by a hàm; before any other declaration it is a parse error (ad_annotation_requires_functio), and it is never a kiểu member, hợp_nhất field or giao_ước method annotation.
• The handler takes zero or one parameter; the one parameter is the opener value of the calling gọi.
• A handler serves one route. Reserved prefixes (such as runtime:) and builtin routes cannot be served.
• Routes form one program-wide static table built from every module in the program, including imported libraries. Two definitions of the same route are a compile error.
• Parsing, checking, and the route table exist today; serving is implemented on Rust, Go, TypeScript, and the MIR runner.

Web, HTTP, and framework routing stay libraries (see Annotations).

---

Collection Operations#

The former khoảng collection pipeline DSL is retired. Collection filtering, slicing, and aggregation are expressed through ordinary textus/lista/tabula/copia methods and closures instead of a grammar-level query expression. textus, numerus, fractus, lista<T>, tabula<K,V>, and copia<T> are compiler-owned core types; their method surfaces are not Norma declarations.

prima and ultima are ordinary method names, not transform keywords. nơi is the owned predicate-tail introducer of the khớp_đầu_tiên first-match expression (see Special Expressions), not collection syntax.

ordina(key) (D1.7) sorts a lista in place by a key selector; ordinata(key) returns a new sorted lista and leaves the receiver untouched. The zero-argument forms ordina() / ordinata() sort by the element's natural order. Both are a stable sort. The key selector's result must be a number or textus; other key types are rejected.

từ is used for iteration (lặp từ items hằng x) and imports (nhập từ "path").

Iteration coordinates (tại)#

The optional tại coordinate clause names the index a loop is walking. The en reader spelling is "at": lặp từ grid tại [r, c] reads as iterating grid at coordinates [r, c].

• `lista` (D3.1): one name binds the element's position (lặp từ items tại [i] hằng v).
• `tabula` (D3.1-D3.3): one name binds the entry's key (lặp từ m tại [k] hằng v); a composite-key tabula<bộ<K1, …, Kn>, V> takes N names, one per part of the bộ key, in declared part order.
• Tensor / matrix: as before — one name per axis, first name = outermost axis, and later names walk successively inner axes; arity must equal rank (fewer or more names is a structured reject).
• No index surface, no `tại`. copia, cursors, generators, textus, and sparsa have no index to name; tại on any of them is a structured reject (itera_apud_requires_indexed_iterable), not a silent no-op.
• `tại` requires `từ`. The coordinate clause is only valid on lặp từ (element iteration); lặp khoảng range loops and lặp ra reject it.
• The coordinate names are immutable index bindings scoped to the loop body, distinct from the element binder that follows the clause.

Composite-key index (D3.2, D3.3). The same bracket-list shape indexes a composite key outside a loop, too: on a tabula<bộ<K1, …, Kn>, V>, m[[k1, …, kn]] reads or writes the entry keyed by that bộ — an ordinary index expression, not a distinct production. A bracket list of the wrong part count or part type falls through to the ordinary map-index type-mismatch report.

Hashable keys and elements (D3.4). A tabula key or copia element must be hashable: no fractus of any width (NaN breaks equality; ±0 hash apart on some targets), no mutable collection (lista, tabula, copia, and the other reference collections), no valor/json/regex. bộ, kiểu, and hợp_nhất keys/elements are hashable when every part is. A non-hashable map key is tabula_key_not_hashable; a non-hashable set element is copia_element_not_hashable. See Loops for map/set iteration order.

---

Fac Block#

• làm { ... } is the explicit do block and executes its body once.
• làm { ... } trong_khi condition is the post-test loop form; postfix trong_khi attaches only to làm, not arbitrary preceding blocks.
• bắt is an attachment shared by several structured forms, not a semantic mode owned by làm. A plain làm is often used when an otherwise unattached block needs a local handler: làm { ... } bắt err { ... }.

---

Admitted, Not Shipped#

These are ruled or admitted for the language and are not accepted by the compiler today. None of them is a production of the grammar above, and the live parser rejects each one.

---

Target Support#

Target support is not part of the grammar — this file defines only the language. For which grammar each compilation target lowers, and the runtime policy around it, see:

• EBNF_MATRIX.md — generated grammar×target lowerability matrix (the official rows).
• docs/design/target-capability-matrix.md — runtime/contract policy (erase/warn/defer), pipeline routing, per-target contracts.

Conditional compilation is package-granular. A package's faber.toml declares its target or targets ([build] target = "ts", or targets = ["rust", "ts"]). There are no conditionals inside a package: no #if, no in-body cfg, and no per-file target selection.

A multi-target package stays target-neutral. Its per-target parts live in the per-target manifest sections ([target.ts]). Code that needs a genuinely different implementation per target is split into separate packages, and the consumer chooses one.

Feature flags (@ feature, [features]) belong to the visibility model and are unchanged. @ nondum stays the marker for "not implemented on this target yet".

There is no unsafe. Faber code is always checked. Code that must step outside the checker is foreign code, written outside Faber.

---

Critical Syntax Rules#

1. Type-first parameters: hàm f(numerus x) NOT hàm f(x: numerus)
2. Type-first declarations: hằng textus name NOT hằng name: textus
3. Iteration loops: lặp từ/ra collection hằng/biến item { } or lặp khoảng range hằng/biến item { } (verb-first, source, then binding)
4. Parentheses around conditions are valid but not idiomatic: prefer nếu x ≻ 0 { } or nếu flag ≡ đúng { } over nếu (x ≻ 0) { }
5. Scribe-family keywords claim statement-initial position only when not followed by `(` — ghi_chú x is the output statement; a statement-initial ghi_chú(x) is a call to the identifier ghi_chú