-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | A modal FRP language
--
-- This library implements the Rattus programming language as an embedded
-- DSL. To this end the library provides a GHC plugin that performs the
-- additional checks that are necessary for Rattus. What follows is a
-- brief introduction to the language and its usage. A more detailed
-- introduction can be found in this paper.
--
-- Rattus is a functional reactive programming (FRP) language that uses
-- modal types to ensure operational properties that are crucial for
-- reactive programs: productivity (in each computation step, the program
-- makes progress), causality (output depends only on current and earlier
-- input), and no implicit space leaks (programs do not implicitly retain
-- memory over time).
--
-- To ensure these properties, Rattus uses the type modality O
-- to express the concept 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 type
-- modality. 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 streams is defined as
--
--
-- data Str a = a ::: (O (Str a))
--
--
-- So the head of the stream is available now, but its tail 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) -> Str a -> Str 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
-- Rattus.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 Rattus programs, one must enable this plugin via the
-- GHC option -fplugin=Rattus.Plugin, e.g. by including the
-- following line in the source file (for better error messages we also
-- suggest using the option -g2):
--
--
-- {-# OPTIONS -fplugin=Rattus.Plugin #-}
--
--
-- In addition, one must annotate the functions that are written in
-- Rattus:
--
--
-- {-# ANN myFunction Rattus #-}
--
--
-- Or annotate the whole module as a Rattus module:
--
--
-- {-# ANN module Rattus #-}
--
--
-- Below is a minimal Rattus program using the Rattus.Stream
-- module for programming with streams:
--
--
-- {-# OPTIONS -fplugin=Rattus.Plugin #-}
--
-- import Rattus
-- import Rattus.Stream
--
-- {-# ANN sums Rattus #-}
-- sums :: Str Int -> Str Int
-- sums = scan (box (+)) 0
--
--
-- The source code of the Rattus.Stream module provides more
-- examples on how to program in Rattus.
@package Rattus
@version 0.2
-- | The plugin to make it all work.
module Rattus.Plugin
-- | Use this to enable Rattus' plugin, either by supplying the option
-- -fplugin=Rattus.Plugin directly to GHC. or by including the
-- following pragma in each source file:
--
--
-- {-# OPTIONS -fplugin=Rattus.Plugin #-}
--
plugin :: Plugin
-- | Use this type to mark a Haskell function definition as a Rattus
-- function:
--
--
-- {-# ANN myFunction Rattus #-}
--
--
-- Or mark a whole module as consisting of Rattus functions only:
--
--
-- {-# ANN module Rattus #-}
--
--
-- If you use the latter option, you can mark exceptions (i.e. functions
-- that should be treated as ordinary Haskell function definitions) as
-- follows:
--
--
-- {-# ANN myFunction NotRattus #-}
--
--
-- By default all 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 #-}
--
data Rattus
Rattus :: Rattus
NotRattus :: Rattus
AllowLazyData :: Rattus
instance GHC.Classes.Eq Rattus.Plugin.Rattus
instance GHC.Show.Show Rattus.Plugin.Rattus
instance Data.Data.Data Rattus.Plugin.Rattus
-- | 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.
module Rattus.Primitives
-- | 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 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
-- | This is the constructor for the "later" modality O:
--
--
-- Γ ✓ ⊢ t :: 𝜏
-- --------------------
-- Γ ⊢ delay t :: O 𝜏
--
delay :: a -> O a
-- | This is the eliminator for the "later" modality O:
--
--
-- Γ ⊢ t :: O 𝜏
-- ---------------------
-- Γ ✓ Γ' ⊢ adv t :: 𝜏
--
adv :: O a -> 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.
box :: a -> Box a
-- | This is the eliminator for the "stable" modality Box:
--
--
-- Γ ⊢ t :: Box 𝜏
-- ------------------
-- Γ ⊢ unbox t :: 𝜏
--
unbox :: Box a -> 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.
class Stable a
-- | This module provides a variant of the standard Arrow type class
-- with a different arr method so that it can be implemented for
-- signal functions in Rattus.
module Rattus.Arrow
-- | Variant of the standard Arrow type class with a different
-- arr method so that it can be implemented for signal functions
-- in Rattus.
class Category a => Arrow a
-- | Lift a function to an arrow. It is here the definition of the
-- Arrow class differs from the standard one. The function to be
-- lifted has to be boxed.
arrBox :: Arrow a => Box (b -> c) -> a b c
-- | Send the first component of the input through the argument arrow, and
-- copy the rest unchanged to the output.
first :: Arrow a => a b c -> a (b, d) (c, d)
-- | A mirror image of first.
--
-- The default definition may be overridden with a more efficient version
-- if desired.
second :: Arrow a => a b c -> a (d, b) (d, c)
-- | Split the input between the two argument arrows and combine their
-- output. Note that this is in general not a functor.
(***) :: Arrow a => a b c -> a b' c' -> a (b, b') (c, c')
-- | Fanout: send the input to both argument arrows and combine their
-- output.
--
-- The default definition may be overridden with a more efficient version
-- if desired.
(&&&) :: Arrow a => a b c -> a b c' -> a b (c, c')
-- | This combinator is subject to the same restrictions as the box
-- primitive of Rattus. That is,
--
--
-- Γ☐ ⊢ t :: b -> c
-- --------------------
-- Γ ⊢ arr t :: a b c
--
--
-- where Γ☐ is obtained from Γ by removing ✓ and any variables x ::
-- 𝜏, where 𝜏 is not a stable type.
arr :: Arrow a => (b -> c) -> a b c
-- | The identity arrow, which plays the role of return in arrow
-- notation.
returnA :: Arrow a => a b b
-- | This module contains strict versions of some standard data structures.
module Rattus.Strict
-- | Strict list type.
data List a
Nil :: List a
(:!) :: !a -> !List a -> List a
infixr 8 :!
-- | Reverse a list.
reverse' :: List a -> List a
-- | Append two lists.
(+++) :: List a -> List a -> List a
-- | Returns Nothing' on an empty list or Just'
-- a where a is the first element of the list.
listToMaybe' :: List a -> Maybe' a
-- | A version of map which can throw out elements. In particular,
-- the function argument returns something of type Maybe'
-- b. If this is Nothing', no element is added on to the
-- result list. If it is Just' b, then b is
-- included in the result list.
mapMaybe' :: (a -> Maybe' b) -> List a -> List b
-- | Strict pair type.
data a :* b
(:*) :: !a -> !b -> (:*) a b
infixr 2 :*
infixr 2 :*
-- | Strict variant of Maybe.
data Maybe' a
Just' :: !a -> Maybe' a
Nothing' :: Maybe' a
-- | takes a default value, a function, and a Maybe' value. If the
-- Maybe' value is Nothing', the function returns the
-- default value. Otherwise, it applies the function to the value inside
-- the Just' and returns the result.
maybe' :: b -> (a -> b) -> Maybe' a -> b
-- | First projection function.
fst' :: (a :* b) -> a
-- | Second projection function.
snd' :: (a :* b) -> b
instance GHC.Float.RealFloat a => Data.VectorSpace.VectorSpace (a Rattus.Strict.:* a) a
instance GHC.Base.Functor ((Rattus.Strict.:*) a)
instance (GHC.Show.Show a, GHC.Show.Show b) => GHC.Show.Show (a Rattus.Strict.:* b)
instance Data.Foldable.Foldable Rattus.Strict.List
instance GHC.Base.Functor Rattus.Strict.List
-- | The bare-bones Rattus language. To program with streams and events,
-- you can use Rattus.Stream and Rattus.Events; to program
-- with Yampa-style signal functions, you can use Rattus.Yampa.
module Rattus
-- | Use this type to mark a Haskell function definition as a Rattus
-- function:
--
--
-- {-# ANN myFunction Rattus #-}
--
--
-- Or mark a whole module as consisting of Rattus functions only:
--
--
-- {-# ANN module Rattus #-}
--
--
-- If you use the latter option, you can mark exceptions (i.e. functions
-- that should be treated as ordinary Haskell function definitions) as
-- follows:
--
--
-- {-# ANN myFunction NotRattus #-}
--
--
-- By default all 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 #-}
--
data Rattus
Rattus :: Rattus
NotRattus :: Rattus
AllowLazyData :: Rattus
-- | Applicative operator for Box.
(|*|) :: Box (a -> b) -> Box a -> Box b
-- | Variant of |*| where the argument is of a stable type..
(|**) :: Stable a => Box (a -> b) -> a -> Box b
-- | Applicative operator for O.
(<*>) :: O (a -> b) -> O a -> O b
-- | Variant of <*> where the argument is of a stable type..
(<**) :: Stable a => O (a -> b) -> a -> O b
-- | Programming with streams.
module Rattus.Stream
-- | Apply a function to each element of a stream.
map :: Box (a -> b) -> Str a -> Str b
-- | Get the first element (= head) of a stream.
hd :: Str a -> a
-- | Get the tail of a stream, i.e. the remainder after removing the first
-- element.
tl :: Str a -> O (Str a)
-- | Construct a stream that has the same given value at each step.
const :: Stable a => a -> Str a
-- | Variant of const that allows any type a as argument as
-- long as it is boxed.
constBox :: Box a -> Str a
-- | Given a value a and a stream as, this function produces a stream that
-- behaves like
shift :: Stable a => a -> Str a -> Str a
-- | Given a list [a1, ..., an] of elements and a stream
-- xs this function constructs a stream that starts with the
-- elements a1, ..., an, and then proceeds as xs. In
-- particular, this means that the ith element of the original stream
-- xs is the (i+n)th element of the new stream. In other words
-- shiftMany behaves like repeatedly applying shift for
-- each element in the list.
shiftMany :: Stable a => List a -> Str a -> Str 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 -> Str a -> Str 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 -> Str a -> Str c
-- | scanMap2 is similar to scanMap but takes two input
-- streams.
scanMap2 :: Stable b => Box (b -> a1 -> a2 -> b) -> Box (b -> c) -> b -> Str a1 -> Str a2 -> Str c
-- | Str a is a stream of values of type a.
data Str a
(:::) :: !a -> O (Str a) -> Str a
-- | Similar to zipWith on Haskell lists.
zipWith :: Box (a -> b -> c) -> Str a -> Str b -> Str c
-- | Similar to zip on Haskell lists.
zip :: Str a -> Str b -> Str (a :* b)
-- | Construct a stream by repeatedly applying a function to a given start
-- element. That is, unfold (box f) x will produce the stream
-- x ::: f x ::: f (f x) ::: ...
unfold :: Stable a => Box (a -> a) -> a -> Str a
-- | Filter out elements from a stream according to a predicate.
filter :: Box (a -> Bool) -> Str a -> Str (Maybe' a)
-- | Calculates an approximation of an integral of the stream of type
-- Str a (the y-axis), where the stream of type Str s
-- provides the distance between measurements (i.e. the distance along
-- the y axis).
integral :: (Stable a, VectorSpace a s) => a -> Str s -> Str a -> Str a
-- | Programming with many-shot events, i.e. events that may occur zero or
-- more times.
module Rattus.Events
-- | Apply a function to the values of the event (every time it occurs).
map :: Box (a -> b) -> Events a -> Events b
-- | An event that will never occur.
never :: Events a
-- | switch s e will behave like s but switches to
-- s'$ every time the event e occurs with some value
-- s'@.
switch :: Str a -> Events (Str a) -> Str a
-- | Like switch but works on stream functions instead of streams.
-- That is, switchTrans s e will behave like s but
-- switches to s'$ every time the event e occurs with some
-- value s'@.
switchTrans :: (Str a -> Str b) -> Events (Str a -> Str b) -> Str a -> Str b
-- | Events are simply streams of Maybe's.
type Events a = Str (Maybe' a)
-- | Trigger an event as every time the given predicate turns true on the
-- given stream. The value of the event is the same as that of the stream
-- at that time.
trigger :: Box (a -> Bool) -> Str a -> Events a
-- | Trigger an event every time the given function produces a Just'
-- value.
triggerMap :: Box (a -> Maybe' b) -> Str a -> Events b
-- | Programming with single shot events, i.e. events that may occur at
-- most once.
module Rattus.Event
-- | Apply a function to the value of the event (if it ever occurs).
map :: Box (a -> b) -> Event a -> Event b
-- | An event that will never occur.
never :: Event a
-- | switch s e will behave like s until the event
-- e occurs with value s', in which case it will behave
-- as s'.
switch :: Str a -> Event (Str a) -> Str a
-- | Like switch but works on stream functions instead of streams.
-- That is, switchTrans s e will behave like s until
-- the event e occurs with value s', in which case it
-- will behave as s'.
switchTrans :: (Str a -> Str b) -> Event (Str a -> Str b) -> Str a -> Str b
-- | Turn a stream of Maybe's into a stream of events. Each such
-- event behaves as if created by firstJust.
whenJust :: Str (Maybe' a) -> Str (Event a)
-- | An event may either occur now or later.
data Event a
Now :: !a -> Event a
Wait :: O (Event a) -> Event a
-- | Synchronise two events. The resulting event occurs after both events
-- have occurred (coinciding with whichever event occurred last.
await :: (Stable a, Stable b) => Event a -> Event b -> Event (a :* b)
-- | Trigger an event as soon as the given predicate turns true on the
-- given stream. The value of the event is the same as that of the stream
-- at that time.
trigger :: Box (a -> Bool) -> Str a -> Event a
-- | Trigger an event as soon as the given function produces a Just'
-- value.
triggerMap :: Box (a -> Maybe' b) -> Str a -> Event b
-- | A simply Yampa-like library for signal functions.
module Rattus.Yampa
-- | Signal functions from inputs of type a to outputs of type
-- b.
data SF a b
-- | The identity signal function that does nothing.
identity :: SF a a
-- | Compose two signal functions.
compose :: SF b c -> SF a b -> SF a c
-- | switch s f behaves like s composed with arr
-- fst until s produces a value of the form Just'
-- c in the second component. From then on it behaves like $f c@.
switch :: SF a (b :* Maybe' c) -> Box (c -> SF a b) -> SF a b
-- | rSwitch s behaves like s, but every time the second
-- input is of the form Just' s' it will change behaviour to
-- s'.
rSwitch :: SF a b -> SF (a :* Maybe' (SF a b)) b
-- | Constant signal function.
constant :: Stable b => b -> SF a b
-- | Loop with an initial value for the signal being fed back.
--
-- Note: The type of loopPre is different from Yampa's as we
-- need the O type here.
loopPre :: c -> SF (a :* c) (b :* O c) -> SF a b
-- | Run a signal function for one step.
stepSF :: SF a b -> DTime -> a -> O (SF a b) :* b
-- | Override initial value of input signal.
initially :: a -> SF a a
-- | Compute the integral of a signal. The first argument is the offset.
integral :: (Stable a, VectorSpace a s) => a -> SF a a
-- | The output at time zero is the first argument, and from that point on
-- it behaves like the signal function passed as second argument.
(-->) :: b -> SF a b -> SF a b
-- | Insert a sample in the output, and from that point on, behave like the
-- given signal function.
--
-- Note: The type of -:> is different from Yampa's: The second
-- argument must be delayed (or boxed).
(-:>) :: b -> O (SF a b) -> SF a b
-- | The input at time zero is the first argument, and from that point on
-- it behaves like the signal function passed as second argument.
(>--) :: a -> SF a b -> SF a b
-- | Apply a function to the first output value at time zero.
(-=>) :: (b -> b) -> SF a b -> SF a b
-- | Apply a function to the first input value at time zero.
(>=-) :: (a -> a) -> SF a b -> SF a b
-- | Precomposition with a pure function.
(^>>) :: Arrow a => Box (b -> c) -> a c d -> a b d
-- | Postcomposition with a pure function.
(>>^) :: Arrow a => a b c -> Box (c -> d) -> a b d
-- | Precomposition with a pure function (right-to-left variant).
(<<^) :: Arrow a => a c d -> Box (b -> c) -> a b d
-- | Postcomposition with a pure function (right-to-left variant).
(^<<) :: Arrow a => Box (c -> d) -> a b c -> a b d
-- | Left-to-right composition
(>>>) :: forall k cat (a :: k) (b :: k) (c :: k). Category cat => cat a b -> cat b c -> cat a c
infixr 1 >>>
instance Control.Category.Category Rattus.Yampa.SF
instance Rattus.Arrow.Arrow Rattus.Yampa.SF
-- | Helper functions to convert streams and signal functions from Rattus
-- into Haskell.
module Rattus.ToHaskell
-- | Turn a stream function into a state machine.
runTransducer :: (Str a -> Str b) -> Trans a b
-- | Turn a signal function into a state machine from inputs of type
-- a and time (since last input) to output of type b.
runSF :: SF a b -> Trans (a, Double) b
-- | Turns a stream into a lazy infinite list.
fromStr :: Str a -> [a]
-- | Turns a lazy infinite list into a stream.
toStr :: [a] -> Str a
-- | A state machine that takes inputs of type a and produces
-- output of type b. In addition to the output of type
-- b the underlying function also returns the new state of the
-- state machine.
data Trans a b
Trans :: (a -> (b, Trans a b)) -> Trans a b