Flix (programming language)

The following program prints "Hello World!" when compiled and executed:

def main(): Unit & Impure = 
    Console.printLine("Hello World!")

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:

enum Shape {
    case Circle(Int),        // has circle radius
    case Square(Int),        // has side length
    case Rectangle(Int, Int) // has height and width
}

The ADT has three constructors: Circle, Square, and Rectangle.

The following program fragment uses pattern matching to destruct a Shape value:

def area(s: Shape): Int = match s {
    case Circle(r)       => 3 * (r * r)
    case Square(w)       => w * w
    case Rectangle(h, w) => h * w
}

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:

def twice(f: Int -> Int): Int -> Int = x -> f(f(x))

We can use the function twice as follows:

twice(x -> x + 1)(0)

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:

def map(f: a -> b, l: List[a]): List[b] = match l {
    case Nil     => Nil
    case x :: xs => f(x) :: map(f, xs)
}

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:

def point2d(): {x: Int, y: Int} = {x = 1, y = 2}

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:

def sum(r: {x: Int, y: Int | rest}): Int = r.x + r.y

The following are all valid calls to the sum function:

sum({x = 1, y = 2})
sum({y = 2, x = 1})
sum({x = 1, y = 2, z = 3})

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:

1 + 2 : Int & Pure

whereas the following expression is Impure:

Console.printLine("Hello World") : Unit & 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 syntax a -> Bool is short-hand for a -> Bool & Pure
def exists(f: a -> Bool, xs: Set[a]): Bool = ...

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 syntax a ~> Unit is short-hand for a -> Unit & Impure
def foreach(f: a ~> Unit, xs: List[a]): Unit & 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:

if (1 == 2) Console.printLine("Hello World!") else ()

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]

def map(f: a -> b & e, xs: List[a]): List[b] & e

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]

def >>(f: a -> b & e1, g: b -> c & e2): a -> c & (e1 and e2) = x -> g(f(x))

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:

def h(f: a -> b & e1, g: b -> c & (not e1 or e2)): Unit

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:

def main(): Unit & Impure = 
    List.map(x -> 2 * x, 1 :: 2 :: Nil);
    Console.printLine("Hello World")

causes a compiler error:

-- Redundancy 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:

Edge(1, 2). Edge(2, 3). Edge(3, 4).

The following Datalog rules compute the transitive closure of the edge relation:

Path(x, y) :- Edge(x, y).
Path(x, z) :- Path(x, y), Edge(y, z).

The minimal model of the facts and rules is:

Edge(1, 2). Edge(2, 3). Edge(3, 4). 
Path(1, 2). Path(2, 3). Path(3, 4). 
Path(1, 3). Path(1, 4). Path(2, 4).

In Flix, Datalog programs are values. The above program can be embedded in Flix as follows:

def main(): #{Edge(Int, Int), Path(Int, Int)} = 
  let f = #{
      Edge(1, 2). Edge(2, 3). Edge(3, 4).
  };
  let p = #{
    Path(x, y) :- Edge(x, y).
    Path(x, z) :- Path(x, y), Edge(y, z).
  };
  solve f <+> p

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 edges(): #{Edge(Int, Int), Path(Int, Int)} = #{
    Edge(1, 2). Edge(2, 3). Edge(3, 4).
}

def closure(): #{Edge(Int, Int), Path(Int, Int)} = #{
    Path(x, y) :- Edge(x, y).
    Path(x, z) :- Path(x, y), Edge(y, z).
}

def main(): #{Edge(Int, Int), Path(Int, Int)} = solve edges() <+> closure()

The un-directed closure of the graph can be computed by adding the rule:

Path(x, y) :- Path(y, x).

We can modify the closure function to take a Boolean argument that determines whether we want to compute the directed or un-directed closure:

def closure(directed: Bool): #{Edge(Int, Int), Path(Int, Int)} = 
    let p1 = #{
        Path(x, y) :- Edge(x, y).
        Path(x, z) :- Path(x, y), Edge(y, z).
    };
    let p2 = #{
        Path(y, x) :- Path(x, y).
    };
    if (directed) p1 else (p1 <+> p2)

The Flix type system ensures that Datalog program values are well-typed.

For example, the following program fragment does not type check:

let p1 = Edge(123, 456).;
let p2 = Edge("a", "b").;
p1 <+> p2;

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:

def main(): #{Male(String), Husband(String), Bachelor(String)} = 
    let p1 = Husband(x)  :- Male(x), not Bachelor(x).;
    let p2 = Bachelor(x) :- Male(x), not Husband(x).;
    p1 <+> p2 // illegal, not 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:

def main(): #{A(Int), B(Int)} = 
    if (true) 
        A(x) :- A(x), not B(x).
    else
        B(x) :- B(x), not A(x).

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.