HTTPS SSH

HOBiT

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 hobit.cabal locates.

  1. cabal configure
  2. cabal install --only-dependencies
  3. make

The make just invokes cabal build and copies the built executable hobit to the directory.

How to Use

Just run hobit. Then, one will see the following prompt of HOBiT's read-eval-print loop.

HOBiT>

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 :h.

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 ./example/Unlines.hobit.

 HOBiT> :l examples/Unlines.hobit
 ...
 unlinesB :: BX [[Char]] -> BX [[Char]]
 ...

The type construtor "BX" indicates that the values can be updated. To run the unlinesB function forward, we just use :get command.

 HOBiT> :get unlinesB ["a", "b", "c"]
 "a\nb\nc\n"

The command :put is used to invoke the backward execution of unlinesB.

 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"]

The directory examples contains several examples. Enjoy!

Differences from the Paper

  • where clauses are not implemented.

  • Some arithmetic operators are not implemented (such as /=, <, *...).

  • Bidirectional case expressions and let expressions are case* and let*.

  • 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 |), and implicitly introduced by some expressions (case* and let*).

    • The bidirectional context is shallow. Arguments of functions are not affected. For example, [] in (| f [] |) is not promoted.

    • Only constructors propage bidirectional contexts. Thus all the constructors in (| True : [] |) are promoted.

Note

The executable hobit creates the file named .HOBiT_history in user's home directory.