Heh

Heh is a functional programming language with a built-in support for infinite arrays. The language is strict, but the infinite structures are lazy. The language includes three built-in higher-order constructs: imap, reduce and filter which make it possible to construct complex array operations that can be often seen in APL or SaC.

One of the main distinctive features of the language is that we use ordinals to index arrays as well as to maintain shapes of the arrays. This gives a rise to a number of important static properties that one can observe in Heh.

Heh makes it possible to write generic programs that do not make distinction between arrays and streams. One can write truly infinity-polymorphic programs:

λa.λv.imap |a| { _(iv): (a iv) + v

Keep in mind, that the increment function never specifies whether the shape of a is finite.

The name Heh refers to the Egyptian mythology, where Heh is the god of infinity.

Results and work in progress

Currently, Heh demonstrates that the concept described in this paper can be implemented. We have formalized semantics of the language here.

We have shown that the number of array equalities from various array algebras hold for infinite arrays as well. As an example, consider drop |a| (a ++ b) == b, where a and b are of infinite shape, ++ is concatenation over the first axis and drop is an inverse of ++.

There is a backend that compiles programs with non-recursive finite imaps can into SaC. See sac backend for more details.

Further we have explored Heh compilation into Python, APL, Julia and C in this paper.

We explore how to bring the power of recursive imaps into a strict language. We found a neat way to do this, making sure that parallel execution of such recursively specified arrays is possible. See this paper for more details.

Currently we are working on:

• Designing a type system for Heh. The main challenge is to keep the type system decidable, yet propagate as much of the shape information as possible. Knowing shapes of all the arrays statically vastly improves the runtime. Currently we are investigating whether the SaC approach of combining sub-typing and intersection types is powerful enough. Alternatively, dependent types offer a solution, but they do have potential impact on the performace. The excalt treatment ordinals within the type system is not yet clear.

• Compiling Heh. So far compilation works for a finite non-recursive subset. Infinite recursive case is more challenging. We didn't fix representation for imaps at runtime. Most likely we want to treat them as hash-tables, where every entry stores a contiguous piece of memory, representing an index subspace.

  Memory management is fun. SaC uses reference counting, which is efficient in the strict and finite array scenario. Here, as imaps can be infinite and recursive, most likely we'd have to combine reference counting and garbage collection.

• Proving programs in Heh. Heh treats infinite structures without using co-induction. It uses transfinite induction instead. Can we use this to take and advantage over co-inductive data structures is not yet clear.

• Streaming primitives. We have seen that a number of streaming primitives can be implemented in Heh right now. Whether it is sufficient for all the streaming scenarios is not clear. Also, we didn't properly investigate how to treat finite streams.

The above list is not exhaustive, and a number of open question still remain. In case you are interested in joining to research around Heh, please contact Artem Shinkarov. We are open for collaboration.

Building the interpreter

The following dependencies are required:

• Ocaml version >= 4.3;
• ocamlbuild
• oUnit if you wan to run unittests

To build the interpreter run make within the top-level directory which by default creates main.native (the interpreter) and test.native (unit tests).

Building the interpreter without unit tests can be acheived by make main.native.

Running the interpreter

An interpreter reads a file and executes the program. Consider an example:

$ echo "2 + 2" | ./main.native /dev/stdin
2 + 2
res: p3 = 4
$ echo "(imap [omega] {[0] <= iv < [omega]: iv.[0]).[42]" > /tmp/x.heh
$ ./main.native /tmp/x.heh
((imap [ω]|[] { [0] <= iv < [ω]: (((iv).([0])))).([42]))
res: p14 = 42

The output contains:

1. the text of a program
2. the resulting pointer and value of the evaluated program.

The interpreter comes with a few flags, which description is available via ./main/native --help.

The interpreter comes with a number of examples available in the examples directory.

Testing

The unit tests can be run as follows ./test.native.

This repository uses travis continuous integration. See .travis.yml file for more details.

Syntax hilighting

Heh comes with a syntax highlighting description for Vim. Copy vim/heh.vim into ~/.vim/syntax to make use of it.