Content deleted Content added
m Dating maintenance tags: {{Primary sources}} {{Refimprove}} {{Excessive detail}} |
The Death of UFCS: https://github.com/flix/flix/issues/1500 |
||
| (27 intermediate revisions by 14 users not shown) | |||
Line 1:
{{about|the Flix programming language|other uses|Flix (disambiguation)}}
{{multiple issues|
{{excessive detail|date=December 2020}}
{{
{{primary sources|date=December 2020}}
}}
Line 16 ⟶ 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 = [[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
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
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]]
== 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]]
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
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
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 47 ⟶ 43:
== Examples ==
=== Hello
The following program prints "[["Hello, World!" program|Hello World!]]" when compiled and executed:
<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 data types and pattern matching ===
Line 62 ⟶ 58:
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 74 ⟶ 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 86 ⟶ 82:
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 polymorphism ===
Line 102 ⟶ 98:
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="
def map(f: a -> b, l: List[a]): List[b] = match l {
case Nil => Nil
Line 117 ⟶ 113:
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="
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 139 ⟶ 135:
=== 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>
<syntaxhighlight lang="
1 + 2 :
</syntaxhighlight>
whereas the following expression
<syntaxhighlight lang="
</syntaxhighlight>
Line 157 ⟶ 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 168 ⟶ 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 185 ⟶ 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 195 ⟶ 190:
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="
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="
-- Redundancy Error --------------------------------------------------
Line 235 ⟶ 230:
=== 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="
Edge(1, 2). Edge(2, 3). Edge(3, 4).
</syntaxhighlight>
Line 245 ⟶ 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 252 ⟶ 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 260 ⟶ 255:
In Flix, Datalog programs are values. The above program can be [[Domain-specific language|embedded]] in Flix as follows:
<syntaxhighlight lang="
def main(): #{Edge(
let f = #{
Edge(1, 2). Edge(2, 3). Edge(3, 4).
Line 276 ⟶ 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 297 ⟶ 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 315 ⟶ 310:
For example, the following program fragment does not type check:
<syntaxhighlight lang="
let p1 = Edge(123, 456).;
let p2 = Edge("a", "b").;
Line 321 ⟶ 316:
</syntaxhighlight>
because in <code>p1</code> the type of the <code>Edge</code> predicate is <code>Edge(
==== Stratified negation ====
Line 329 ⟶ 324:
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 342 ⟶ 337:
The stratification is sound, but conservative. For example, the following program is [[Type system#Static type checking|unfairly rejected]]:
<syntaxhighlight lang="
def main(): #{A(
if (true)
A(x) :- A(x), not B(x).
Line 368 ⟶ 363:
== 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}}
Line 373 ⟶ 369:
== External links ==
* [https://flix.dev/ Official
* [https://github.com/flix/flix Flix implementation source code], hosted at [[GitHub]].
[[Category:Procedural programming languages]]
| |||