AsyncRattus.InternalPrimitives

Documentation

type InputChannelIdentifier = Int

type Clock = IntSet

singletonClock :: InputChannelIdentifier -> Clock

clockUnion :: Clock -> Clock -> Clock

channelMember :: InputChannelIdentifier -> Clock -> Bool

data InputValue where

Constructors

InputValue :: !InputChannelIdentifier -> !a -> InputValue

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.

Constructors

Delay !Clock (InputValue -> a)

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 Select a b

The return type of the select primitive.

Constructors

Fst !a !(O b)

Snd !(O a) !b

Both !a !b

asyncRattusError :: [Char] -> a

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

extractClock :: O a -> Clock

adv' :: O a -> InputValue -> a

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

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.

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

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.

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.

Constructors

Box a

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

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 :: 𝜏