Flix (programming language)
This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these template messages)
|
Flix is a
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
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 processesWhile 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
Flix supports
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
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
- ^ "Apache License 2.0". 27 July 2022 – via GitHub.
- ^ "Forskningsprojekter". Danmarks Frie Forskningsfond (in Danish).
- ^ "Flix Authors". GitHub. 27 July 2022.
- ^ Leijen, Daan. "Extensible records with scoped labels". Trends in Functional Programming.
- ^ S2CID 227044242.
- ^ S2CID 227107960.
- S2CID 13015611.
- S2CID 14902937.
- ^ a b "Programming Flix - Fixpoints". flix.dev.
- .
- S2CID 49427988.
- S2CID 203631644.
- ^ Gong, Qing. Extending Parallel Datalog with Lattice. Pennsylvania State University.
- ^ Yee, Ming-Ho (2016-09-15). Implementing a Functional Language for Flix. University of Waterloo.
- ^ "Monomorphise". mlton.org.
- ^ "Programming Flix - Interoperability". flix.dev.
- S2CID 3432962.
- )
- ^ "Redundancies as Compile-Time Errors". flix.dev.
- .
- ^ "flix - Visual Studio Marketplace". marketplace.visualstudio.com.
- ^ "Programming Flix - Effects". flix.dev.
- ^ "Rust Internals - Flix Polymorphic Effects". 15 November 2020.
- ^ "The Flix API - List". api.flix.dev.
- ^ "The Flix API - Prelude". api.flix.dev.
- S2CID 208305062.
- ^ Minker, Jack. Foundations of deductive databases and logic programming. Morgan Kaufmann.
- ^ "The Flix Programming Language - Principles". flix.dev. Retrieved 28 August 2020.
- ^ "Taming Impurity with Polymorphic Effects". flix.dev.
External links
- Official website
- Flix implementation source code, hosted at GitHub.