[Agda] Functional Reactive Types

[Alan Jeffrey]

Hi everyone,

A paper about FRP formalized in Agda:

   Functional Reactive Types
   A. S. A. Jeffrey.
   To appear in Proc. EACSL Computer Science Logic /
   IEEE Logic in Computer Science. 2014.
   http://ect.bell-labs.com/who/ajeffrey/papers/lics14.pdf

The summary is that FRP streams of values [v1,v2,...] can naturally 
typed using a stream of types [A1,A2,...] where each vi has type Ai. 
This means that functions on streams of types can be used to give the 
types of functions on streams of values. For example the tail function 
takes a stream [v1,v2,...] of type [A1,A2,...] and gives back the stream 
[v2,v3,...] of type [A2,A3,...] so its type can be considered to be 
(tail : [As] -> [tail(As)]). The paper discusses a minimal FRP library 
(head, tail, cons, induction, and applicative functor) and shows that it 
is enough to type itself, and to define a constructive past-time LTL.

Of particular interest to this mailing list may be the Agda sources 
themselves (http://ect.bell-labs.com/who/ajeffrey/papers/lics14.tgz) 
since they use a collection of LaTeX and Agda trickery to allow the 
paper to be a Literate Agda development where the Agda (hopefully) 
doesn't get in the way too much.

Alan.