Flix (programming language): Difference between revisions

Revision as of 09:24, 14 March 2023

Latest revision as of 09:34, 8 August 2025

(9 intermediate revisions by 5 users not shown)

Line 15:

| website = {{URL|https://flix.dev/}}

| influenced_by = [[F Sharp (programming language)|F#]], [[Go (programming language)|Go]], [[Haskell (programming language)|Haskell]], [[OCaml]], [[Scala (programming language)|Scala]]

| file_ext = {{Mono|.flix}}

}}

'''Flix''' is a [[functional programming|functional]], [[imperative programming|imperative]], and [[logic programming|logic]] [[programming language]] developed at [[Aarhus University]], with funding from the [[Danish Council for Independent Research|Independent Research Fund Denmark]],<ref>{{cite web |title=Forskningsprojekter |url=https://dff.dk/forskningsprojekter?SearchableText=functional+and+declarative+logic+programming&period%3Alist=all&instrument%3Alist=all&filed_method%3Alist=all |website=Danmarks Frie Forskningsfond |language=da}}</ref> and by a community of [[open source]] contributors.<ref>{{cite web |title=Flix Authors |url=https://github.com/flix/flix/blob/master/AUTHORS.md |website=GitHub |date=27 July 2022 |language=en}}</ref> The Flix language supports [[algebraic data types]], [[pattern matching]], [[parametric polymorphism]], [[currying]], [[higher-order function]]s, [[extensible records]],<ref>{{cite journal |last1=Leijen |first1=Daan |title=Extensible records with scoped labels |journal=Trends in Functional Programming}}</ref> [[Communicating sequential processes|channel and process-based concurrency]], and [[tail call elimination]]. Two notable features of Flix are its type and effect system<ref name="oopsla2020a">{{cite journal |last1=Madsen |first1=Magnus |last2=van de Pol |first2=Jaco |title=Polymorphic Types and Effects with Boolean Unification |journal=Proceedings of the ACM on Programming Languages |date=13 November 2020 |volume=4 |issue=OOPSLA |pages=1–29 |doi=10.1145/3428222|s2cid=227044242 |doi-access=free }}</ref> and its support for first-class Datalog constraints.<ref name="oopsla2020b">{{cite journal |last1=Madsen |first1=Magnus |last2=Lhoták |first2=Ondřej |title=Fixpoints for the Masses: Programming with First-class Datalog Constraints |journal=Proceedings of the ACM on Programming Languages |date=13 November 2020 |volume=4 |issue=OOPSLA |pages=125:1–125:28 |doi=10.1145/3428193|s2cid=227107960 |doi-access=free }}</ref>

The Flix type and effect system supports [[Hindley–Milner type system|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]]<ref>{{cite journalbook |last1=Lucassen |first1=J. M. |last2=Gifford |first2=D. K. |title=Polymorphic effect systems |journal=Proceedings of the 15th ACM SIGPLAN-SIGACT Symposiumsymposium on Principles of Programmingprogramming Languageslanguages - POPL '88 |chapter=Polymorphic effect systems |date=1988 |pages=47–57 |doi=10.1145/73560.73564|isbn=0897912527 |s2cid=13015611 |doi-access=free }}</ref><ref>{{cite journal |last1=Leijen |first1=Daan |title=Koka: Programming with Row Polymorphic Effect Types |journal=Electronic Proceedings in Theoretical Computer Science |date=5 June 2014 |volume=153 |pages=100–126 |doi=10.4204/EPTCS.153.8|arxiv=1406.2061 |s2cid=14902937 }}</ref> 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 citizen|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 program|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 [[metaprogramming|meta programming]] language for Datalog. Flix supports [[Stratification (mathematics)#In mathematical logic|stratified negation]] and the Flix compiler ensures stratification at compile-time.<ref name="Programming Flix - Fixpoints">{{cite web |title=Programming Flix - Fixpoints |url=https://doc.flix.dev/fixpoints/ |website=flix.dev}}</ref> Flix also supports an enriched form of Datalog constraints where predicates are given [[Lattice (order)|lattice]] semantics.<ref>{{cite journal |last1=Madsen |first1=Magnus |last2=Yee |first2=Ming-Ho |last3=Lhoták |first3=Ondřej |title=From Datalog to flix: a declarative language for fixed points on lattices |journal=ACM SIGPLAN Notices |date=August 2016 |volume=51 |issue=6 |pages=194–208 |doi=10.1145/2980983.2908096}}</ref><ref>{{cite journalbook |last1=Madsen |first1=Magnus |last2=Lhoták |first2=Ondřej |title=Safe and sound program analysis with Flix |journal=Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis -|chapter=Safe ISSTAand 2018sound program analysis with Flix |date=2018 |pages=38–48 |doi=10.1145/3213846.3213847|isbn=9781450356992 |s2cid=49427988 }}</ref><ref>{{cite journal |last1=Keidel |first1=Sven |last2=Erdweg |first2=Sebastian |title=Sound and reusable components for abstract interpretation |journal=Proceedings of the ACM on Programming Languages |date=10 October 2019 |volume=3 |issue=OOPSLA |pages=1–28 |doi=10.1145/3360602|s2cid=203631644 |doi-access=free }}</ref><ref>{{cite book |last1=Gong |first1=Qing |title=Extending Parallel Datalog with Lattice |publisher=Pennsylvania State University}}</ref>

== Overview ==

Flix is a [[programming language]] in the [[Standard ML|ML]]-family of languages. Its type and effect system is based on [[Hindley–Milner type system|Hindley-Milner]] with several extensions, including [[row polymorphism]] and [[Unification (computer science)#E-unification|Boolean unification]]. The syntax of Flix is inspired by [[Scala (programming language)|Scala]] and uses short [[Reserved word|keywords]] and [[curly braces]]. Flix supports [[Uniform Function Call Syntax|uniform function call syntax]] which allows a function call <code>f(x, y, z)</code> to be written as <code>x.f(y, z)</code>. The concurrency model of Flix is inspired by [[Go (programming language)|Go]] and based on [[Communicating sequential processes|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 programming|purely functional style]] with purity enforced by the effect system.

Line 33:

Monomorphization avoids [[Value type and reference type|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 programming language|Java]].<ref>{{cite web |title=Programming Flix - Interoperability |url=https://doc.flix.dev/interoperability/ |website=flix.dev}}</ref>

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.<ref>{{cite journalbook |last1=Madsen |first1=Magnus |last2=Zarifi |first2=Ramin |last3=Lhoták |first3=Ondřej |title=Proceedings of the 27th International Conference on Compiler Construction |chapter=Tail call elimination and data representation for functional languages on the Java virtual machine |journal=Proceedings of the 27th International Conference on Compiler Construction - CC 2018 |date=2018 |pages=139–150 |doi=10.1145/3178372.3179499|isbn=9781450356442 |s2cid=3432962 }}</ref> Since the [[Java bytecode instruction listings|JVM instruction set]] lacks explicit support for tail calls, such calls are emulated using a form of reusable stack frames.<ref>{{cite journalbook |last1=Tauber |first1=Tomáš |last2=Bi |first2=Xuan |last3=Shi |first3=Zhiyuan |last4=Zhang |first4=Weixin |last5=Li |first5=Huang |last6=Zhang |first6=Zhenrui |last7=Oliveira |first7=Bruno C. D. S. |titlechapter=Memory-Efficient Tail Calls in the JVM with Imperative Functional Objects |journaltitle=Programming Languages and Systems |series=Lecture Notes in Computer Science |date=2015 |volume=9458 |pages=11–28 |doi=10.1007/978-3-319-26529-2_2|isbn=978-3-319-26528-5 }}</ref> 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.<ref>{{cite web |title=Redundancies as Compile-Time Errors |url=https://flix.dev/blog/redundancies-as-compile-time-errors/ |website=flix.dev}}</ref> [[Variable shadowing]] is also disallowed. The stated rationale is that unused or redundant code is often correlated with erroneous code<ref>{{cite journal |last1=Engler |first1=D. |title=Using redundancies to find errors |journal=IEEE Transactions on Software Engineering |date=October 2003 |volume=29 |issue=10 |pages=915–928 |doi=10.1109/TSE.2003.1237172}}</ref>

Line 48:

<syntaxhighlight lang="flx">

def main(): Unit &\ ImpureIO =

Console.printLineprintln("Hello World!")

</syntaxhighlight>

The type and effect signature of the <code>main</code> function specifies that it has no parameters, returns a value of type <code>Unit</code>, and that the function has the IO effect, i.e. is impure. The <code>main</code> function is impure because it invokes <code>printLine</code> which is impure.

=== Algebraic data types and pattern matching ===

Line 60:

<syntaxhighlight lang="flx">

enum Shape {

case Circle(IntInt32), // has circle radius

case Square(IntInt32), // has side length

case Rectangle(IntInt32, IntInt32) // has height and width

}

</syntaxhighlight>

Line 71:

<syntaxhighlight lang="flx">

def area(s: Shape): IntInt32 = match s {

case Circle(r) => 3 * (r * r)

case Square(w) => w * w

Line 83:

<syntaxhighlight lang="flx">

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

</syntaxhighlight>

Line 114:

<syntaxhighlight lang="flx">

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

</syntaxhighlight>

Line 120:

<syntaxhighlight lang="flx">

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

</syntaxhighlight>

Line 137:

The Flix type and effect system separates pure and impure expressions.<ref name="oopsla2020a"/><ref>{{cite web |title=Programming Flix - Effects |url=https://doc.flix.dev/effects/ |website=flix.dev}}</ref><ref>{{cite web|title=Rust Internals - Flix Polymorphic Effects|date=15 November 2020 |url=https://internals.rust-lang.org/t/flix-polymorphic-effects/13395}}</ref> A pure expression is guaranteed to be [[Referential transparency|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 <code>IntInt32</code> and ishas the empty effect set <code>Pure{}</code>, i.e. it is pure:

<syntaxhighlight lang="flx">

1 + 2 : IntInt32 &\ Pure{}

</syntaxhighlight>

whereas the following expression ishas the <code>ImpureIO</code> effect, i.e. is impure:

<syntaxhighlight lang="flx">

Console.printLineprintln("Hello World") : Unit &\ ImpureIO

</syntaxhighlight>

Line 154:

<syntaxhighlight lang="flx">

// The syntax a -> Bool is short-hand for a -> Bool &\ Pure{}

def exists(f: a -> Bool, xs: Set[a]): Bool = ...

</syntaxhighlight>

Line 165:

<syntaxhighlight lang="flx">

//def The syntaxforeach(f: a ~-> Unit is\ short-handIO, forxs: List[a ->]): Unit &\ ImpureIO

def foreach(f: a ~> Unit, xs: List[a]): Unit & Impure

</syntaxhighlight>

Line 174 ⟶ 173:

<syntaxhighlight lang="flx">

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

</syntaxhighlight>

Line 182 ⟶ 181:

<syntaxhighlight lang="flx">

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

</syntaxhighlight>

Line 192 ⟶ 191:

<syntaxhighlight lang="flx">

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

</syntaxhighlight>

The type and effect signature can be understood as follows: The <code>&gt;&gt;</code> function takes two function arguments: <code>f</code> with effect <code>e1</code> and <code>g</code> with effect <code>e2</code>. The effect of <code>&gt;&gt;</code> is effect polymorphic in the [[Logical conjunction|conjunction]] of <code>e1</code> and <code>e2</code>. 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 booleanset expressions to control the purity of function arguments.

For example, it is possible to express a higher-order function <code>h</code> that accepts two function arguments <code>f</code> and <code>g</code> where the effects of which<code>f</code> atare mostdisjoint onefrom isthose of impure<code>g</code>:

<syntaxhighlight lang="flx">

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

</syntaxhighlight>

If <code>h</code> is called with a function argument <code>f</code> which is impure (false) thenhas the second argument must be pure (true). Conversely, if <code>fIO</code> is pure (true)effect then <code>g</code> maycannot behave pure (true) or impure (false). It is a compile-time error to callthe <code>hIO</code> with two impure functionseffect.

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:

<syntaxhighlight lang="flx">

def main(): Unit &\ ImpureIO =

List.map(x -> 2 * x, 1 :: 2 :: Nil);

Console.printLineprintln("Hello World")

</syntaxhighlight>

Line 241 ⟶ 240:

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

<syntaxhighlight lang="flxprolog">

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

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

Line 257 ⟶ 256:

<syntaxhighlight lang="flx">

def main(): #{Edge(IntInt32, IntInt32), Path(IntInt32, IntInt32)} =

let f = #{

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

Line 273 ⟶ 272:

<syntaxhighlight lang="flx">

def edges(): #{Edge(IntInt32, IntInt32), Path(IntInt32, IntInt32)} = #{

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

}

def closure(): #{Edge(IntInt32, IntInt32), Path(IntInt32, IntInt32)} = #{

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

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

}

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

</syntaxhighlight>

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

<syntaxhighlight lang="flxprolog">

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

</syntaxhighlight>

Line 294 ⟶ 293:

<syntaxhighlight lang="flx">

def closure(directed: Bool): #{Edge(IntInt32, IntInt32), Path(IntInt32, IntInt32)} =

let p1 = #{

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

Line 317 ⟶ 316:

</syntaxhighlight>

because in <code>p1</code> the type of the <code>Edge</code> predicate is <code>Edge(IntInt32, IntInt32)</code> whereas in <code>p2</code> it has type <code>Edge(String, String)</code>. The Flix compiler rejects such programs as ill-typed.

==== Stratified negation ====

Line 339 ⟶ 338:

<syntaxhighlight lang="flx">

def main(): #{A(IntInt32), B(IntInt32)} =

if (true)

A(x) :- A(x), not B(x).