AsyncRattus.Primitives

The language primitives of Async Rattus. Note that the typing rules for delay, adv,select and box are more restrictive than the Haskell types that are indicated. The stricter Async Rattus typing rules for these primitives are given below.

Documentation

data O a

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.

Instances

Producer p a => Producer (O p) a

Defined in AsyncRattus.Channels

Methods

getCurrent :: O p -> Maybe' a

getNext :: O p -> (forall q. Producer q a => O q -> b) -> b

data Box a

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.

Instances

Producer p a => Producer (Box p) a

Defined in AsyncRattus.Channels

Methods

getCurrent :: Box p -> Maybe' a

getNext :: Box p -> (forall q. Producer q a => O q -> b) -> b

data Select a b

The return type of the select primitive.

Constructors

Fst !a !(O b)

Snd !(O a) !b

Both !a !b

delay :: a -> O a

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 θ.

adv :: O a -> a

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).

box :: a -> Box a

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.

unbox :: Box a -> a

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

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

select :: O a -> O b -> Select a b

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.

never :: O a

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.

class Stable 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.