Documentation

The "later" type modality. A value v of type O 𝜏 consists of two components: Its clock, denoted cl(v), and a delayed computation that will produce a value of type 𝜏 as soon as the clock cl(v) ticks. The clock cl(v) is only used for type checking and is not directly accessible, whereas the delayed computation is accessible via adv and select.

The return type of the select primitive.

This is the constructor for the "later" modality O:

    Γ ✓θ ⊢ t :: 𝜏
--------------------
 Γ ⊢ delay t :: O 𝜏

The typing rule requires that its argument t typecheck with an additional tick ✓θ of some clock θ.

This is the eliminator for the "later" modality O:

  Γ ⊢ t :: O 𝜏     Γ' tick-free
---------------------------------
    Γ ✓cl(t) Γ' ⊢ adv t :: 𝜏

It requires that a tick ✓θ is in the context whose clock matches exactly the clock of t, i.e. θ = cl(t).

If we want to eliminate more than one delayed computation, i.e. two s :: O σ and t :: O 𝜏, we need to use select instead of just adv.

  Γ ⊢ s :: O σ     Γ ⊢ t :: O 𝜏     Γ' tick-free
--------------------------------------------------
   Γ ✓cl(s)⊔cl(t) Γ' ⊢ select s t :: Select σ 𝜏

It requires that we have a tick ✓θ in the context whose clock matches the union of the clocks of s and t, i.e. θ = cl(s)⊔cl(t). The union of two clocks ticks whenever either of the two clocks ticks, i.e. cl(s)⊔cl(t), whenever cl(s) or cl(t) ticks.

That means there are three possible outcomes, which are reflected in the result type of select s t. A value of Select σ 𝜏 is either

• a value of type σ and a delayed computation of type O 𝜏, if cl(s) ticks before cl(t),
• a value of type 𝜏 and a delayed computation of type O σ, if cl(t) ticks before cl(s), or
• a value of type σ and a value of type 𝜏, if cl(s) and
• cl(s) tick simultaneously.

The clock of never :: O 𝜏 will never tick, i.e. it will never produce a value of type 𝜏. With never we can for example implement the constant signal x ::: never of type Sig a for any x :: a.

A type is Stable if it is a strict type and the later modality O and function types only occur under Box.

For example, these types are stable: Int, Box (a -> b), Box (O Int), Box (Sig a -> Sig b).

But these types are not stable: [Int] (because the list type is not strict), Int -> Int, (function type is not stable), O Int, Sig Int.

The "stable" type modality. A value of type Box a is a time-independent computation that produces a value of type a. Use box and unbox to construct and consume Box-types.

This is the constructor for the "stable" modality Box:

    Γ☐ ⊢ t :: 𝜏
--------------------
 Γ ⊢ box t :: Box 𝜏

where Γ☐ is obtained from Γ by removing all ticks and all variables x :: 𝜏, where 𝜏 is not a stable type.

This is the eliminator for the "stable" modality Box:

  Γ ⊢ t :: Box 𝜏
------------------
 Γ ⊢ unbox t :: 𝜏

Atomic version of progressPromoteStore.

For promote to work, its argument must be stored in the "promote store", and whenenver an input is received on some channel, all values in the "promote store" must be advanced (using progressInternal).