BiGUL: The Bidirectional Generic Update Language

Putback-based bidirectional programming allows the programmer to write only one putback transformation, from which the unique corresponding forward transformation is derived for free. BiGUL, short for the Bidirectional Generic Update Language, is designed to be a minimalist putback-based bidirectional programming language. Originally developed in the dependently typed programming language Agda, BiGUL’s well-behavedness has been completely formally verified. It has subsequently been ported to Haskell for developing various bidirectional applications.

The module Generics.BiGUL.Lib.HuStudies (haddock documentation on Hackage) contains some small, illustrative examples of BiGUL programs, and is a good place for getting started quickly.

For more detail, see the following tutorial:

There is also an earlier paper describing the reification technique used in the Agda formalisation:

This paper uses an outdated version of BiGUL, but the reification technique still underlies the current formalisation.


BiGUL works with GHC 7.10 and above, and is released to Hackage, so the installation of the latest release of BiGUL is as simple as executing

cabal update
cabal install BiGUL

in the command line (i.e., the standard way of installing Haskell packages).

The most recent development version (with changes not yet released to Hackage) is maintained in the master branch. To install the development version, first clone this git repository, and then invoke cabal install under the Haskell/ subdirectory of the local copy of the repository:

git clone
cd BiGUL/Haskell/
cabal update
cabal install