Content deleted Content added
No edit summary |
The Death of UFCS: https://github.com/flix/flix/issues/1500 |
||
| (211 intermediate revisions by 22 users not shown) | |||
Line 1:
{{about|the Flix programming language|other uses|Flix (disambiguation)}}
{{multiple issues|
{{excessive detail|date=December 2020}}
{{more citations needed|date=December 2020}}
{{primary sources|date=December 2020}}
}}
{{Infobox programming language
| name = Flix
| paradigm = [[Multi-paradigm programming language|Multi-paradigm]]: [[Functional programming|functional]], [[Imperative programming|imperative]], [[Logic programming|logic]]
| developer = [[Aarhus University]], open-source contributors
| typing = [[Hindley-Milner|inferred]], [[Static typing|static]], [[Strong and weak typing|strong]], [[
| platform = [[Java virtual machine|JVM]]
| license = [[Apache License 2.0]].<ref name="license-github">{{cite web |url=https://github.com/flix/flix/blob/master/LICENSE.md|title=Apache License 2.0|date=27 July 2022 |via=[[GitHub]]}}</ref>
| 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 book |last1=Lucassen |first1=J. M. |last2=Gifford |first2=D. K. |title=Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - 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 book |last1=Madsen |first1=Magnus |last2=Lhoták |first2=Ondřej |title=Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis |chapter=Safe and sound 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]]. 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.
Flix programs compile to [[JVM bytecode]] and are executable on the [[Java Virtual Machine]] (JVM).<ref>{{cite book |last1=Yee |first1=Ming-Ho |title=Implementing a Functional Language for Flix |date=2016-09-15 |publisher=University of Waterloo}}</ref>
The Flix compiler performs [[whole program compilation]], eliminates polymorphism via [[monomorphization]],<ref>{{cite web |title=Monomorphise |url=http://mlton.org/Monomorphise |website=mlton.org}}</ref> and uses [[tree shaking]] to remove [[unreachable code]].
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 book |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 |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 book |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. |chapter=Memory-Efficient Tail Calls in the JVM with Imperative Functional Objects |title=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>
A [[Visual Studio Code]] extension for Flix is available.<ref>{{cite web |title=flix - Visual Studio Marketplace |url=https://marketplace.visualstudio.com/items?itemName=flix.flix |website=marketplace.visualstudio.com |language=en-us}}</ref> The extension is based on the [[Language Server Protocol]], a common interface between [[Integrated development environment|IDEs]] and [[compilers]] being developed by [[Microsoft]].
Flix is [[Open-source software|open source software]] available under the [[Apache License|Apache 2.0 License]].
== Examples ==
===
The following program prints "[["Hello, World!" program|Hello World!]]" when compiled and executed:
<syntaxhighlight lang="flx">
def main(): Unit \ IO =
println("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 ===
The following program fragment declares an [[algebraic data type]] (ADT) named <code>Shape</code>:
<syntaxhighlight lang="flx">
enum Shape {
case Circle(Int32), // has circle radius
case Square(Int32), // has side length
case Rectangle(Int32, Int32) // has height and width
}
</syntaxhighlight>
The ADT has three constructors: <code>Circle</code>, <code>Square</code>, and <code>Rectangle</code>.
The following program fragment uses [[pattern matching]] to destruct a <code>Shape</code> value:
<syntaxhighlight lang="flx">
def area(s: Shape): Int32 = match s {
case Circle(r) => 3 * (r * r)
case Square(w) => w * w
case Rectangle(h, w) => h * w
}
</syntaxhighlight>
=== Higher-order functions ===
The following program fragment defines a [[higher-order function]] named <code>twice</code> that when given a function <code>f</code> from <code>Int</code> to <code>Int</code> returns a function that applies <code>f</code> to its input two times:
<syntaxhighlight lang="flx">
def twice(f: Int32 -> Int32): Int32 -> Int32 = x -> f(f(x))
</syntaxhighlight>
We can use the function <code>twice</code> as follows:
<syntaxhighlight lang="flx">
twice(x -> x + 1)(0)
</syntaxhighlight>
Here the call to <code>twice(x -> x + 1)</code> returns a function that will increment its argument two times. Thus the result of the whole expression is <code>0 + 1 + 1 = 2</code>.
=== Parametric polymorphism ===
The following program fragment illustrates a [[Parametric polymorphism|polymorphic function]] that maps a function <code>f: a -> b</code> over a list of elements of type <code>a</code> returning a list of elements of type <code>b</code>:
<syntaxhighlight lang="flx">
def map(f: a -> b, l: List[a]): List[b] = match l {
case Nil => Nil
case x :: xs => f(x) :: map(f, xs)
}
</syntaxhighlight>
The <code>map</code> function recursively traverses the list <code>l</code> and applies <code>f</code> to each element constructing a new list.
Flix supports type parameter elision hence it is not required that the type parameters <code>a</code> and <code>b</code> are explicitly introduced.
=== Extensible records ===
The following program fragment shows how to construct a [[Record (computer science)|record]] with two fields <code>x</code> and <code>y</code>:
<syntaxhighlight lang="flx">
def point2d(): {x: Int32, y: Int32} = {x = 1, y = 2}
</syntaxhighlight>
Flix uses [[row polymorphism]] to type records. The <code>sum</code> function below takes a record that has <code>x</code> and <code>y</code> fields (and possibly other fields) and returns the sum of the two fields:
<syntaxhighlight lang="flx">
def sum(r: {x: Int32, y: Int32 | rest}): Int = r.x + r.y
</syntaxhighlight>
The following are all valid calls to the <code>sum</code> function:
<syntaxhighlight lang="flx">
sum({x = 1, y = 2})
sum({y = 2, x = 1})
sum({x = 1, y = 2, z = 3})
</syntaxhighlight>
== Notable features ==
=== Polymorphic effects ===
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>Int32</code> and has the empty effect set <code>{}</code>, i.e. it is pure:
<syntaxhighlight lang="flx">
1 + 2 : Int32 \ {}
</syntaxhighlight>
whereas the following expression has the <code>IO</code> effect, i.e. is impure:
<syntaxhighlight lang="flx">
println("Hello World") : Unit \ IO
</syntaxhighlight>
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 <code>Set.exists</code> requires that its function argument <code>f</code> is pure:
<syntaxhighlight lang="flx">
// The syntax a -> Bool is short-hand for a -> Bool \ {}
def exists(f: a -> Bool, xs: Set[a]): Bool = ...
</syntaxhighlight>
The requirement that <code>f</code> must be pure ensures that implementation details do not [[leaky abstraction|leak]]. For example, since <code>f</code> is pure it cannot be used to determine in what order the elements of the set are traversed. If <code>f</code> 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 <code>List.foreach</code> requires that its function argument <code>f</code> is impure:
<syntaxhighlight lang="flx">
def foreach(f: a -> Unit \ IO, xs: List[a]): Unit \ IO
</syntaxhighlight>
The requirement that <code>f</code> must be impure ensures that the code makes sense: It would be meaningless to call <code>List.foreach</code> with a pure function since it always returns <code>Unit</code>.
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:
<syntaxhighlight lang="flx">
if (1 == 2) println("Hello World!") else ()
</syntaxhighlight>
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 <code>List.map</code> is effect polymorphic:<ref>{{cite web |title=The Flix API - List|url=https://api.flix.dev/List |website=api.flix.dev}}</ref>
<syntaxhighlight lang="flx">
def map(f: a -> b \ e, xs: List[a]): List[b] \ e
</syntaxhighlight>
The <code>List.map</code> function takes a function <code>f</code> from elements of type <code>a</code> to <code>b</code> with effect <code>e</code>. The effect of the map function is itself <code>e</code>. Consequently, if <code>List.map</code> 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 (computer science)|function composition]] <code>>></code> is pure if both its function arguments are pure:<ref>{{cite web |title=The Flix API - Prelude |url=https://api.flix.dev/ |website=api.flix.dev}}</ref>
<syntaxhighlight lang="flx">
def >>(f: a -> b \ e1, g: b -> c \ e2): a -> c \ e1 + e2 = x -> g(f(x))
</syntaxhighlight>
The type and effect signature can be understood as follows: The <code>>></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>>></code> is effect polymorphic in the [[Logical conjunction|conjunction]] of <code>e1</code> and <code>e2</code>. If both are pure then the overall expression is pure.
The type and effect system allows arbitrary set 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 <code>f</code> are disjoint from those of <code>g</code>:
<syntaxhighlight lang="flx">
def h(f: a -> b \ e1, g: b -> c \ e2 - e1): Unit
</syntaxhighlight>
If <code>h</code> is called with a function argument <code>f</code> which has the <code>IO</code> effect then <code>g</code> cannot have the <code>IO</code> effect.
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 \ IO =
List.map(x -> 2 * x, 1 :: 2 :: Nil);
println("Hello World")
</syntaxhighlight>
causes a compiler error:
<syntaxhighlight lang="output">
-- 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.
</syntaxhighlight>
because it is non-sensical to evaluate the pure expression <code>List.map(x -> 2 * x, 1 :: 2 :: Nil)</code> 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.<ref name="oopsla2020b"/><ref name="Programming Flix - Fixpoints"/><ref>{{cite journal |last1=Arntzenius |first1=Michael |last2=Krishnaswami |first2=Neel |title=Seminaïve evaluation for a higher-order functional language |journal=Proceedings of the ACM on Programming Languages |date=January 2020 |volume=4 |issue=POPL |pages=1–28 |doi=10.1145/3371090|s2cid=208305062 |doi-access=free }}</ref> A Datalog program is a logic program that consists of a collection of unordered [[fact]]s and [[Horn clause|rules]]. Together, the facts and rules imply a [[Minimal model program|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:
<syntaxhighlight lang="flx">
Edge(1, 2). Edge(2, 3). Edge(3, 4).
</syntaxhighlight>
The following Datalog rules compute the [[transitive closure]] of the edge relation:
<syntaxhighlight lang="prolog">
Path(x, y) :- Edge(x, y).
Path(x, z) :- Path(x, y), Edge(y, z).
</syntaxhighlight>
The minimal model of the facts and rules is:
<syntaxhighlight lang="flx">
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).
</syntaxhighlight>
In Flix, Datalog programs are values. The above program can be [[Domain-specific language|embedded]] in Flix as follows:
<syntaxhighlight lang="flx">
def main(): #{Edge(Int32, Int32), Path(Int32, Int32)} =
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
</syntaxhighlight>
The local variable <code>f</code> holds a Datalog program value that consists of the edge facts. Similarly, the local variable <code>p</code> is a Datalog program value that consists of the two rules. The <code>f <+> p</code> expression computes the composition (i.e. union) of the two Datalog programs <code>f</code> and <code>p</code>. The <code>solve</code> 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:
<syntaxhighlight lang="flx">
def edges(): #{Edge(Int32, Int32), Path(Int32, Int32)} = #{
Edge(1, 2). Edge(2, 3). Edge(3, 4).
}
def closure(): #{Edge(Int32, Int32), Path(Int32, Int32)} = #{
Path(x, y) :- Edge(x, y).
Path(x, z) :- Path(x, y), Edge(y, z).
}
def run(): #{Edge(Int32, Int32), Path(Int32, Int32)} = solve edges() <+> closure()
</syntaxhighlight>
The un-directed closure of the graph can be computed by adding the rule:
<syntaxhighlight lang="prolog">
Path(x, y) :- Path(y, x).
</syntaxhighlight>
We can modify the <code>closure</code> function to take a Boolean argument that determines whether we want to compute the directed or un-directed closure:
<syntaxhighlight lang="flx">
def closure(directed: Bool): #{Edge(Int32, Int32), Path(Int32, Int32)} =
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)
</syntaxhighlight>
==== 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:
<syntaxhighlight lang="flx">
let p1 = Edge(123, 456).;
let p2 = Edge("a", "b").;
p1 <+> p2;
</syntaxhighlight>
because in <code>p1</code> the type of the <code>Edge</code> predicate is <code>Edge(Int32, Int32)</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 ====
The Flix compiler ensures that every Datalog program value constructed at run-time is [[Stratification (mathematics)#In mathematical logic|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,<ref>{{cite book |last1=Minker |first1=Jack |title=Foundations of deductive databases and logic programming |publisher=Morgan Kaufmann}}</ref> 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:
<syntaxhighlight lang="flx">
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.
</syntaxhighlight>
because the last expression constructs a Datalog program value whose [[precedence graph (Datalog)|precedence graph]] contains a negative cycle: the <code>Bachelor</code> predicate negatively depends on the <code>Husband</code> predicate which in turn (positively) depends on the <code>Bachelor</code> 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 [[Type system#Static type checking|unfairly rejected]]:
<syntaxhighlight lang="flx">
def main(): #{A(Int32), B(Int32)} =
if (true)
A(x) :- A(x), not B(x).
else
B(x) :- B(x), not A(x).
</syntaxhighlight>
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 <code>A</code> and <code>B</code> predicates. Thus the program is rejected. This is despite the fact that at run-time the <code>main</code> function always returns a stratified Datalog program value.
== Design philosophy ==
Flix is designed around a collection of stated principles:<ref>{{cite web |title=The Flix Programming Language - Principles |url=https://flix.dev/principles/ |website=flix.dev |accessdate=28 August 2020}}</ref>
* [[Expression-oriented programming language|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<ref>{{cite web |title=Taming Impurity with Polymorphic Effects |url=https://flix.dev/blog/taming-impurity-with-polymorphic-effects/ |website=flix.dev}}</ref>
* 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 pointer|Null values]]. Instead the use of the [[Option type|Option]] data type is recommended.
* [[Type conversion|Implicit coercions]]. Instead type conversions must be performed explicitly by the programmer.
* [[Reflection (computer programming)|Reflection]]. The programmer cannot reflect over the structure of the program at run-time.
== References ==
<!-- Inline citations added to your article will automatically display here. See en.wikipedia.org/wiki/WP:REFB for instructions on how to add citations. -->
{{reflist}}
== External links ==
* [https://flix.dev/ Official website]
* [https://github.com/flix/flix Flix implementation source code], hosted at [[GitHub]].
[[Category:Procedural programming languages]]
[[Category:Functional languages]]
[[Category:Logic programming languages]]
[[Category:High-level programming languages]]
| |||