Functions and lambdas

Functions are tulam’s main unit of computation. Named functions, anonymous lambdas, methods, effect operations, and many desugared forms share the same parameter-and-result model.

Named functions

function add(x:Int, y:Int) : Int = x + y;
function square(x:Int) : Int = x * x;

Parameters are an n-ary telescope, not a compiler-generated chain of unary or binary pairs. The call mirrors the declaration:

add(20, 22)

Annotations may be inferred when unambiguous, but public declarations should normally state their contract.

Anonymous functions

fn(x) = x + 1
fn(x:Int, y:Int) : Int = x + y
fn(item) = match | Nothing -> 0 | Just * value -> value

fn creates a function value without giving it a top-level name. It can capture lexical values:

function makeAdder(amount:Int) : Int -> Int =
    fn(item:Int) : Int = item + amount;

Captured values remain part of the closure’s checked environment.

Higher-order functions

function applyTwice(f:Int -> Int, item:Int) : Int =
    f(f(item));

value result = applyTwice(fn(x:Int) : Int = x + 3, 10);

Functions may be passed and returned like other values. The type Int -> Int is right-associative; A -> B -> C means A -> (B -> C).

Type parameters

Square brackets introduce implicit parameters:

function id[a:Type](item:a) : a = item;

At id(42), checking infers a = Int. Type-only implicit parameters are normally erased at runtime, while retained value parameters remain ordinary runtime inputs.

Universal annotations express the same general idea as an implicit Pi binder:

forall a. a -> a

Constraints

function equal[a:Type](left:a, right:a) : Bool
    requires Eq(a) = left == right;

requires asks for coherent evidence after type and value substitution. A call fails statically when evidence is missing or ambiguous. Multiple constraints are comma-separated.

The canonical declaration order is result type, requires, then an optional placement clause:

function calculate(x:a) : a
    requires Field(a)
    on compute = ...;

Placement is declaration metadata, not part of the function type. General placement planning remains incomplete; ordinary calls never acquire call-site target syntax.

Application and recursion

Application uses parentheses and binds more tightly than infix operators:

f(x, y)
f(x) + g(y)

Runtime recursion is available:

function factorial(n:Int) : Int =
    if n <= 1 then 1 else n * factorial(n - 1);

Definitions used during type checking must satisfy the required termination rules. General runtime recursion does not automatically become type-level computation.

Functions and effects

A pure function returns a; an effectful function returns Eff { ... } a. Actions are convenient sequencing syntax, but the effect row remains part of the contract.

Common mistakes

• Parentheses contain one n-ary argument telescope; they do not imply currying.
• Put requires after the result type and before on.
• Do not add call-site placement syntax to an ordinary function call.

Recap

Functions use explicit n-ary parameters, lambdas are ordinary function values, implicit binders provide polymorphism, and requires makes extra capabilities precise.

Normative details: Language Reference §7.