Flix (programming language)

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

Overview

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.

Examples

Hello world

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.

Algebraic data types and pattern matching

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
}

Higher-order functions

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.

Parametric polymorphism

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.

Extensible records

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})

Notable features

Polymorphic effects

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.

First-class datalog constraints

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)

Type-safe composition

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.

Stratified negation

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.

Design philosophy

Flix is designed around a collection of stated principles:^[28]

• Everything is an expression. Most Flix constructs, except for top-level declarations, are expressions that evaluate to values.
• Closed-world assumption. The Flix compiler assumes that the source code of the entire program is available at compile-time.
• Pure and impure code is separated. The type and effect system precisely captures whether an expression may produce an effect^[29]
• The language has no compile-time warnings, only errors.

The principles also list several programming language features that have been deliberately omitted. In particular, Flix lacks support for:

• Null values. Instead the use of the Option data type is recommended.
• Implicit coercions. Instead type conversions must be performed explicitly by the programmer.
• Reflection. The programmer cannot reflect over the structure of the program at run-time.

References

External links

• Official website
• Flix implementation source code, hosted at GitHub.

0.00 (0 votes) Original source: https://en.wikipedia.org/wiki/Flix (programming language). Read more