Skip to content


Subversion checkout URL

You can clone with
Download ZIP
ECMAScript back end for Functional Reactive Programming in Agda
tree: aadb8dd385


An implementation of Functional Reactive Programming for building HTML
applications in Agda.

To build and application, start with an HTML file:

      <title>Hello World</title>
      <script data-main="agda.frp.main" src="require.js"></script>
      <h1>A greeting</h1>
      <p class="agda" data-agda="Demo.Hello"></p>

This is just a regular old HTML file, which loads the agda.frp.main
JavaScript module (using require.js, but any AMD-compliant JavaScript
module loader should work). The important part is:

  <p class="agda" data-agda="Demo.Hello"></p>

The "agda" class and data-agda attribute indicates that an Agda program
should be executed inside the annotated node.

Now write an Agda program:

  open import FRP.JS.Behaviour using ( Beh ; [_] )
  open import FRP.JS.DOM using ( DOM ; text )
  open import FRP.JS.RSet using ( ⟦_⟧ )

  module Demo.Hello where
  main : ∀ {w} → ⟦ Beh (DOM w) ⟧
  main = text ["Hello, world."]

This program creates a text node whose content is always "Hello, World."

Compile (using the darcs snapshot of Agda 2.2.11):

  agda --js Demo/Hello.agda

this will create a bunch of js files such as jAgda.Demo.Hello.js.

Put all the .js files (including require.js and the agda.frp.*.js
files) in the same directory as hello.html.

Load hello.html in a browser, and enjoy.

There are unit tests in FRP.JS.Test, which link against John Resig's
QUnit ( To run the tests, first "make tests",
then load build/tests.html in a browser.

Something went wrong with that request. Please try again.