# an ascii plaintext math notation # identifiers, types, and function application use lowercase ascii identifiers with underscores. type annotations follow the form: ``` function_name(arg1: type1, arg2: type2): return_type ``` all operations use explicit prefix calls: ``` contains(set, element) product(type_a, type_b) ``` # function definitions functions are total and context-free. no overloading. no implicit dependencies. ``` function root_group(p: potential): group = find_shallowest(mounted_groups(p)) ``` # struct, module, and traits ``` type group: id: string start_time: time duration: time ``` ``` module potential_mounting: function referenced_groups(p: potential): list = ... function root_group(p: potential): group = ... ``` ``` trait group_homomorphism: function map(x: group_elem): group_elem ``` # lexical scoping allow `let`, `match`, and block structure. ``` potential_analysis: function evaluate_window(p: potential): (time, duration) = let g = root_group(p) in (g.start_time, g.duration) ``` desugaring: ``` match r as t: f1 = ... f2 = ... -> let f1 = r.f1 let f2 = r.f2 ``` # quantification and iteration replace symbolic quantifiers with iteration: ``` for x in domain: ... exists y in domain: ... ``` # indexing and summation arrays are typed functions: ``` a: function(i: int, j: int): real ``` explicit index binding: ``` sum(i: 1..n, a(i, j) * b(j, k)) ``` desugaring: ``` sum(i: 1..n, expr) -> sum(i in range(1, n), expr) ``` ``` a[i][j] -> a(i, j) ``` # function composition and pipelines ``` compose(f, g)(x) -> f(g(x)) ``` ``` pipe(x, f, g) -> g(f(x)) ``` # avoiding point-free style use named expressions: ``` delta(x) = (x, x) pair(x) = (x, f(x)) ``` # operator precedence fully parenthesize: ``` sub(add(1, div(mul(2, pow(c, d)), e)), f) ``` # set comprehension ``` filter(x in domain, condition) -> filter(domain, function(x): condition) ``` # ranges and sequences avoid "...": ``` sequence(n: int): list = map(i: 1..n, i) ``` # algebraic data types tagged sum types: ``` type expr = | number(value: real) | variable(name: string) | binary(op: operator, left: expr, right: expr) ``` # anonymous functions ``` function(x): expr -> lambda_expr(param = x, body = expr) ``` # preconditions and optional types ``` function f(x: t): u precondition: p -> function f(x: t): u? if p then return ``` ``` real? -> optional ``` # predicates and proofs ``` predicate is_prime(n: int): bool proof: exists p in primes: divides(p, n) ``` # safe operations ``` function safe_div(x: real, y: real): real? if y ≠ 0 then return x / y ``` # notation expansion symbolic forms must expand to referential form: ``` notation: "⟨x, y⟩" maps to inner(x, y) ``` # shorthand trait tagging ``` φ: map g -> h where φ is group_homomorphism -> φ: function(x: group_elem): group_elem satisfies group_homomorphism ``` # examples epsilon-delta definition: ``` for epsilon in positive_reals: exists delta in positive_reals: for x in reals: if 0 < abs(x - c) and abs(x - c) < delta: abs(f(x) - l) < epsilon ``` matrix multiplication: ``` c(i, k) = sum(j: 1..n, a(i, j) * b(j, k)) ``` set-builder: ``` filter(x in naturals, exists y in naturals: y * y = x) ``` inner product: ``` inner(x: vector, y: vector): scalar = sum(i: 1..n, x(i) * y(i)) ``` pointwise equality: ``` functions_equal(f, g, domain) = for x in domain: f(x) = g(x) ``` # minimal core - function application - type definitions - lexical blocks - iteration - conditionals - lambda expressions - primitive data and operators all other forms desugar to these.