| Flix | |
| Paradigm: | Multi-paradigm |
| Developer: | Aarhus University, open-source contributors |
| Typing: | inferred, static, strong, structural |
| Platform: | JVM |
| License: | Apache License 2.0.[1] |
| Influenced By: | F#, Go, Haskell, OCaml, Scala |
Flix is a functional, imperative, and logic programming language developed at Aarhus University, with funding from the Independent Research Fund Denmark,[2] and by a community of open source contributors.[3] The Flix language supports algebraic data types, pattern matching, parametric polymorphism, currying, higher-order functions, extensible records,[4] channel and process-based concurrency, and tail call elimination. Two notable features of Flix are its type and effect system[5] and its support for first-class Datalog constraints.[6]
The Flix type and effect system supports Hindley-Milner-style type inference. The system separates pure and impure code: if an expression is typed as pure then it cannot produce an effect at run-time. Higher-order functions can enforce that they are given pure (or impure) function arguments. The type and effect system supports effect polymorphism[7] [8] which means that the effect of a higher-order function may depend on the effect(s) of its argument(s).
Flix supports Datalog programs as first-class values. A Datalog program value, i.e. a collection of Datalog facts and rules, can be passed to and returned from functions, stored in data structures, and composed with other Datalog program values. The minimal model of a Datalog program value can be computed and is itself a Datalog program value. In this way, Flix can be viewed as a meta programming language for Datalog. Flix supports stratified negation and the Flix compiler ensures stratification at compile-time.[9] Flix also supports an enriched form of Datalog constraints where predicates are given lattice semantics.[10] [11] [12] [13]
Flix is a programming language in the ML-family of languages. Its type and effect system is based on Hindley-Milner with several extensions, including row polymorphism and Boolean unification. The syntax of Flix is inspired by Scala and uses short keywords and curly braces. Flix supports uniform function call syntax which allows a function call f(x, y, z) to be written as x.f(y, z). The concurrency model of Flix is inspired by Go and based on channels and processes. A process is a light-weight thread that does not share (mutable) memory with another process. Processes communicate over channels which are bounded or unbounded queues of immutable messages.
While many programming languages support a mixture of functional and imperative programming, the Flix type and effect system tracks the purity of every expression making it possible to write parts of a Flix program in a purely functional style with purity enforced by the effect system.
Flix programs compile to JVM bytecode and are executable on the Java Virtual Machine (JVM).[14] The Flix compiler performs whole program compilation, eliminates polymorphism via monomorphization,[15] and uses tree shaking to remove unreachable code.Monomorphization avoids boxing of primitive values at the cost of longer compilation times and larger executable binaries. Flix has some support for interoperability with programs written in Java.[16]
Flix supports tail call elimination which ensures that function calls in tail position never consume stack space and hence cannot cause the call stack to overflow.[17] Since the JVM instruction set lacks explicit support for tail calls, such calls are emulated using a form of reusable stack frames.[18] Support for tail call elimination is important since all iteration in Flix is expressed through recursion.
The Flix compiler disallows most forms of unused or redundant code, including: unused local variables, unused functions, unused formal parameters, unused type parameters, and unused type declarations, such unused constructs are reported as compiler errors.[19] Variable shadowing is also disallowed. The stated rationale is that unused or redundant code is often correlated with erroneous code[20]
A Visual Studio Code extension for Flix is available.[21] The extension is based on the Language Server Protocol, a common interface between IDEs and compilers being developed by Microsoft.
Flix is open source software available under the Apache 2.0 License.
The following program prints "Hello World!" when compiled and executed:
The type and effect signature of the main function specifies that it has no parameters, returns a value of type Unit, and that the function is impure. The main function is impure because it invokes printLine which is impure.
The following program fragment declares an algebraic data type (ADT) named Shape:
The ADT has three constructors: Circle, Square, and Rectangle.
The following program fragment uses pattern matching to destruct a Shape value:
The following program fragment defines a higher-order function named twice that when given a function f from Int to Int returns a function that applies f to its input two times:
We can use the function twice as follows:
Here the call to twice(x -> x + 1) returns a function that will increment its argument two times. Thus the result of the whole expression is 0 + 1 + 1 = 2.
The following program fragment illustrates a polymorphic function that maps a function f: a -> b over a list of elements of type a returning a list of elements of type b:
The map function recursively traverses the list l and applies f to each element constructing a new list.
Flix supports type parameter elision hence it is not required that the type parameters a and b are explicitly introduced.
The following program fragment shows how to construct a record with two fields x and y:
Flix uses row polymorphism to type records. The sum function below takes a record that has x and y fields (and possibly other fields) and returns the sum of the two fields:
The following are all valid calls to the sum function:
The Flix type and effect system separates pure and impure expressions.[5] [22] [23] A pure expression is guaranteed to be referentially transparent. A pure function always returns the same value when given the same argument(s) and cannot have any (observable) side-effects.
For example, the following expression is of type Int and is Pure:
whereas the following expression is Impure:
A higher-order function can specify that a function argument must be pure, impure, or that it is effect polymorphic.
For example, the definition of Set.exists requires that its function argument f is pure:
The requirement that f must be pure ensures that implementation details do not leak. For example, since f is pure it cannot be used to determine in what order the elements of the set are traversed. If f was impure such details could leak, e.g. by passing a function that also prints the current element, revealing the internal element order inside the set.
A higher-order function can also require that a function is impure.
For example, the definition of List.foreach requires that its function argument f is impure:
The requirement that f must be impure ensures that the code makes sense: It would be meaningless to call List.foreach with a pure function since it always returns Unit.
The type and effect is sound, but not complete. That is, if a function is pure then it cannot cause an effect, whereas if a function is impure then it may, but not necessarily, cause an effect. For example, the following expression is impure even though it cannot produce an effect at run-time:
A higher-order function can also be effect polymorphic: its effect(s) can depend on its argument(s).
For example, the standard library definition of List.map is effect polymorphic:[24]
The List.map function takes a function f from elements of type a to b with effect e. The effect of the map function is itself e. Consequently, if List.map is invoked with a pure function then the entire expression is pure whereas if it is invoked with an impure function then the entire expression is impure. It is effect polymorphic.
A higher-order function that takes multiple function arguments may combine their effects.
For example, the standard library definition of forward function composition >> is pure if both its function arguments are pure:[25]
The type and effect signature can be understood as follows: The >> function takes two function arguments: f with effect e1 and g with effect e2. The effect of >> is effect polymorphic in the conjunction of e1 and e2. If both are pure (their effect is true) then the overall expression is pure (true). Otherwise it is impure.
The type and effect system allows arbitrary boolean expressions to control the purity of function arguments.
For example, it is possible to express a higher-order function h that accepts two function arguments f and g of which at most one is impure:
If h is called with a function argument f which is impure (false) then the second argument must be pure (true). Conversely, if f is pure (true) then g may be pure (true) or impure (false). It is a compile-time error to call h with two impure functions.
The type and effect system can be used to ensure that statement expressions are useful, i.e. that if an expression or function is evaluated and its result is discarded then it must have a side-effect. For example, compiling the program fragment below:
causes a compiler error:
>> Useless expression: It has no side-effect(s) and its result is discarded.
2 | List.map(x -> 2 * x, 1 :: 2 :: Nil); ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ useless expression.
because it is non-sensical to evaluate the pure expression List.map(x -> 2 * x, 1 :: 2 :: Nil) and then to discard its result. Most likely the programmer wanted to use the result (or alternatively the expression is redundant and could be deleted). Consequently, Flix rejects such programs.
Flix supports Datalog programs as first-class values.[6] [9] [26] A Datalog program is a logic program that consists of a collection of unordered facts and rules. Together, the facts and rules imply a minimal model, a unique solution to any Datalog program. In Flix, Datalog program values can be passed to and returned from functions, stored in data structures, composed with other Datalog program values, and solved. The solution to a Datalog program (the minimal model) is itself a Datalog program. Thus, it is possible to construct pipelines of Datalog programs where the solution, i.e. "output", of one Datalog program becomes the "input" to another Datalog program.
The following edge facts define a graph:
The following Datalog rules compute the transitive closure of the edge relation:
The minimal model of the facts and rules is:
In Flix, Datalog programs are values. The above program can be embedded in Flix as follows:
The local variable f holds a Datalog program value that consists of the edge facts. Similarly, the local variable p is a Datalog program value that consists of the two rules. The f <+> p expression computes the composition (i.e. union) of the two Datalog programs f and p. The solve expression computes the minimal model of the combined Datalog program, returning the edge and path facts shown above.
Since Datalog programs are first-class values, we can refactor the above program into several functions. For example:
def closure: # = #
def main: # = solve edges <+> closure
The un-directed closure of the graph can be computed by adding the rule:
We can modify the closure function to take a Boolean argument that determines whether we want to compute the directed or un-directed closure:
The Flix type system ensures that Datalog program values are well-typed.
For example, the following program fragment does not type check:
because in p1 the type of the Edge predicate is Edge(Int, Int) whereas in p2 it has type Edge(String, String). The Flix compiler rejects such programs as ill-typed.
The Flix compiler ensures that every Datalog program value constructed at run-time is stratified. Stratification is important because it guarantees the existence of a unique minimal model in the presence of negation. Intuitively, a Datalog program is stratified if there is no recursion through negation,[27] i.e. a predicate cannot depend negatively on itself. Given a Datalog program, a cycle detection algorithm can be used to determine if it is stratified.
For example, the following Flix program contains an expression that cannot be stratified:
because the last expression constructs a Datalog program value whose precedence graph contains a negative cycle: the Bachelor predicate negatively depends on the Husband predicate which in turn (positively) depends on the Bachelor predicate.
The Flix compiler computes the precedence graph for every Datalog program valued expression and determines its stratification at compile-time. If an expression is not stratified, the program is rejected by the compiler.
The stratification is sound, but conservative. For example, the following program is unfairly rejected:
The type system conservatively assumes that both branches of the if expression can be taken and consequently infers that there may be a negative cycle between the A and B predicates. Thus the program is rejected. This is despite the fact that at run-time the main function always returns a stratified Datalog program value.
Flix is designed around a collection of stated principles:[28]
The principles also list several programming language features that have been deliberately omitted. In particular, Flix lacks support for: