Lambda the Ultimate

Golly, how did I never hear of this before?

Flix is a declarative language for specifying and solving fixed-point computations on lattices, such as static program analyses. The syntax and semantics of Flix are inspired by Datalog, but extended to support user-defined lattices and monotone functions. Flix is open-source and available on GitHub.

Static analyzers implemented in general-purpose languages, such as C++ or Java, can be difficult to understand and maintain. A more elegant approach is to express the mutual dependencies of a fixed-point computation in a declarative manner. Thus, there is interest in using a declarative language such as Datalog to implement pointer analyses.

However, Datalog does not support lattices or functions, which limits its expressivity. While it is sometimes possible to work around these limitations, it can be slow and cumbersome. Furthermore, most Datalog implementations have poor integration with existing tools.

Flix allows users to define their own lattices and functions. Rules over relations and lattices are expressed in a logic language with Datalog-like syntax, while functions are written in a pure functional language with Scala-like syntax. The functional language, while small, supports algebraic data types, sets, and pattern matching. Flix also supports interop with JVM languages.

Flix is implemented in Scala, with a standard front-end for parsing, weeding, resolving, and typechecking. The back-end has two components, a solver for the logic language and an interpreter for the functional language. As an initial step to improve performance, we have implemented a bytecode generator to replace the interpreter.