Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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
This is the constructor for the "later" modality O
:
Γ ✓ ⊢ t :: 𝜏 -------------------- Γ ⊢ delay t :: O 𝜏
This is the eliminator for the "later" modality O
:
Γ ⊢ t :: O 𝜏 --------------------- Γ ✓ Γ' ⊢ adv t :: 𝜏
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.
This is the eliminator for the "stable" modality Box
:
Γ ⊢ t :: Box 𝜏 ------------------ Γ ⊢ unbox t :: 𝜏
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
.