Content deleted Content added
m Add missing DOI |
The Death of UFCS: https://github.com/flix/flix/issues/1500 |
||
| (41 intermediate revisions by 19 users not shown) | |||
Line 1:
{{about|the Flix programming language|other uses|Flix (disambiguation)}}
{{Orphan|date=December 2020}}▼
{{multiple issues|
{{excessive detail|date=December 2020}}
{{more citations needed|date=December 2020}}
}}
{{Infobox programming language
| name = Flix
Line 7 ⟶ 12:
| typing = [[Hindley-Milner|inferred]], [[Static typing|static]], [[Strong and weak typing|strong]], [[structural typing|structural]]
| 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 = [[
| 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 [[
The Flix type and effect system supports [[
Flix supports [[Datalog]] programs as [[First-
== Overview ==
Flix is a [[programming language]] in the [[Standard ML|ML]]-family of languages. Its type and effect system is based on [[
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 [[
Flix programs
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>
Monomorphization avoids [[
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
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>
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>
Flix is [[Open-
== Examples ==
=== Hello
The following program prints "[["Hello,
<syntaxhighlight lang="
def main(): Unit
</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
The following program fragment declares an [[algebraic data type]] (ADT) named <code>Shape</code>:
<syntaxhighlight lang="
enum Shape {
case Circle(
case Square(
case Rectangle(
}
</syntaxhighlight>
Line 65 ⟶ 70:
The following program fragment uses [[pattern matching]] to destruct a <code>Shape</code> value:
<syntaxhighlight lang="
def area(s: Shape):
case Circle(r) => 3 * (r * r)
case Square(w) => w * w
Line 73 ⟶ 78:
</syntaxhighlight>
=== Higher-
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="
def twice(f:
</syntaxhighlight>
We can use the function <code>twice</code> as follows:
<syntaxhighlight lang="
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.
=== Parametric
The following program fragment illustrates a [[
<syntaxhighlight lang="
def map(f: a -> b, l: List[a]): List[b] = match l {
case Nil => Nil
Line 100 ⟶ 105:
</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
The following program fragment shows how to construct a [[
<syntaxhighlight lang="
def point2d(): {x:
</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="
def sum(r: {x:
</syntaxhighlight>
The following are all valid calls to the <code>sum</code> function:
<syntaxhighlight lang="
sum({x = 1, y = 2})
sum({y = 2, x = 1})
Line 126 ⟶ 131:
</syntaxhighlight>
== Notable
=== Polymorphic
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>
For example, the following expression is of type <code>
<syntaxhighlight lang="
1 + 2 :
</syntaxhighlight>
whereas the following expression
<syntaxhighlight lang="
</syntaxhighlight>
Line 148 ⟶ 153:
For example, the definition of <code>Set.exists</code> requires that its function argument <code>f</code> is pure:
<syntaxhighlight lang="
// The syntax a -> Bool is short-hand for a -> Bool
def exists(f: a -> Bool, xs: Set[a]): Bool = ...
</syntaxhighlight>
Line 159 ⟶ 164:
For example, the definition of <code>List.foreach</code> requires that its function argument <code>f</code> is impure:
<syntaxhighlight lang="
</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
<syntaxhighlight lang="
if (1 == 2)
</syntaxhighlight>
Line 176 ⟶ 180:
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="
def map(f: a -> b
</syntaxhighlight>
Line 184 ⟶ 188:
A higher-order function that takes multiple function arguments may combine their effects.
For example, the standard library definition of forward [[
<syntaxhighlight lang="
def >>(f: a -> b
</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
The type and effect system allows arbitrary
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
<syntaxhighlight lang="
def h(f: a -> b
</syntaxhighlight>
If <code>h</code> is called with a function argument <code>f</code> which
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="
def main(): Unit
List.map(x -> 2 * x, 1 :: 2 :: Nil);
</syntaxhighlight>
causes a compiler error:
<syntaxhighlight lang="output">
-- Redundancy Error --------------------------------------------------
Line 224 ⟶ 228:
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
Flix supports [[Datalog]] programs as first-class values.<ref name="oopsla2020b"/>
The following edge facts define a graph:
<syntaxhighlight lang="
Edge(1, 2). Edge(2, 3). Edge(3, 4).
</syntaxhighlight>
Line 236 ⟶ 240:
The following Datalog rules compute the [[transitive closure]] of the edge relation:
<syntaxhighlight lang="
Path(x, y) :- Edge(x, y).
Path(x, z) :- Path(x, y), Edge(y, z).
Line 243 ⟶ 247:
The minimal model of the facts and rules is:
<syntaxhighlight lang="
Edge(1, 2). Edge(2, 3). Edge(3, 4).
Path(1, 2). Path(2, 3). Path(3, 4).
Line 249 ⟶ 253:
</syntaxhighlight>
In Flix, Datalog programs are values. The above program can be [[Domain-
<syntaxhighlight lang="
def main(): #{Edge(
let f = #{
Edge(1, 2). Edge(2, 3). Edge(3, 4).
Line 267 ⟶ 271:
Since Datalog programs are first-class values, we can refactor the above program into several functions. For example:
<syntaxhighlight lang="
def edges(): #{Edge(
Edge(1, 2). Edge(2, 3). Edge(3, 4).
}
def closure(): #{Edge(
Path(x, y) :- Edge(x, y).
Path(x, z) :- Path(x, y), Edge(y, z).
}
def
</syntaxhighlight>
The un-directed closure of the graph can be computed by adding the rule:
<syntaxhighlight lang="
Path(x, y) :- Path(y, x).
</syntaxhighlight>
Line 288 ⟶ 292:
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="
def closure(directed: Bool): #{Edge(
let p1 = #{
Path(x, y) :- Edge(x, y).
Line 300 ⟶ 304:
</syntaxhighlight>
==== Type-safe
The Flix type system ensures that Datalog program values are well-typed.
Line 306 ⟶ 310:
For example, the following program fragment does not type check:
<syntaxhighlight lang="
let p1 = Edge(123, 456).;
let p2 = Edge("a", "b").;
Line 312 ⟶ 316:
</syntaxhighlight>
because in <code>p1</code> the type of the <code>Edge</code> predicate is <code>Edge(
==== Stratified
The Flix compiler ensures that every Datalog program value constructed at run-time is [[
For example, the following Flix program contains an expression that cannot be stratified:
<syntaxhighlight lang="
def main(): #{Male(String), Husband(String), Bachelor(String)} =
let p1 = Husband(x) :- Male(x), not Bachelor(x).;
Line 327 ⟶ 331:
</syntaxhighlight>
because the last expression constructs a Datalog program value whose [[
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 [[
<syntaxhighlight lang="
def main(): #{A(
if (true)
A(x) :- A(x), not B(x).
Line 343 ⟶ 347:
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
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-
* [[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>
Line 354 ⟶ 358:
The principles also list several programming language features that have been deliberately omitted. In particular, Flix lacks support for:
* [[
* [[
* [[
== 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
* [https://flix.dev/
* [https://
[[Category:Procedural programming languages]]
[[Category:Functional languages]]
[[Category:Logic programming languages]]
[[Category:High-level programming languages]]
| |||