Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- type InputChannelIdentifier = Int
- type Clock = IntSet
- singletonClock :: InputChannelIdentifier -> Clock
- clockUnion :: Clock -> Clock -> Clock
- channelMember :: InputChannelIdentifier -> Clock -> Bool
- data InputValue where
- InputValue :: !InputChannelIdentifier -> !a -> InputValue
- data O a = Delay !Clock (InputValue -> a)
- data Select a b
- asyncRattusError :: [Char] -> a
- delay :: a -> O a
- extractClock :: O a -> Clock
- adv' :: O a -> InputValue -> a
- adv :: O a -> a
- select :: O a -> O b -> Select a b
- select' :: O a -> O b -> InputValue -> Select a b
- never :: O a
- class Stable a
- data Box a = Box a
- box :: a -> Box a
- unbox :: Box a -> a
Documentation
type InputChannelIdentifier = Int Source #
channelMember :: InputChannelIdentifier -> Clock -> Bool Source #
data InputValue where Source #
InputValue :: !InputChannelIdentifier -> !a -> InputValue |
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
.
Delay !Clock (InputValue -> a) |
The return type of the select
primitive.
asyncRattusError :: [Char] -> a Source #
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 Source #
adv' :: O a -> InputValue -> a Source #
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 Source #
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 typeO 𝜏
, ifcl(s)
ticks beforecl(t)
, - a value of type
𝜏
and a delayed computation of typeO σ
, ifcl(t)
ticks beforecl(s)
, or - a value of type
σ
and a value of type𝜏
, ifcl(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.
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.