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:
{-# 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.