Rattus.Primitives

The language primitives of Rattus. Note that the Rattus types delay, adv, and box are more restrictive that the Haskell types that are indicated. The more stricter Rattus typing rules for these primitives are given. To ensure that your program adheres to these stricter typing rules, use the plugin in Rattus.Plugin so that GHC will check these stricter typing rules.

Documentation

data O a

The "later" type modality. A value of type O a is a computation that produces a value of type a in the next time step. Use delay and adv to construct and consume O-types.

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.

delay :: a -> O a

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

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

adv :: O a -> a

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

    Γ ⊢ t :: O 𝜏
---------------------
 Γ ✓ Γ' ⊢ adv t :: 𝜏

box :: a -> Box a

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

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

where Γ☐ is obtained from Γ by removing ✓ and any 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 :: 𝜏

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 (Str a -> Str b).

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