std.time

For time: waiting, and two clocks. A C program and a page’s script both have a handler for it. In C, a sleep started in a group of std.reactor’s — a thread’s, under cml’s scheduledWithReactor — is pending while the other threads go on; elsewhere the program waits where it is. (browser.dom has a sleep too: import one of them as.)

The clocks are as precise as the system keeps them: now, the time of day, an Instant (std.instant), which the system may set back or forward; monotonic, a Duration (std.duration) since some time of the system’s own, which only goes forward — so that only the difference of two means anything: what an elapsed time is measured by. A sleep is of a Duration too, to the millisecond, rounded up. What the clocks on a wall say at an instant is std.zoneddatetime’s at, in a zone std.tzdb reads from the system’s files (system, the zone the system is set to): no clock of this module’s.

import co
import std.duration as Duration
import std.io
import std.time

-- | how long a computation took, said after it
timed : {e : HFunctor}
      -> {a : Type}
      -> {{clock : time <: e}}
      -> {{io : stdio <: e}}
      -> Co e a
      -> Co e a
timed c = do
  start <- monotonic
  x <- c
  end <- monotonic
  print ("took " ^ show (end - start))
  pure x

TimeF

data TimeF (m : Type -> Type) x
  = Sleep Int x
  | Now (Int -> x)
  | Monotonic (Int -> x)

time

time : HFunctor

For time: a sleep, the time of day, and a monotonic clock.

sleep

sleep : {e : HFunctor} -> {{ev : time <: e}} -> Duration.Duration -> Co e Unit

Wait: the rest runs when the time has passed, in any effect the time is in, by the evidence — d to the millisecond, rounded up, so never less (of none or less, no wait).

now

now : {e : HFunctor} -> {{ev : time <: e}} -> Co e Instant.Instant

The time of day, as the system has it (which may be set back or forward).

monotonic

monotonic : {e : HFunctor} -> {{ev : time <: e}} -> Co e Duration.Duration

The time since some time of the system’s own, never less than the time before: the difference of two is the time between them.