This document specifies Ephapax (ἐφάπαξ — "once for all"), a dyadic programming language combining:
- Affine types (values used at most once — implicit drop permitted)
- Linear types (values used exactly once — implicit drop is a compile error)
- Region-based memory management (scoped arenas, no GC)
- WASM-first compilation (no garbage collector required)
The dyadic principle: both disciplines coexist at per-binding granularity.
Ephapax's type system has four orthogonal disciplines: L1 region capabilities, L2 structural modality (linear/affine), L3 irreversibility residue (Echo Types — planned), and L4 dyadic interaction mode (project-level declaration). This specification is normative for L1 and L2 and forward-looking for L3 and L4. See docs/vision/EPHAPAX-VISION.adoc for the dyad framing and formal/PRESERVATION-DESIGN.md for the per-layer design.
letter = 'a'..'z' | 'A'..'Z' ;
digit = '0'..'9' ;
alpha_num = letter | digit | '_' ;
hex_digit = digit | 'a'..'f' | 'A'..'F' ;
bin_digit = '0' | '1' ;
oct_digit = '0'..'7' ;whitespace = ' ' | '\t' | '\n' | '\r' ;
line_comment = '//' { any_char - '\n' } '\n' ;
skip = whitespace | line_comment ;lower_ident = ('a'..'z' | '_') { alpha_num } ;
upper_ident = ('A'..'Z') { alpha_num } ;
ident = lower_ident ;
type_ident = upper_ident ;
module_path = upper_ident { '.' upper_ident } ;fn let let! in region
match if else type module
import return true false copy
borrow move drop
+ - * / % == != < > <= >=
&& || ! & @ :: -> => : ;
= | , . .. ( ) { } [ ]
integer = digit { digit | '_' }
| '0x' hex_digit { hex_digit | '_' }
| '0b' bin_digit { bin_digit | '_' }
| '0o' oct_digit { oct_digit | '_' } ;
float = digit { digit } '.' digit { digit }
[ ('e' | 'E') ['+' | '-'] digit { digit } ] ;
boolean = 'true' | 'false' ;
string = '"' { string_char | escape_seq } '"' ;
string_char = any_char - '"' - '\\' ;
escape_seq = '\\' ( 'n' | 'r' | 't' | '\\' | '"' | '\''
| 'x' hex_digit hex_digit
| 'u' '{' hex_digit { hex_digit } '}' ) ;
char = '\'' ( any_char - '\'' - '\\' | escape_seq ) '\'' ;
unit = '(' ')' ;program = { declaration } ;
declaration = fn_decl
| type_decl
| module_decl
| import_decl ;
fn_decl = 'fn' ident [ type_params ] '(' [ params ] ')' '->' type_expr block ;
type_params = '<' type_param { ',' type_param } '>' ;
type_param = upper_ident
| upper_ident ':' upper_ident (* bounded *)
;
params = param { ',' param } ;
param = ident ':' type_expr ;
type_decl = 'type' upper_ident [ type_params ] '=' type_expr ;
module_decl = 'module' module_path block ;
import_decl = 'import' module_path ;expr = let_expr
| let_linear_expr
| region_expr
| if_expr
| match_expr
| lambda_expr
| binary_expr
| call_expr
| borrow_expr
| copy_expr
| block
| literal
| ident
| '(' expr ')' ;
let_expr = 'let' pattern '=' expr [ 'in' expr ]
| 'let' pattern '=' expr ';' expr ;
let_linear_expr = 'let!' pattern '=' expr [ 'in' expr ]
| 'let!' pattern '=' expr ';' expr ;
region_expr = 'region' ident ':' block ;
if_expr = 'if' expr block [ 'else' ( block | if_expr ) ] ;
match_expr = 'match' expr '{' { match_arm } '}' ;
match_arm = pattern '=>' expr [ ',' ] ;
lambda_expr = 'fn' '(' [ params ] ')' [ '->' type_expr ] block
| 'fn' '(' [ params ] ')' [ '->' type_expr ] '=>' expr ;
binary_expr = expr bin_op expr ;
bin_op = '+' | '-' | '*' | '/' | '%'
| '==' | '!=' | '<' | '>' | '<=' | '>='
| '&&' | '||' | '++' ;
call_expr = expr '(' [ args ] ')'
| module_path '.' ident '(' [ args ] ')' ;
args = expr { ',' expr } ;
borrow_expr = '&' expr ;
copy_expr = 'copy' '(' expr ')' ;
block = '{' { stmt } [ expr ] '}' ;
stmt = expr ';'
| let_expr
| let_linear_expr ;(* Region-scoped allocation: value allocated in region r *)
region_alloc = expr '@' ident '(' args ')' ;
(* Example: String.new@r("hello") *)
(* The @r is the region annotation — binds value's lifetime to region r *)pattern = '_' (* wildcard *)
| ident (* variable binding *)
| literal (* literal pattern *)
| upper_ident '(' pattern { ',' pattern } ')' (* constructor *)
| '(' pattern ',' pattern { ',' pattern } ')' (* tuple *)
;type_expr = type_ident (* named type *)
| type_ident '<' type_expr { ',' type_expr } '>' (* generic *)
| '(' type_expr { ',' type_expr } ')' (* tuple *)
| type_expr '->' type_expr (* function *)
| '&' type_expr (* borrow/reference *)
| type_expr '@' ident (* region-scoped type *)
| 'i32' | 'i64' | 'f32' | 'f64' | 'bool' | 'String' | '()' ;Every binding has a qualifier:
- Affine (
let): value may be used at most once. Unused values are implicitly dropped at scope exit. - Linear (
let!): value must be used exactly once. Unused values are a compile-time error.
When an expression has sub-expressions, the typing context is split:
- Linear bindings go to exactly one sub-expression.
- Affine bindings go to at most one sub-expression (may be dropped).
Both branches of if/match must consume the same linear bindings.
The interaction between regions and qualifiers is the core innovation. Three rules govern region exit, and they are orthogonal to qualifiers:
The return type of a region block must not reference the region.
Ty::references_region(r) recursively checks all type constructors:
String, Region, Ref, Fun, Prod, Sum, List, Tuple, Borrow.
This rule is qualifier-independent: it applies identically to affine and linear bindings. One implementation, both modes.
region r:
let s = String.new@r("hello")
s // ERROR: String@r references region r — cannot escape
At region exit, all linear variables bound within the region must have been consumed. Affine variables may be implicitly dropped — the region's arena deallocator frees their memory.
region r:
let! conn = Db.connect@r(...) // linear
let buf = Buffer.new@r(1024) // affine
Db.close(conn) // linear consumed — OK
// buf not consumed — OK (affine, arena handles it)
42
After exit, the region is no longer active. Any attempt to allocate
in it (String.new@r(...)) or reference it is a type error.
The region rules (3.4.1, 3.4.3) never inspect the qualifier. The qualifier rules (3.1, 3.2, 3.3) never inspect the region. They compose without interaction. This means:
- Adding region support doesn't change affine/linear enforcement.
- Changing a binding's qualifier doesn't change region escape checking.
- The region system only needs to be implemented once for both modes.
&x borrows x without consuming it. The borrow's lifetime is bounded
by x's region. Borrows are always read-only.
region r: { ... }creates an arena allocatorr.Foo.new@r(...)allocates inr.- At region exit, all memory in
ris freed in bulk. - Values in
rare inaccessible after exit (enforced by type system).
- A linear binding (
let!) must appear exactly once in the continuation. - If unused: compile error "linear variable not consumed".
- If used twice: compile error "linear variable already consumed".
- An affine binding (
let) may appear at most once. - If unused: silently dropped (weakening rule applies).
- If used twice: compile error "affine variable already consumed".
- Left-to-right evaluation of arguments.
- Eager/strict evaluation (no laziness).
- Block expressions evaluate sequentially; final expression is the result.