Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Time

Time: instants, wall-clock timestamps, durations, and RFC 3339.

Three value types keep the two kinds of clock reading from being confused:

  • Instant is a monotonic reading (nanoseconds from an unspecified origin). Only differences of instants are meaningful; the origin is arbitrary. Use it to measure elapsed time, never to name a point in the calendar. - Wall is a system-clock reading: nanoseconds since the Unix epoch (1970-01-01T00:00:00Z), in UTC. Use it to stamp and format a moment. - Duration is a signed span of nanoseconds, the difference of two readings.

Both readings come from the one Clock capability (declared in Concurrent): mono_clock performs mono_now, wall_clock performs wall_now. Which reading a program actually gets is a property of the installed handler, not of the call site. Concurrent.run_clock serves every Clock op from a virtual counter, so a test’s time is a pure function of its sleeps; run_clock_real here serves the two real reads from the OS clock. Both real reads are recorded capability observations, so a time-reading program replays byte-for-byte.

RFC 3339 formatting and parsing are pure, total, UTC-only string code: no locale, no time zone database (tzdb is a political data blob and belongs in a content-addressed package, not a frozen Std). Timestamps at or after the epoch (non-negative wall readings) are supported.

Types

Duration

type Duration = Duration(Int)

A signed span of time, in nanoseconds.

Instant

type Instant = Instant(Int)

A monotonic clock reading, in nanoseconds from an unspecified origin.

Wall

type Wall = Wall(Int)

A wall-clock reading: nanoseconds since the Unix epoch, in UTC.

Functions and Values

nanos_per_sec

nanos_per_sec : () -> Int

nanos_per_milli

nanos_per_milli : () -> Int

nanos_per_micro

nanos_per_micro : () -> Int

dur_nanos

dur_nanos : (Time.Duration) -> Int

The span in whole nanoseconds.

nanos

nanos : (Int) -> Time.Duration

A duration of n nanoseconds.

micros

micros : (Int) -> Time.Duration

A duration of n microseconds.

millis

millis : (Int) -> Time.Duration

A duration of n milliseconds.

seconds

seconds : (Int) -> Time.Duration

A duration of n seconds.

minutes

minutes : (Int) -> Time.Duration

A duration of n minutes.

hours

hours : (Int) -> Time.Duration

A duration of n hours.

dur_as_secs

dur_as_secs : (Time.Duration) -> Int

The whole-second part of a duration (truncated toward zero).

dur_as_millis

dur_as_millis : (Time.Duration) -> Int

The whole-millisecond part of a duration (truncated toward zero).

dur_add

dur_add : (Time.Duration, Time.Duration) -> Time.Duration

Sum of two durations.

dur_sub

dur_sub : (Time.Duration, Time.Duration) -> Time.Duration

Difference of two durations (a - b).

dur_scale

dur_scale : (Time.Duration, Int) -> Time.Duration

A duration scaled by an integer factor.

dur_negate

dur_negate : (Time.Duration) -> Time.Duration

A duration with the sign flipped.

dur_cmp

dur_cmp : (Time.Duration, Time.Duration) -> Int

Ordering of two durations (-1, 0, 1).

dur_eq

dur_eq : (Time.Duration, Time.Duration) -> Bool

True when the two durations are equal.

instant_nanos

instant_nanos : (Time.Instant) -> Int

The raw monotonic reading in nanoseconds. The absolute value is meaningless across processes; subtract two instants to get an elapsed Duration.

elapsed

elapsed : (Time.Instant, Time.Instant) -> Time.Duration

The span from earlier to later (later - earlier). Named elapsed, not between, to leave the prelude’s numeric between range test unshadowed.

instant_add

instant_add : (Time.Instant, Time.Duration) -> Time.Instant

An instant advanced by a duration.

wall_nanos

wall_nanos : (Time.Wall) -> Int

The reading in nanoseconds since the Unix epoch (UTC).

wall_of_nanos

wall_of_nanos : (Int) -> Time.Wall

A wall reading from nanoseconds since the Unix epoch.

wall_unix_secs

wall_unix_secs : (Time.Wall) -> Int

Whole seconds since the Unix epoch (truncated toward zero).

wall_add

wall_add : (Time.Wall, Time.Duration) -> Time.Wall

A wall reading advanced by a duration.

wall_diff

wall_diff : (Time.Wall, Time.Wall) -> Time.Duration

The span from earlier to later wall readings (later - earlier).

wall_cmp

wall_cmp : (Time.Wall, Time.Wall) -> Int

Ordering of two wall readings (-1, 0, 1).

mono_clock

mono_clock : () -> Time.Instant ! {Concurrent.Clock}

Read the monotonic clock. Deterministic under run_clock, real (and recorded) under run_clock_real.

wall_clock

wall_clock : () -> Time.Wall ! {Concurrent.Clock}

Read the wall clock. Deterministic under run_clock, real (and recorded) under run_clock_real.

run_clock_real

run_clock_real : forall e0 a. (() -> a ! {Concurrent.Clock, IO, e0}) -> a ! {IO, e0}

Run action against the real OS clock. now/sleep still thread a virtual counter (they are the scheduler’s logical time), so this is a superset of run_clock: wall_now and mono_now read the real clock through the prim_* builtins, each a recorded observation, and everything else stays virtual.

format_rfc3339

format_rfc3339 : (Time.Wall) -> String

Format a wall reading as an RFC 3339 timestamp in UTC, e.g. 2026-07-04T12:34:56Z. A nonzero sub-second part is emitted as exactly nine fractional digits (nanoseconds); an exact second emits no fraction. The output is canonical: one reading formats to one string, so timestamps are comparable and hashable as text.

parse_rfc3339

parse_rfc3339 : (String) -> Option(Time.Wall)

Parse an RFC 3339 timestamp to a wall reading in UTC, or None if the string is not a well-formed YYYY-MM-DDTHH:MM:SS[.frac](Z|(+|-)HH:MM). The date/time separators are checked, field ranges are validated, an offset is folded into UTC, and any trailing input is rejected, so the parser is total: a malformed or overlong string is None, never a partial or wrapped value.