-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | An asynchronous modal FRP language -- -- This library implements the Async Rattus programming language as an -- embedded DSL. To this end the library provides a GHC plugin that -- checks the stricter typing rules of Async Rattus. What follows is a -- brief introduction to the language and its usage. A more detailed -- introduction can be found in this paper. -- -- Async Rattus is a functional reactive programming (FRP) language that -- uses modal types to express temporal dependencies. In return the -- language will guarantee that programs are productive (in each -- computation step, the program makes progress), causal (output depends -- only on current and earlier input), and have no space leaks (programs -- do not implicitly retain memory over time). -- -- The modal type constructor O (pronounced "later") is used to -- express the passage of time at the type level. Intuitively speaking, a -- value of type O a represents a computation that will produce -- a value of type a in the next time step. Additionally, the -- language also features the Box modal type constructor. A -- value of type Box a is a time-independent computation that -- can be executed at any time to produce a value of type a. -- -- For example, the type of signals is defined as -- --
-- data Sig a = a ::: (O (Sig a)) ---- -- So the current value of the signal is available now, but its future -- state is only available in the next time step. Writing a map -- function for this type of streams, requires us to use the Box -- modality: -- --
-- map :: Box (a -> b) -> Sig a -> Sig b -- map f (x ::: xs) = unbox f x ::: delay (map f (adv xs)) ---- -- This makes sure that the function f that we give to -- map is available at any time in the future. -- -- The core of the language is defined in the module -- AsyncRattus.Primitives. Note that the operations on O -- and Box have non-standard typing rules. Therefore, this -- library provides a compiler plugin that checks these non-standard -- typing rules. To write Async Rattus programs, you must enable this -- plugin via the GHC option -fplugin=AsyncRattus.Plugin, e.g. -- by including the following line in the source file: -- --
-- {-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
--
--
-- Below is a minimal Async Rattus program using the
-- AsyncRattus.Signal module for programming with signals:
--
--
-- {-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
--
-- import AsyncRattus
-- import AsyncRattus.Signal
--
-- sums :: Sig Int -> Sig Int
-- sums = scan (box (+)) 0
--
--
-- The source code of the AsyncRattus.Signal module provides more
-- examples on how to program in Async Rattus. An example project using
-- Async Rattus can be found here.
@package AsyncRattus
@version 0.2
module AsyncRattus.InternalPrimitives
type InputChannelIdentifier = Int
type Clock = IntSet
singletonClock :: InputChannelIdentifier -> Clock
clockUnion :: Clock -> Clock -> Clock
channelMember :: InputChannelIdentifier -> Clock -> Bool
data InputValue
[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.
data O a
Delay :: !Clock -> (InputValue -> a) -> O a
-- | The return type of the select primitive.
data Select a b
Fst :: !a -> !O b -> Select a b
Snd :: !O a -> !b -> Select a b
Both :: !a -> !b -> Select a b
asyncRattusError :: [Char] -> 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 θ. delay :: a -> O a extractClock :: O a -> Clock adv' :: O a -> InputValue -> 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). adv :: O a -> a -- | 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 -- --
-- Γ☐ ⊢ t :: 𝜏 -- -------------------- -- Γ ⊢ box t :: Box 𝜏 ---- -- where Γ☐ is obtained from Γ by removing all ticks and all variables -- x :: 𝜏, where 𝜏 is not a stable type. box :: a -> Box a -- | This is the eliminator for the "stable" modality Box: -- --
-- Γ ⊢ t :: Box 𝜏 -- ------------------ -- Γ ⊢ unbox t :: 𝜏 --unbox :: Box a -> a module AsyncRattus.Plugin.Annotation -- | By default all Async Rattus functions are checked for use of lazy data -- types, since these may cause memory leaks. If any lazy data types are -- used, a warning is issued. These warnings can be disabled by -- annotating the module or the function with AllowLazyData -- --
-- {-# ANN myFunction AllowLazyData #-}
--
-- {-# ANN module AllowLazyData #-}
--
--
-- Async Rattus only allows guarded recursion, i.e. recursive calls must
-- occur in the scope of a tick. Structural recursion over strict data
-- types is safe as well, but is currently not checked. To disable the
-- guarded recursion check, annotate the module or function with
-- AllowRecursion.
--
--
-- {-# ANN myFunction AllowRecursion #-}
--
-- {-# ANN module AllowRecursion #-}
--
data AsyncRattus
AllowLazyData :: AsyncRattus
AllowRecursion :: AsyncRattus
-- | This annotation type is for internal use only.
data InternalAnn
ExpectError :: InternalAnn
ExpectWarning :: InternalAnn
instance GHC.Classes.Eq AsyncRattus.Plugin.Annotation.AsyncRattus
instance GHC.Classes.Ord AsyncRattus.Plugin.Annotation.AsyncRattus
instance GHC.Show.Show AsyncRattus.Plugin.Annotation.AsyncRattus
instance Data.Data.Data AsyncRattus.Plugin.Annotation.AsyncRattus
instance GHC.Classes.Ord AsyncRattus.Plugin.Annotation.InternalAnn
instance GHC.Classes.Eq AsyncRattus.Plugin.Annotation.InternalAnn
instance GHC.Show.Show AsyncRattus.Plugin.Annotation.InternalAnn
instance Data.Data.Data AsyncRattus.Plugin.Annotation.InternalAnn
-- | The plugin to make it all work.
module AsyncRattus.Plugin
-- | Use this to enable Asynchronous Rattus' plugin, either by supplying
-- the option -fplugin=AsyncRattus.Plugin directly to GHC, or by
-- including the following pragma in each source file:
--
--
-- {-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
--
plugin :: Plugin
-- | By default all Async Rattus functions are checked for use of lazy data
-- types, since these may cause memory leaks. If any lazy data types are
-- used, a warning is issued. These warnings can be disabled by
-- annotating the module or the function with AllowLazyData
--
--
-- {-# ANN myFunction AllowLazyData #-}
--
-- {-# ANN module AllowLazyData #-}
--
--
-- Async Rattus only allows guarded recursion, i.e. recursive calls must
-- occur in the scope of a tick. Structural recursion over strict data
-- types is safe as well, but is currently not checked. To disable the
-- guarded recursion check, annotate the module or function with
-- AllowRecursion.
--
--
-- {-# ANN myFunction AllowRecursion #-}
--
-- {-# ANN module AllowRecursion #-}
--
data AsyncRattus
AllowLazyData :: AsyncRattus
AllowRecursion :: AsyncRattus
-- | The language primitives of Async Rattus. Note that the typing rules
-- for delay, adv,select and box are more
-- restrictive than the Haskell types that are indicated. The stricter
-- Async Rattus typing rules for these primitives are given below.
module AsyncRattus.Primitives
-- | 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.
data O 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.
data Box a
-- | The return type of the select primitive.
data Select a b
Fst :: !a -> !O b -> Select a b
Snd :: !O a -> !b -> Select a b
Both :: !a -> !b -> Select a b
-- | 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 θ. delay :: a -> O 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). adv :: O a -> 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. box :: a -> Box a -- | This is the eliminator for the "stable" modality Box: -- --
-- Γ ⊢ t :: Box 𝜏 -- ------------------ -- Γ ⊢ unbox t :: 𝜏 --unbox :: Box a -> a -- | 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 -- --
-- getNext :: p -> (exists q. Producer q a => O q) ---- -- We encode the existential type using continuation-passing style. getNext :: Producer p a => p -> (forall q. Producer q a => O q -> b) -> b instance AsyncRattus.Channels.Producer p a => AsyncRattus.Channels.Producer (AsyncRattus.InternalPrimitives.O p) a instance AsyncRattus.Channels.Producer p a => AsyncRattus.Channels.Producer (AsyncRattus.InternalPrimitives.Box p) a -- | The bare-bones Asynchronous Rattus language. To program with streams, -- you can use AsyncRattus.Stream. module AsyncRattus -- | By default all Async Rattus functions are checked for use of lazy data -- types, since these may cause memory leaks. If any lazy data types are -- used, a warning is issued. These warnings can be disabled by -- annotating the module or the function with AllowLazyData -- --
-- {-# ANN myFunction AllowLazyData #-}
--
-- {-# ANN module AllowLazyData #-}
--
--
-- Async Rattus only allows guarded recursion, i.e. recursive calls must
-- occur in the scope of a tick. Structural recursion over strict data
-- types is safe as well, but is currently not checked. To disable the
-- guarded recursion check, annotate the module or function with
-- AllowRecursion.
--
--
-- {-# ANN myFunction AllowRecursion #-}
--
-- {-# ANN module AllowRecursion #-}
--
data AsyncRattus
AllowLazyData :: AsyncRattus
AllowRecursion :: AsyncRattus
mapO :: Box (a -> b) -> O a -> O b
-- | Programming with signals.
module AsyncRattus.Signal
-- | Apply a function to the value of a signal.
map :: Box (a -> b) -> Sig a -> Sig b
-- | Turn a producer into a signal. This is a variant of mkInput
-- that returns a signal instead of a boxed delayed computation.
mkInputSig :: Producer p a => p -> IO (Box (O (Sig a)))
-- | Variant of getInput that returns a signal instead of a boxed
-- delayed computation.
getInputSig :: IO (Box (O (Sig a)) :* (a -> IO ()))
-- | This function is essentially the composition of filter with
-- map. The signal produced by filterMap f s has the
-- value v whenever s has the value u such
-- that unbox f u = Just' v.
filterMap :: Box (a -> Maybe' b) -> Sig a -> IO (Box (O (Sig b)))
-- | This function is similar to filterMap but takes a delayed
-- signal (type O (Sig a)) as an argument instead of a signal
-- (Sig a).
filterMapAwait :: Box (a -> Maybe' b) -> O (Sig a) -> IO (Box (O (Sig b)))
-- | Filter the given signal using a predicate. The signal produced by
-- filter p s contains only values from s that satisfy
-- the predicate p.
filter :: Box (a -> Bool) -> Sig a -> IO (Box (O (Sig a)))
-- | This function is similar to filter but takes a delayed signal
-- (type O (Sig a)) as an argument instead of a signal (Sig
-- a).
filterAwait :: Box (a -> Bool) -> O (Sig a) -> IO (Box (O (Sig a)))
-- | This function is a variant of zipWith. Whereas zipWith f xs
-- ys produces a new value whenever xs or ys
-- produce a new value, trigger f xs ys only produces a new
-- value when xs produces a new value.
--
-- Example:
--
-- -- xs: 1 2 3 2 -- ys: 1 0 5 2 -- -- zipWith (box (+)) xs ys: 2 3 4 3 8 4 -- trigger (box (+)) xy ys: 2 3 8 4 --trigger :: (Stable a, Stable b) => Box (a -> b -> c) -> Sig a -> Sig b -> IO (Box (Sig c)) -- | This function is similar to trigger but takes a delayed signal -- (type O (Sig a)) as an argument instead of a signal (Sig -- a). triggerAwait :: Stable b => Box (a -> b -> c) -> O (Sig a) -> Sig b -> IO (Box (O (Sig c))) -- | A version of map for delayed signals. mapAwait :: Box (a -> b) -> O (Sig a) -> O (Sig b) -- | This function allows to switch from one signal to another one -- dynamically. The signal defined by switch xs ys first behaves -- like xs, but as soon as ys produces a new value, -- switch xs ys behaves like ys. -- -- Example: -- --
-- xs: 1 2 3 4 5 6 7 8 9 -- ys: 1 2 3 4 5 6 -- -- switch xs ys: 1 2 3 1 2 4 3 4 5 6 --switch :: Sig a -> O (Sig a) -> Sig a -- | This function is similar to switch, but the (future) second -- signal may depend on the last value of the first signal. switchS :: Stable a => Sig a -> O (a -> Sig a) -> Sig a -- | This function is similar to switch but works on delayed signals -- instead of signals. switchAwait :: O (Sig a) -> O (Sig a) -> O (Sig a) -- | This function interleaves two signals producing a new value v -- whenever either input stream produces a new value v. In case -- the input signals produce a new value simultaneously, the function -- argument is used break ties, i.e. to compute the new output value -- based on the two new input values -- -- Example: -- --
-- xs: 1 3 5 3 1 3 -- ys: 0 2 4 -- -- interleave (box (+)) xs ys: 1 3 2 5 7 1 3 --interleave :: Box (a -> a -> a) -> O (Sig a) -> O (Sig a) -> O (Sig a) -- | Turns a boxed delayed computation into a delayed signal. mkSig :: Box (O a) -> O (Sig a) -- | Variant of mkSig that returns a boxed delayed signal mkBoxSig :: Box (O a) -> Box (O (Sig a)) -- | Get the current value of a signal. current :: Sig a -> a -- | Get the future the signal. future :: Sig a -> O (Sig a) -- | Construct a constant signal that never updates. const :: a -> Sig a -- | Similar to Haskell's scanl. -- --
-- scan (box f) x (v1 ::: v2 ::: v3 ::: ... ) == (x `f` v1) ::: ((x `f` v1) `f` v2) ::: ... ---- -- Note: Unlike scanl, scan starts with x f -- v1, not x. scan :: Stable b => Box (b -> a -> b) -> b -> Sig a -> Sig b -- | Like scan, but uses a delayed signal. scanAwait :: Stable b => Box (b -> a -> b) -> b -> O (Sig a) -> Sig b -- | scanMap is a composition of map and scan: -- --
-- scanMap f g x === map g . scan f x --scanMap :: Stable b => Box (b -> a -> b) -> Box (b -> c) -> b -> Sig a -> Sig c -- | Sig a is a stream of values of type a. data Sig a (:::) :: !a -> !O (Sig a) -> Sig a infixr 5 ::: -- | This function is a variant of combines the values of two signals using -- the function argument. zipWith f xs ys produces a new value -- unbox f x y whenever xs or ys produce a new -- value, where x and y are the current values of -- xs and ys, respectively. -- -- Example: -- --
-- xs: 1 2 3 2 -- ys: 1 0 5 2 -- -- zipWith (box (+)) xs ys: 2 3 4 3 8 4 --zipWith :: (Stable a, Stable b) => Box (a -> b -> c) -> Sig a -> Sig b -> Sig c -- | Variant of zipWith with three signals. zipWith3 :: forall a b c d. (Stable a, Stable b, Stable c) => Box (a -> b -> c -> d) -> Sig a -> Sig b -> Sig c -> Sig d -- | This is a special case of zipWith using the tupling function. -- That is, -- --
-- zip = zipWith (box (:*)) --zip :: (Stable a, Stable b) => Sig a -> Sig b -> Sig (a :* b) -- | If-then-else lifted to signals. cond bs xs ys produces a -- stream whose value is taken from xs whenever bs is -- true and from ys otherwise. cond :: Stable a => Sig Bool -> Sig a -> Sig a -> Sig a -- | integral x xs computes the integral of the signal xs -- with the constant x. For example, if xs is the -- velocity of an object, the signal integral 0 xs describes the -- distance travelled by that object. integral :: forall a v. (VectorSpace v a, Eq v, Fractional a, Stable v, Stable a) => v -> Sig v -> Sig v -- | Compute the derivative of a signal. For example, if xs is the -- velocity of an object, the signal derivative xs describes the -- acceleration travelled by that object. derivative :: forall a v. (VectorSpace v a, Eq v, Fractional a, Stable v, Stable a) => Sig v -> Sig v instance AsyncRattus.Channels.Producer (AsyncRattus.Signal.SigMaybe a) a instance AsyncRattus.Channels.Producer (AsyncRattus.Signal.Sig a) a -- | Programming with futures. module AsyncRattus.Future -- | F a will produces a value of type a after zero or -- more ticks of some clocks data F a Now :: !a -> F a Wait :: !O (F a) -> F a -- | SigF a is a signal of values of type a. In contrast -- to Sig, SigF supports the filter and -- filterMap functions. data SigF a (:>:) :: !a -> !O (F (SigF a)) -> SigF a mkSigF :: Box (O a) -> F (SigF a) mkSigF' :: Box (O a) -> O (F (SigF a)) -- | Get the current value of a signal. current :: SigF a -> a -- | Get the future the signal. future :: SigF a -> O (F (SigF a)) bindF :: F a -> Box (a -> F b) -> F b mapF :: Box (a -> b) -> F a -> F b sync :: O (F a) -> O (F b) -> O (F a :* F b) syncF :: (Stable a, Stable b) => F a -> F b -> F (a :* b) switchAwait :: F (SigF a) -> F (SigF a) -> F (SigF a) switch :: SigF a -> F (SigF a) -> SigF a switchS :: Stable a => SigF a -> F (a -> SigF a) -> SigF a filterMap :: Box (a -> Maybe' b) -> SigF a -> F (SigF b) filterMapAwait :: Box (a -> Maybe' b) -> F (SigF a) -> F (SigF b) filterAwait :: Box (a -> Bool) -> F (SigF a) -> F (SigF a) filter :: Box (a -> Bool) -> SigF a -> F (SigF a) trigger :: Stable b => Box (a -> b -> c) -> SigF a -> SigF b -> SigF c triggerAwait :: Stable b => Box (a -> b -> c) -> F (SigF a) -> SigF b -> F (SigF c) map :: Box (a -> b) -> SigF a -> SigF b mapAwait :: Box (a -> b) -> F (SigF a) -> F (SigF b) zipWith :: (Stable a, Stable b) => Box (a -> b -> c) -> SigF a -> SigF b -> SigF c zipWithAwait :: (Stable a, Stable b) => Box (a -> b -> c) -> a -> b -> F (SigF a) -> F (SigF b) -> F (SigF c) fromSig :: Sig a -> SigF a scan :: Stable b => Box (b -> a -> b) -> b -> SigF a -> SigF b scanAwait :: Stable b => Box (b -> a -> b) -> b -> F (SigF a) -> F (SigF b) instance AsyncRattus.Channels.Producer (AsyncRattus.Future.SigF a) a instance AsyncRattus.Channels.Producer (AsyncRattus.Future.OneShot a) a instance AsyncRattus.Channels.Producer p a => AsyncRattus.Channels.Producer (AsyncRattus.Future.F p) a