A proto type implementation of a higher-order bidirectional programming language HOBiT.
How to Build
Install the latest GHC ecosystem (including cabal, alex, and happy) first, as HOBiT is implemented in Haskell.
Then, type the following command in the directory where
cabal install --only-dependencies
make just invokes
cabal build and copies the built executable
hobit to the directory.
How to Use
hobit. Then, one will see the following prompt of HOBiT's
You can type expressions to evaluate.
HOBiT> 1 + 2 3
The read-eval-print loop also accepts some commands, where valid
commands are displayed by typing
HOBiT> :h :quit Quit REPL. :load FILEPATH Load a program. :reload Reload the last program. :put EXP [EXP [EXP]] Evaluate a function as "put". :get Exp [Exp] Evaluate a function as "get". :set verbosity INT Set verbosity to the specified number. :help Show this help. :type EXP Show expression's type.
The ":get" and ":put" are most interesting parts of HOBiT's
functionarity. To explain the behavior, we first load the file
HOBiT> :l examples/Unlines.hobit ... unlinesB :: BX [[Char]] -> BX [[Char]] ...
The type construtor "BX" indicates that the values can be updated. To
unlinesB function forward, we just use
HOBiT> :get unlinesB ["a", "b", "c"] "a\nb\nc\n"
:put is used to invoke the backward execution of
HOBiT> :put unlinesB ["a", "b", "c"] "AA\nBB\nCC\n" ... ["AA","BB","CC"] HOBiT> :put unlinesB ["a", "b", "c"] "AA\nBB\n" ... ["AA","BB"] HOBiT> :put unlinesB ["a", "b", "c"] "AA\nBB\nCC\nDD\n" ... ["AA","BB","CC","DD"]
examples contains several examples. Enjoy!
Differences from the Paper
whereclauses are not implemented.
Some arithmetic operators are not implemented (such as
Bidirectional case expressions and let expressions are
We do not have nay direct ways to write bidirectional constructors. Instead, the syntactic notion of the bidirectional context is introduced. Constructors directly occurring in a bidirectional context are automatically promoted to bidirectional ones.
The bidirectional context is explicitly introduced by
|), and implicitly introduced by some expressions (
The bidirectional context is shallow. Arguments of functions are not affected. For example,
(| f  |)is not promoted.
Only constructors propage bidirectional contexts. Thus all the constructors in
(| True :  |)are promoted.
hobit creates the file named
user's home directory.