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
- defaultPromote :: Continuous a => a -> Box a
- class Continuous p where
- progressInternal :: InputValue -> p -> p
- promoteInternal :: p -> Box p
- data ContinuousData where
- ContinuousData :: Continuous a => !(Weak (IORef a)) -> ContinuousData
- promoteStore :: IORef [ContinuousData]
- progressPromoteStoreMutex :: MVar ()
- progressPromoteStoreAtomic :: InputValue -> IO ()
- progressPromoteStore :: InputValue -> IO ()
- promote :: Continuous a => a -> Box a
- newtype Chan a = Chan InputChannelIdentifier
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.
This is the eliminator for the "stable" modality Box
:
Γ ⊢ t :: Box 𝜏 ------------------ Γ ⊢ unbox t :: 𝜏
defaultPromote :: Continuous a => a -> Box a Source #
class Continuous p where Source #
progressInternal :: InputValue -> p -> p Source #
promoteInternal :: p -> Box p Source #
Instances
Stable a => Continuous a Source # | |
Defined in AsyncRattus.InternalPrimitives progressInternal :: InputValue -> a -> a Source # promoteInternal :: a -> Box a Source # | |
Continuous a => Continuous (Sig a) Source # | |
Defined in AsyncRattus.Signal progressInternal :: InputValue -> Sig a -> Sig a Source # | |
Continuous a => Continuous (List a) Source # | |
Defined in AsyncRattus.Strict progressInternal :: InputValue -> List a -> List a Source # | |
Continuous a => Continuous (Maybe' a) Source # | |
Defined in AsyncRattus.Strict progressInternal :: InputValue -> Maybe' a -> Maybe' a Source # | |
(Continuous a, Continuous b) => Continuous (a :* b) Source # | |
Defined in AsyncRattus.Strict progressInternal :: InputValue -> (a :* b) -> a :* b Source # |
data ContinuousData where Source #
ContinuousData :: Continuous a => !(Weak (IORef a)) -> ContinuousData |
progressPromoteStoreMutex :: MVar () Source #
progressPromoteStoreAtomic :: InputValue -> IO () Source #
Atomic version of progressPromoteStore
.
progressPromoteStore :: InputValue -> IO () Source #
For promote to work, its argument must be stored in the "promote
store", and whenenver an input is received on some channel, all
values in the "promote store" must be advanced (using
progressInternal
).
promote :: Continuous a => a -> Box a Source #