Function Definitions

Function definitions follow Python’s grammar with two mandatory rules: every parameter and the return type must be annotated.

Syntax

function_def ::= [decorator]* ["async"] "def" NAME [type_params] "(" parameters ")" "->" TYPE ":" suite
type_params  ::= "[" type_param ("," type_param)* "]"
type_param   ::= NAME [":" BOUND]
parameters   ::= [param ("," param)*]
param        ::= [("/" | "*")] [NAME ":" TYPE ["=" DEFAULT]]

Examples:

def f(x: int) -> int: ...
def f(x: int, y: int = 0) -> int: ...
def f(x: int, /, y: int, *, z: int) -> int: ...
def f(*args: int, **kwargs: str) -> None: ...
def f[T](xs: list[T]) -> T?: ...
def f[T, U](x: T, f: Callable[[T], U]) -> U: ...
async def g(url: str) -> bytes: ...

Mandatory annotations

Every parameter must have a type annotation; the return type must be present (-> None for void).

def add(a, b): ...               # ❌ tyc::missing_annotation — both params and return type
def add(a: int, b: int): ...     # ❌ tyc::missing_annotation — return type
def add(a: int, b: int) -> int: ...    # ✅

tyc check is unambiguous about both kinds of error.

Default values

The default must match the annotation:

def f(n: int = 0) -> int: ...      # ✅
def f(n: int = "zero") -> int: ...  # ❌ type_mismatch on the default

Nullable parameters

T? does not auto-default to None:

def find(name: str?) -> int?: ...           # caller must pass an arg
def find(name: str? = None) -> int?: ...    # caller may omit

Keyword-only and positional-only

Python’s * and / separators work unchanged:

def connect(host: str, /, *, port: int = 5432, ssl: bool = True) -> None: ...

connect("localhost", port=5433)         # ✅
connect(host="localhost")               # ❌ host is positional-only
connect("localhost", 5433)              # ❌ port is keyword-only

*args and **kwargs

Each must be annotated — Rule 1 (every parameter annotated) extends to variadic parameters since v0.9.0:

def log_all(*messages: str, **tags: str) -> None:
    # messages: tuple[str, ...]
    # tags:     dict[str, str]
    ...

def trace(f, *args, **kwargs):       # ❌ tyc::missing_annotation on every param
    ...

For genuinely variadic functions (typically generic decorators or **kwargs forwarders), the canonical idiom is object:

def trace[R](f: Callable[..., R], *args: object, **kwargs: object) -> R:
    log(f.__name__, args, kwargs)
    return f(*args, **kwargs)

If you know the shape — say every variadic argument is a str — type it concretely. object is the escape hatch for “really any value”; it is honest about the lack of static knowledge without falling back to the implicit-Any path.

Decorators

Standard Python decorators work:

import functools

@functools.cache
def fib_plain(n: int) -> int: ...

Typhon-specific decorators:

Decorator	Effect
@pure	Asserts the six purity conditions. Erased at emit.
@memo	Adds @functools.cache at desugar (function must be pure-eligible).
@memo(max=N)	@functools.lru_cache(maxsize=N).
@pure(memo=True)	Combined.
@gatherable	Opts into automatic gather rewriting (only fires when [strictness] auto-gather = true).

See @pure and @memo.

Generic type parameters (PEP 695)

def first[T](xs: list[T]) -> T?: ...
def pair[T, U](a: T, b: U) -> tuple[T, U]: ...
def smallest[T: Ordered](xs: list[T]) -> T?: ...

Explicit type instantiation is not supported

def identity[T](x: T) -> T: return x

let y: int = identity[int](7)        # ❌ check-time error since v0.9.0
let y: int = identity(7)             # ✅ T inferred from the argument

Type parameters are always inferred from arguments and the call-site expected type. f[T](args) used to crash at runtime with TypeError: 'function' object is not subscriptable; v0.9.0 fires a clear check-time error pointing users at the inference pattern. See Generics for the full reference.

async def

async def fetch(url: str) -> bytes:
    ...

The checker enforces:

• async def containing no await is a warning (tyc::async_without_await).
• Calling an async def from a sync function without await is a hard error (tyc::missing_await).

Return-path checking (reserved)

Static fall-through analysis is reserved for a future Typhon release. Today the checker validates that every explicit return matches the declared type, but does not flag a function that may exit without returning:

def f() -> int:
    if cond:
        return 1
    # accepted today; future versions will surface this as a hard error

raise counts as an exit at runtime. Prefer exhaustive match over sealed unions for guaranteed full-coverage control flow.

while True: reachability (v0.9.0)

The reachability analyser recognises infinite loops whose body always exits via return / raise on every branch and contains no break. The post-loop point is unreachable, so tyc::missing_return does not fire:

def serve() -> Never:
    while True:
        let req: Request = accept()
        if req.is_quit():
            raise SystemExit
        handle(req)
    # post-loop point is unreachable since v0.9.0 — no fall-through warning

Adding a break anywhere in the body re-enables the fall-through check, so loops that exit cleanly still need a post-loop return.

Lambdas

let double = lambda n: n * 2     # type inferred from context

Lambda parameters and return types are inferred from the call site or assignment target. If the context can’t pin them down, the lambda’s parameters fall back to Any and the inferred type leaks through — promote to a named function with explicit annotations when the binding outlives a single call.

Where next

• Functions (tour) — the teaching page.
• Generics — type parameters.
• @pure and @memo — purity decorators.
• async, await, gather, go — async functions.