Evaluation semantics

A program runs by evaluating an expression, and every form Expressions lists is evaluated by a rule below. Two properties decide almost all of them. Evaluation is strict: a subexpression is evaluated when it is reached, not when its value is demanded. And it is pure: evaluating an expression produces a value and has no other consequence.

Not implemented: the compiler turns a module into JavaScript text, but writes that text nowhere and runs none of it, so an expect=ok block here is a program the type checker accepted and nothing holds it to the value a rule below says it has. GEN-1 is the ticket.

Two outcomes

Evaluating an expression either produces a value or does not terminate. There is no third outcome: no exception, no crash, no undefined result. Nothing in the language throws, so nothing in it catches.

That is a promise about a well-typed program, and it is kept by pushing every failure somewhere earlier or somewhere else:

What would otherwise fail	Where it goes instead
A `case` with no branch for the value	Coverage is checked, so no such `case` compiles
A name that is not in scope	Name resolution
Applying a value that is not a function	Type checking
Integer division by zero	Defined below to be `0`, because no `Int` value means no answer
A lookup, a parse, a conversion that can fail	The type: `Maybe a`, `Result e a`
A companion that throws, or returns a value of the wrong shape	The `Task`'s payload: `Result Failure a`

Known gap: coverage is not checked — the exhaustiveness phase inspects nothing and accepts every module — so a case missing a branch compiles today and would have no value to produce. LANG-19 is the ticket.

That is a claim about evaluating an expression. A whole program has one more outcome, because a program has a boundary and an expression does not: see When a program aborts.

Evaluation is strict

An argument is a value before the function it is passed to is entered, and it is evaluated whether or not the body ever mentions it.

expect=ok

module Example exposing ()

first a b =
  a

loop n =
  loop n

stuck =
  first 1 (loop 2)

first ignores its second argument, and stuck still has no value: loop 2 is evaluated before first is entered, and it does not terminate.

if and case are the exception; see Conditional evaluation, below.

Order of evaluation

Subexpressions are evaluated left to right, in the order they are written.

An application evaluates the function expression first, then each argument in source order, and applies last.

expect=ok

module Example exposing ()

infix left 6 (+) = add

add a b =
  a

g x =
  x

h x =
  x

f a b =
  g a + h b

g a + h b is add (g a) (h b), so add is evaluated, then g a, then h b, and then the application happens. Precedence and associativity decide how an expression groups; they never decide what runs first.

The same rule covers every other form that holds more than one subexpression: a tuple evaluates its elements left to right, an if evaluates its condition before either arm, and a case evaluates its scrutinee before any branch is tried.

Because evaluation is pure, the order is observable only through non-termination: it settles which of two diverging subexpressions hangs the program.

Conditional evaluation

if evaluates its condition, then exactly one of its arms. case evaluates its scrutinee, then tries its branches in the order written and evaluates the body of the first one that matches.

These are the only two forms in the language that evaluate one subexpression and not another.

Nothing short-circuits

&& and || are names, bound by an infix declaration to ordinary functions. Both operands of && are evaluated, always, and likewise for ||.

expect=ok

module Example exposing ()

type Bool
  = True
  | False

infix right 3 (&&) = and

and a b =
  if a then b else False

safe a b =
  a && b

and's body uses if, so the body looks at b only when a is True. Conditional evaluation is a property of the call site, and && is a call.

Skipping the right operand is written out:

expect=ok

module Example exposing ()

type Bool
  = True
  | False

expensive n =
  expensive n

careful a n =
  if a then expensive n else False

&& gets no exception: an operator's meaning is its infix declaration and nothing else, and no signature can defer a parameter.

Known gap: std/core's (&&) and (||) are documented as short-circuiting. LANG-36 is the ticket. No block holds it to account: the claim is in a doc comment, and the JavaScript behind those two operators already takes both operands evaluated.

Bindings

A binding with no parameters is evaluated once

A top-level binding that names no parameters is evaluated once, before the program runs, and every reference to it is that one value. Such bindings are evaluated in dependency order: one is evaluated after everything it depends on. A declaration depends on every top-level declaration its body mentions, on every one those declarations' bodies mention, and so on, through functions as well as through other bindings.

expect=ok

module Example exposing ()

type Colour
  = Red
  | Green

base =
  Red

shifted =
  other base

other c =
  case c of
    Red ->
      Green

    Green ->
      Red

shifted mentions base, so base is evaluated first, whichever order the two are written in. A dependency can also run through a function:

expect=ok

module Example exposing ()

type Colour
  = Red
  | Green

start =
  flip Red

flip c =
  case c of
    Red ->
      fallback

    Green ->
      Red

fallback =
  Green

start mentions only flip, but flip's body mentions fallback, so start depends on fallback and fallback is evaluated first.

Declarations are unordered as text; this is the one place the language puts an order on them, and it reads it off the references.

A binding that does name parameters is not evaluated at initialisation at all. Its value is the function, and its body runs when the function is applied.

A binding may not depend on itself

Under strict evaluation a parameterless binding's value has to exist before the binding can be used. A parameterless binding that depends on itself is an error, whether the cycle is one binding long or runs through several declarations.

expect=canonical-error:SelfDependency

module Example exposing ()

x =
  x

a = b beside b = a is rejected the same way: the cycle runs through two bindings, and neither has a value the other can use. So is a cycle that runs through a function:

expect=canonical-error:SelfDependency

module Example exposing ()

type Colour
  = Red
  | Green

start =
  flip Red

flip c =
  case c of
    Red ->
      start

    Green ->
      Red

start depends on flip, and flip's body mentions start, so start depends on itself. The rule reads mentions, not applications: a binding depends on a function it mentions whether or not evaluating the binding applies it.

A cycle of functions only is not an error. A function may call itself, and two functions may call each other, because neither body runs until the function is applied:

expect=ok

module Example exposing ()

type Bool
  = True
  | False

type Nat
  = Zero
  | Succ Nat

isEven n =
  case n of
    Zero ->
      True

    Succ m ->
      isOdd m

isOdd n =
  case n of
    Zero ->
      False

    Succ m ->
      isEven m

`let` follows the same rule

expect=unimplemented

module Example exposing (f)

f n =
  let
    doubled =
      add n n

    quadrupled =
      add doubled doubled
  in
  quadrupled

Not implemented: there is no let production (LANG-33). Its bindings are evaluated when the let is reached, in dependency order, once each — doubled above is computed once and used twice. The bindings of one let are mutually recursive, and the same restriction applies one level down: a cycle among one let's bindings is an error when it holds a binding without parameters.

Function values

A function is a value like any other. It can be an argument, a result, an element of a tuple, and the value of a binding.

Every function takes exactly one argument, and a function of several is one that returns a function (Application), so applying a function to fewer arguments than its type has arrows produces a function value:

expect=ok

module Example exposing ()

type Pair a
  = Pair a a

pair a b =
  Pair a b

pairWithOne =
  pair 1

pairWithOne is a value: the function pair, carrying the argument it has already been given. Nothing of pair's body has run.

A function value carries whatever its body needs from the scope it was built in, which is what makes a partially applied function, a let-bound function, and a lambda work away from where they were written.

A function is not observable except by applying it. It has no identity, no arity that can be asked for, and no equality — see below. Two functions that compute the same results are indistinguishable, and so are two occurrences of the same lambda.

Equality

== is not built into the language. It is an operator, bound to a function, and that function is a member of the Eq class (Type classes). What equality means is therefore a property of each instance.

expect=ok

module Example exposing ()

type Bool
  = True
  | False

infix non 4 (==) = eq

eq a b =
  True

alike a b =
  a == b

What structural equality computes

Every instance std/core declares is structural, and so is a derived instance. Structural equality is defined by the shape of the value:

Two values of a union type are equal when they are the same constructor and their corresponding arguments are equal.
Two tuples are equal when their elements are pairwise equal. They have the same arity by construction, since arity is part of the type.
Two Chars are equal when they are the same character; two Strings when they are the same sequence of characters; two Ints when they are the same number.
Two Floats are compared as IEEE 754 does, which is the one place structural equality does not apply: nan is equal to nothing, itself included, and 0.0 is equal to -0.0.

An instance is free to define something else — equality up to a normal form, say, for a type whose representation has more than one spelling of the same value.

expect=ok

module Example exposing (Colour, alike)

type Colour
  = Red
  | Green

alike : Eq a => a -> a -> Bool
alike a b =
  eq a b

A type asks for the definition above by declaring an instance whose body is derived, and what that yields is the definition Eq's own declaration supplies, not one the compiler holds for a class it recognises.

Functions are not comparable

There is no Eq instance for a function type, and there cannot usefully be one: deciding whether two functions agree on every input is not something a program can do. So f == g is a type error — an unsatisfied constraint, reported where every other unsatisfied constraint is reported.

Ordering

<, <=, > and >= are not built into the language either. Each is an operator bound to a function written over compare, the one member of the Comparable class (Type classes), and compare a b answers LT, EQ or GT. What an ordering means is a property of each instance.

What the standard library's instances compute

Two Ints are ordered as numbers.
Two Chars are ordered by code point: 'Z' comes before 'a', and '\u{E000}' before '\u{1F600}'.
Two Strings are ordered lexicographically. The first position at which they differ decides, by the code points of the two characters there, and a string that another begins with comes first, so "" comes before every other string.
Two tuples are ordered lexicographically, element by element, and two Positions by where their constructors are declared. Both are what a derived instance computes.
Two Floats are ordered as IEEE 754 orders them, with 0.0 and -0.0 answering EQ. A nan is ordered against nothing.

A Char is a Unicode scalar value, and its code point is all an ordering reads. No locale takes part and nothing is normalised: "\u{E9}" and "e\u{301}" spell one letter with different code points, so they are two strings, unequal, and the second comes first.

The order is the same on every compilation target, including one whose own string comparison reads UTF-16 units and would place '\u{1F600}' before '\u{E000}'.

compare a b is EQ exactly when a == b, in every instance std/core declares.

A `nan` is ordered against nothing

<, <=, > and >= are each False when either side is a nan, a nan against itself included. compare answers GT for a pair holding a nan on either side. a < b and a <= b read compare a b, a > b and a >= b read compare b a, and GT is the one answer all four read as False.

compare is therefore not antisymmetric on a nan: compare nan 1.5, compare 1.5 nan and compare nan nan are all GT. Every function written over compare inherits that:

min x y and max x y answer y when either argument is a nan. min nan 1.5 is 1.5, and min 1.5 nan is nan.
clamp low high x answers x when x is a nan, and a bound that is a nan bounds nothing.
A nan inside a tuple, or inside a value of a type whose instance is derived, decides only when the walk reaches it. (1.0, nan) < (2.0, nan) is True, the first elements having decided; (nan, 1) < (nan, 2) is False.

A program that needs one answer whichever side a nan is on tests with isNaN before comparing.

Recursion and tail calls

Recursion is the only way to iterate. There is no loop form, and there is nothing to mutate that a loop would use.

A self tail call runs in constant stack. A call to the enclosing declaration, in tail position, is compiled as a jump back to the top of that declaration with new arguments, so a recursion written this way may be of any depth.

expect=ok

module Example exposing ()

type Nat
  = Zero
  | Succ Nat

count acc n =
  case n of
    Zero ->
      acc

    Succ m ->
      count (Succ acc) m

An expression is in tail position when its value is the value of the whole declaration body. The body itself is; both arms of an if in tail position are; every branch body of a case in tail position is; and the expression after in of a let in tail position is. Nothing else is — not an argument, not an operand, not a scrutinee, not an if's condition. count (Succ acc) m above is in tail position; Succ (count acc m) would not be, and would use stack proportional to n.

The guarantee covers a call to the declaration the call is written in. Mutual tail recursion between two declarations carries no guarantee.

No rule above says how long an operation takes or how much memory it uses, and nothing here gives one. The promise below is narrower, and needs only one notion of what a value is: a value exists independently of any name bound to it, so binding a second name to one produces a second way to reach it, not a second value.

A value is not copied when it is passed as an argument, returned as a result, bound to a name, or stored inside another value. Binding a large structure to a second name costs nothing beyond the binding itself. A backend that copies a value on assignment does not implement Zelkova.

Not promised: anything about a function value. Applying a function to fewer arguments than its type has arrows produces a function value (Function values), and whether the code generator builds a new one on every such application or reuses one across calls made with the same arguments is left to it entirely. A program whose performance depends on f 1, written inside a loop where f is applied to a constant, not allocating depends on a particular backend, never on the language.

Sharing does not widen the tail-call rule, and names no allocation count for any operation — only that reusing an existing value is free.

Numbers

Int is a 64-bit signed two's-complement integer. Arithmetic wraps: 9223372036854775807 + 1 is -9223372036854775808. The range and the wrapping are the same on every compilation target, so a program computes the same answer wherever it is run.

Float is an IEEE 754 binary64 number, with IEEE's own answers throughout. 1.0 / 0.0 is positive infinity, 0.0 / 0.0 is nan, and the ordering of a nan against anything is False. Nothing about a Float operation is a failure; IEEE defines a result for every one of them, and those results are the language's.

A float literal denotes the binary64 value nearest to the decimal number it spells, rounding to nearest, with ties going to the value whose final mantissa bit is even — the rounding IEEE 754 specifies for every decimal-to-binary conversion. Rounding is total: every literal that Lexical structure accepts denotes some binary64 value, and none is rejected for the value it rounds to. A literal too large in magnitude for any finite binary64 value denotes positive infinity; one too small to be distinguished from zero denotes positive zero. Both are the positive infinity and the positive zero, because a float literal's grammar never places a - before it — a literal is always non-negative — so a negative literal, a negative infinity and a negative zero are all reached the same way any other negative Float is: by prefix negation applied to a non-negative one.

nan has no literal spelling and is reached only through an operation IEEE defines to produce it, such as the 0.0 / 0.0 above. Once reached, nan, the infinities and the negative zero are ordinary Float values: every operation this section defines accepts them and returns IEEE's answer, and structural equality is the one place that answer is not the everyday one.

An operation with no answer

Some operations are handed arguments for which no answer exists: a divisor of zero, the square root of a negative number, the logarithm of a negative one. A well-typed program has only two outcomes and a crash is not one of them, so each of these still produces a value — and which value it produces is decided by what the result type has room for.

A Float-returning operation with no answer produces nan. binary64 keeps a value meaning not a number: nan is not any number, it propagates through every arithmetic operation it reaches, and isNaN detects it. So a Float operation never invents a stand-in answer. sqrt (-1) is nan, logBase 0 0 is nan, 0.0 / 0.0 is nan, and a caller can ask afterwards whether an answer was ever found.

This rule does not reach rounding. An operation whose exact result is too small for binary64 has an answer — the nearest representable value, which is a zero — and returns it, so 1.0e-300 * 1.0e-300 is 0.0 rather than nan, and a literal too small to be distinguished from zero denotes positive zero for the same reason.

Int has no such value. Every 64-bit two's-complement bit pattern is a number somebody might have meant, so whatever an integer operation returns is indistinguishable from a real result, and the language names one:

expect=ok

module Example exposing ()

infix left 7 (//) = idiv

idiv a b =
  a

half n =
  n // 2

n // 0 is 0. modBy 0 n is 0. remainderBy 0 n is 0. These are the values that keep those three operations total. Nothing marks such a zero as invented, so a caller for whom a zero divisor is a real case tests the divisor beforehand, where a Float caller can test the result afterwards.

Converting a `Float` to an `Int`

round, floor, ceiling and truncate each take a Float and produce an Int, and there are Floats the Ints have no room for: nan, both infinities, and every finite value outside the 64-bit range.

A conversion to Int rounds as its name says and then wraps into 64 bits, the way Int arithmetic wraps, and nan and both infinities convert to 0. That zero is the same concession // makes, and for the same reason: the result type has no value meaning no answer, so the conversion returns one that means something else. A program holding a Float it is unsure of tests it with isNaN or isInfinite before converting, as a program holding a divisor tests the divisor.

Purity and the foreign boundary

An expression's value depends only on the values of the names it mentions. Evaluating it twice gives the same value, and evaluating it does nothing else — nothing is written, read, mutated or sent anywhere.

A module foreign facade is where that guarantee meets code the compiler did not produce and cannot inspect. A facade declares an effect by default, and its companion is under no obligation to be a function of anything: reading a clock, keeping a counter, printing and reaching the network are what it is for.

The word unsafe is what claims otherwise. A signature marked with it declares a function rather than an effect, and its author is asserting that the same arguments give the same result and that calling it has no other consequence.

expect=ok

module foreign Core.Math exposing (square)

unsafe square : Float -> Float

Nothing distinguishes that from the same word over an impure export:

expect=ok

module foreign Core.Random exposing (next)

unsafe next : Int -> Int

The second is a broken program, and the rule it breaks is one only its author can keep. What the word buys is not a check but a place to look: the assertions a program makes about foreign code are the declarations carrying it, and a reader who wants to know what this language is trusting reads those.

An unsafe companion also owes the answers Numbers defines: a Float-returning companion with no answer returns nan, an Int-returning one returns the value that section names, and a conversion returns a value the Int type can hold. Nothing checks that either, for the reason nothing checks purity: a type annotation with no body is all the compiler ever sees.

Effects

Everything above describes a computation. A program reaches the outside world by producing a Task: a value describing work, which the runtime performs.

Task is a type zelkova-core declares and exposes without its constructors, so a Task is opaque everywhere but in core — nothing else builds one out of parts or takes one apart. A Task a describes work that produces an a when it is run.

Building a Task performs nothing. An expression whose value is a Task is as pure as any other: evaluating it twice gives the same description twice, and neither evaluation reads a file or writes a byte. The work happens when a Task is run, so the guarantee above holds over a program with effects in it.

Where a `Task` comes from

A primitive Task is declared by a module foreign facade whose result type is one.

expect=unimplemented

module foreign Core.File exposing (read)

import Task exposing (Failure)

read : String -> Task (Result Failure String)

That is the only place an effect enters the language. What the companion behind such a signature returns, and which types the signature may still name, is Foreign interoperability's. Every other Task is built from those, so a package declares its own effects on the same terms zelkova-core declares its.

Sequencing

Task.andThen runs one Task after another, and it is an ordinary function.

expect=fragment

succeed : a -> Task a
map : (a -> b) -> Task a -> Task b
andThen : (a -> Task b) -> Task a -> Task b

andThen f t describes running t, handing its result to f, and running the Task f returns. None of the three is a member of a class: a class is always over a complete type, and Task on its own is not one.

Nothing about Task is built into the language beyond the name and running one. Core writes its sequencing the way any module writes a function over a type it declares, and which shape it picks is core's: a program outside core cannot observe the difference.

Not implemented: zelkova-core exports succeed and map and no andThen (LANG-78).

Running a `Task`

A program hands the runtime one Task, and running the program is running that Task. The value it hands over is main, whose type Packages writes down. Nothing else runs one: a Task a program builds and never gives to the runtime describes work that never happens.

A Task is a value, so sharing reaches it like anything else — binding one to two names gives two ways to reach one description. Running that description twice performs its work twice.

The effects of a Task happen in the order it sequences them: andThen runs the second only once the first has produced a value.

A Task sequences any number of steps in constant stack. A chain of andThens of any length, and a Task that builds the next one by calling itself, run without exhausting the stack, whether or not any step waits. The guarantee covers the sequencing only: a function a step calls uses stack as any other call does, under the tail-call rule.

An effect that can fail

Task takes one type parameter and carries no channel for an error. A failure an effect can produce is a value in its payload, which is where every other failure the language admits goes.

Every effect can produce two of those values whatever else it produces, because a primitive effect is a call into JavaScript and such a call can break in two ways its caller did not ask for. Task declares them, and exposes them with their constructors — the type is matched on rather than held opaque:

expect=ok

module Task exposing (Failure(..))

type Failure
  = Threw String
  | Malformed String

Threw is a companion that threw, or whose promise rejected, carrying the host's description of what happened. Malformed is a companion that returned a value its declared type does not admit, carrying the name of the export that returned it.

So a facade declares a Task (Result Failure a) unless it is marked unsafe, a rule Foreign interoperability states in full. Running such a Task yields a value even when the code behind it breaks, so the two outcomes above are the two outcomes of running one.

A failure belonging to the effect's own domain goes in the payload beside those. read above, reporting a missing file apart from a broken companion, is String -> Task (Result Failure (Result IoError String)). The module that publishes read outside its package is where the two Results collapse into the one its dependents see.

Not implemented: the read block under Where a Task comes from fails at its import Task, because this harness compiles a block against a stand-in Basics and nothing else, and zelkova-core's own Task is not among its interfaces. The block above compiles by naming module Task, which puts it in the core package and gets it the scalar type names — String included — directly rather than through an import zelkova-core does not ship. No facade wrapper is generated, and nothing runs a program at all — the pipeline ends at type checking, so there is no runtime for a Task to be handed to (GEN-1).

When a program aborts

Evaluating an expression has two outcomes. Running a program has a third: it can abort, stopping without producing a value and without running any more of itself.

No Zelkova expression asks for one. The language has no keyword that aborts and none that catches one, so an abort is never a step a program takes — it is the runtime saying it can no longer keep the guarantees above. Three things cause one.

An unsafe facade whose companion breaks its promise. A companion declared as a function that throws, or that returns a value its declared type does not admit, leaves its caller owed a value that nothing produced. An effectful facade has somewhere to put that and an unsafe one has nowhere.

So every abort a program's own code can cause is attributable to a declaration carrying that word.

Exhaustion. No memory left to hold a value, or no stack left to enter a call. The second is reachable from Zelkova alone, by a recursion that neither the tail-call rule nor a Task's sequencing covers.

The host. Whatever runs the program can stop it.

An abort says what caused it, and one caused by a facade names the export whose companion broke.

Only the first is a promise broken. The other two are the runtime running out of what it needs.

Not implemented: a companion that throws does not abort naming its export — the check above runs only over a returned value, so a throw propagates as the companion's own exception instead (GEN-23).

Evaluation semantics

Two outcomes

Evaluation is strict

Order of evaluation

Conditional evaluation

Nothing short-circuits

Bindings

A binding with no parameters is evaluated once

A binding may not depend on itself

let follows the same rule

Function values

Equality

What structural equality computes

Functions are not comparable

Ordering

What the standard library's instances compute

A nan is ordered against nothing

Recursion and tail calls

Sharing

Numbers

An operation with no answer

Converting a Float to an Int

Purity and the foreign boundary

Effects

Where a Task comes from

Sequencing

Running a Task

An effect that can fail

When a program aborts

`let` follows the same rule

A `nan` is ordered against nothing

Converting a `Float` to an `Int`

Where a `Task` comes from

Running a `Task`