Language reference

This page covers Gale’s syntax and supported language features. Use it to write modules, define types and functions, and work with Elixir and OTP. For the formal typing rules, inference procedure, and BEAM representation, read the type system.

Gale source files use .gale or .🌀. A project may use either extension, but must not contain both extensions for the same module. The supported toolchain is Elixir 1.20 on OTP 28 or newer.

Module structure

Every file declares one module. Library module names must equal the Mix app name or begin with that name followed by a dot.

mod shop.orders

@moduledoc "Order operations."

alias gale_std.result
alias shop.customer as customer

pub type Status = Pending | Paid | Cancelled(reason: String)

pub fn label(status: Status) -> String {
  case status {
    Pending -> "pending"
    Paid -> "paid"
    Cancelled(reason) -> reason
  }
}

The header order is mod, optional @moduledoc, aliases, behaviour declarations or implementations, and an optional struct block. Types and functions follow in any order. All names are private unless marked pub.

The following forms appear at module scope. Square brackets indicate optional syntax; do not write the brackets:

Form	Purpose
mod path.name	Declare the file’s module
alias path.name	Refer to the module as name
alias path.name as short	Choose a local module name
[pub] fn name(...) -> Type { ... }	Define a function
[pub] type Name = ...	Define an alias or algebraic data type
[pub] opaque type Name = ...	Hide a type’s representation from other modules
[pub] extern "Module.fun" name(...) -> Type	Declare a typed foreign function
[pub] extern type Name	Declare a foreign nominal type
[pub] extern struct "Module" Name { fields }	Bind a native Elixir struct to a Gale type
[pub] extern exception "Module" Name { ... }	Model an Elixir exception
declares Behaviour<...>	Declare a Gale behaviour
extern "Module" declares Behaviour<...>	Type an existing BEAM behaviour
implements Behaviour<...> as name	Implement and name a capability
extern mod "Module" name	Declare a native module value

Use snake case for modules, functions, and bindings. Type and constructor names start with an uppercase letter. Predicate names may end in ?.

Comments and documentation

Line comments begin with #. Documentation attaches to the declaration that follows it:

@moduledoc """
Utilities for customer names.
"""

@typedoc "A normalized customer name."
pub opaque type Name = String

@doc "Builds a checked name."
pub fn name(value: String) -> Result<Name, :empty> { ... }

Here, ... stands for an omitted function body; it is not Gale syntax. @moduledoc must immediately follow mod. Use @typedoc before a type and @doc before a function, extern, callback, or exception.

Types

Built-in types

Type	Meaning
Integer, Float	Separate numeric types; operators never mix them implicitly
String	UTF-8 text; a subtype of Binary
Binary	Arbitrary bytes
Atom, :ready	Any atom, or one literal atom
Boolean	true | false
Term	Any BEAM value; decode or refine before use
Never	No possible value
List<A>	A linked list containing A
Map<K, V>	A map with keys K and values V
{A, B} and {}	Tuples and the empty tuple
%{name: String}	An exact record with fixed atom keys
fn(A) -> B	A function value
fn() receives M -> A	A function allowed to receive mailbox type M
Pid<M>, AnyPid	A typed process and a non-sendable process reference
Option<A>	Some(A) | None
Result<A, E>	Ok(A) | Error(E)

Join alternatives with |, for example :open | :closed or Integer | :infinity. Generic type parameters use angle brackets.

Aliases and algebraic data types

A type alias gives another name to a type. An algebraic data type declares a closed set of constructors:

pub type UserId = Integer

pub type Tree<A> =
  | Leaf
  | Node(A, Tree<A>, Tree<A>)

Constructors without fields, such as Leaf, are values. Constructors with fields are called like functions: Node(1, Leaf, Leaf). ADTs may be recursive.

Constructor result annotations support reply-indexed protocols:

pub type Request<Reply> =
  | Count : Request<Integer>
  | Rename(name: String) : Request<:ok>

Records, structs, maps, and opaque types

Records are structural and exact. A value with an extra field is a different record type.

user = %{name: "Ada", age: 36}
older = %{user | age: user.age + 1}
name = user.name

A struct is a named type owned by its module and appears in the module header:

mod shop.user

struct {
  name: String,
  active: Boolean = true
}

pub fn new(name: String) -> User {
  %User{name: name}
}

Use %{key => value} for maps whose keys are determined at runtime. %{} is an empty map. Exact records are compatible with Map<K, V> when every atom key fits K and every field value fits V. Use opaque type to hide a representation outside its defining module:

pub opaque type AccountId = Integer

Functions and bindings

Every named function annotates all parameters and its result. Functions may be declared in any order and may call themselves recursively.

pub fn add<A>(item: A, items: List<A>) -> List<A> {
  [item | items]
}

count: Integer = 3
doubled = fn(value: Integer) -> value * 2

Bindings are immutable and lexically scoped. A later binding may shadow an earlier name. Add : Type before = when an explicit local annotation helps; the compiler reports an error if the inferred value does not fit it. Lambda parameter types may be omitted when the surrounding function type supplies them.

Pipelines insert the value as the first argument:

items |> list.map(transform) |> list.take(10)

Values and literals

Gale supports decimal integers and floats, including digit separators: 1_000, -12, and 3.14. There are no hexadecimal, octal, binary, or exponent literals.

Strings support interpolation and the escapes \", \\, \n, \t, \r, and \u{...}. Interpolation accepts String, numbers, booleans, and atoms. Convert raw Binary data with gale_std.string.from_binary before inserting it into a string.

greeting = "Hello, #{name}"
lines = ["one", "two"]
pair = {1, "one"}
options = [timeout: 5_000]

List cons syntax is [head | tail]. Keyword entries such as timeout: 5_000 are syntax sugar for the ordinary tuple {:timeout, 5_000}; keyword lists have no special type. A literal atom begins with :. nil is the atom :nil; it is not Option.None.

Control flow

All control-flow forms are expressions and return a value.

if and cond

if always has an else. Conditions must be Boolean.

if ready {
  "ready"
} else {
  "waiting"
}

cond {
  count == 0 -> "empty"
  count < 10 -> "few"
  true -> "many"
}

The final cond condition must be the literal true.

case

case checks its arms from top to bottom. The compiler rejects missing cases and unreachable arms.

case result {
  Ok(value) -> value
  Error(:missing) -> fallback
  Error(:invalid) -> fallback
}

with

with chains Result values. Each <- unwraps Ok; the first Error is returned. The final expression is wrapped in Ok.

with {
  user <- load_user(id)
  email <- validate_email(user.email)
  email
}

Add else { ... } to handle the combined error type explicitly. Every else arm must return a Result.

Patterns

Patterns appear in bindings, case, with, and receive with different restrictions.

_                         # ignore a value
name                      # bind a value
^expected                 # compare with an existing binding
{left, right}             # tuple
[head | tail]             # non-empty list
%{name: name}             # record
Some(value)               # ADT constructor
"GET " <> rest           # non-empty string prefix

| in a pattern is only the list-tail marker shown above. Use separate arms for alternatives. Bindings and with require patterns that cannot fail. Refutable patterns belong in case or receive.

An arm may add a guard:

value when is_integer(value) -> value
level when level in [:debug, :info] -> level

Guards allow literals, variables, field access, comparisons, boolean operators, selected type tests, and literal-list in. They cannot call arbitrary functions. Type-test guards refine a Term or union inside the arm.

The guard-safe built-ins are is_atom, is_binary, is_boolean, is_float, is_integer, is_list, is_map, is_nil, is_number, is_pid, is_reference, is_tuple, is_function, byte_size, map_size, is_map_key, map_get, length, hd, tl, tuple_size, elem, min, max, round, trunc, and abs.

Operators

Operators	Use
+ - *, unary -	Integer arithmetic; unary - also accepts Float
integer.div, integer.rem	Checked integer division and remainder returning Result
<>	String or binary concatenation
++	List concatenation
== !=	Strict equality between related types
< <= > >=	Ordering between compatible numeric or binary types
and or not	Boolean logic
|>	Pass a value as the first function argument

Numeric operators do not mix Integer and Float. Equality requires related operand types and remains strict. Generic equality uses an explicit bound: fn same<A: Eq>(left: A, right: A). Eq is built in and cannot overload the operator. Every instantiation must satisfy the bound. Narrow Term values before comparing or pinning them, including terms stored in collections or records; Term does not satisfy Eq. There is no raw term-comparison API or coercing equality spelling. Use gale_std.integer.div and gale_std.integer.rem for integer division and remainder and handle their Result values.

Floats use finite BEAM binary64 values. Strict equality distinguishes 0.0 from -0.0, including inside containers; numerical ordering does not. Binary Float arithmetic operators are rejected because BEAM overflow and zero division can raise. Use gale_std.float.add, subtract, multiply, or divide, which return Result<Float, gale_std.number.ArithmeticError>. No operation implicitly promises exact real arithmetic. Verification treats Float ordering branches as reported, unconstrained values so unrelated invariants can still be proved. Numerical Float claims are outside the proof language and are rejected.

Use gale_std.list.subtract(left, right) for list subtraction.

Processes and mailboxes

A function that uses receive declares its mailbox with receives. Typed PIDs carry the message type accepted by process.send.

pub type Message = Ping(Pid<:pong>) | Stop

fn loop() receives Message -> :ok {
  receive {
    Ping(reply_to) -> {
      process.send(reply_to, :pong)
      loop()
    }
    Stop -> :ok
  }
}

receive must cover the mailbox type. An optional after timeout -> value clause adds a timeout; the timeout is an Integer in milliseconds or :infinity. Pins work in receive patterns and compile to native BEAM selective receive patterns. Monitor and linked-process events use dedicated arms:

receive {
  Reply(value) -> value
  down(monitor) event -> handle_down(event)
  exit(trap_exit) event -> handle_exit(event)
  after 5_000 -> fallback
}

Elixir and library interop

Declare an Elixir function at a typed boundary with extern:

pub extern "String.trim" trim(value: String) -> String

pub extern "String.to_integer" to_integer(value: String) -> Integer
raises ArgumentError

The compiler trusts the signature. raises E converts the declared exception and returns Result<Success, E>; other exceptions and exits keep their native behaviour. Gale generates ordinary Elixir modules, functions, structs, specs, and OTP callbacks.

An extern type is nominal. An extern struct binds a native Elixir struct to a Gale type with declared fields and boundary checks. An extern exception names an Elixir exception struct and may be used by raises. An extern mod is a module value and exposes only the behaviour capabilities named by its implements clauses. See the Externs chapter for examples.

Behaviours

Declare a behaviour with callback signatures:

mod storage

declares Store<K, V>

callback get(data: Map<K, V>, key: K) -> Option<V>
optional callback close() -> :ok

Implement it in another module:

implements storage.Store<String, Integer> as store

The compiler checks every required callback and any optional callbacks you provide. A mod storage.Store<K, V> value lets a caller accept an implementation explicitly and call its available callbacks. OTP behaviours use the same mechanism through gale_std.

Gale performs no global implementation lookup. Pass a mod Behaviour<...> value or a function when generic code needs an implementation.

Contracts and proof annotations

Functions can state requires { ... } and ensures { ... } between their return type and body. Predicates return Boolean; ensures also binds result to the return value. Opaque types with a representation can declare invariant(value) { ... } immediately after the representation.

pub opaque type State = %{reserved: Integer, capacity: Integer}
invariant(state) {
  state.reserved >= 0 and state.reserved <= state.capacity
}

pub fn available(state: State) -> Integer
ensures { result >= 0 }
{
  state.capacity - state.reserved
}

assert { predicate } and proof { ... } are erased statements followed by a continuation expression. A proof block returns :ok. spec fn and lemma fn declare erased, effect-free helpers; lemmas return :ok and state at least one postcondition. Executable code cannot call or capture these helpers. Existing runtime calls to gale_std.test.assert remain unchanged.

decreases { integer_expression } supplies a measure for well-founded Gale recursion. Specification functions, lemmas, and generated default helpers must terminate. Defaults must be effect-free; use explicit factory functions for effectful initialization.

Compilation checks annotation types, scope, effect restrictions, and erasure; it does not establish invariants, assertions, contracts, or termination. gale check typechecks a project without emitting Elixir or running solvers. gale verify (and mix gale.verify) proves the written contracts with Why3 and Z3. The proving tour walks through a complete example. Successful units are reused from .gale/proofs. Extern requires/ensures are trusted as written: callers prove preconditions, inhabit the return type, and assume postconditions. Proofs cover Gale code that returns normally. They do not imply process survival or message delivery. Unsupported operations fail explicitly. Predicates and proof blocks cannot perform effects.

Reserved words

mod alias as implements declares pub fn type struct opaque extern
exception raises receives case if cond with else receive after when
requires ensures invariant decreases spec lemma assert proof
true false nil and or not in

Gale also reserves Elixir special forms and definition macros that generated code relies on, including for, import, quote, require, try, def, and defmodule. See the complete reserved-word rules.

What Gale does not include

Gale has no macros, protocols, implicit conversions, implicit truthiness, exceptions as a language construct, try/rescue, comprehensions, bitstring syntax, mutable bindings, function overloading by type, or default parameters. Model foreign features with typed externs and ordinary Gale functions.

For the precise rules behind inference, subtyping, exhaustiveness, runtime checks, and emitted Elixir, continue to the type system.