Content deleted Content added
too much detial |
The Death of UFCS: https://github.com/flix/flix/issues/1500 |
||
| (33 intermediate revisions by 16 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
Line 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 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 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 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 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 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 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 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 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 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 181 ⟶ 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 191 ⟶ 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 231 ⟶ 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 241 ⟶ 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 248 ⟶ 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 256 ⟶ 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 272 ⟶ 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 293 ⟶ 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 311 ⟶ 310:
For example, the following program fragment does not type check:
<syntaxhighlight lang="
let p1 = Edge(123, 456).;
let p2 = Edge("a", "b").;
Line 317 ⟶ 316:
</syntaxhighlight>
because in <code>p1</code> the type of the <code>Edge</code> predicate is <code>Edge(
==== Stratified negation ====
Line 325 ⟶ 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 338 ⟶ 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 364 ⟶ 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 369:
== External links ==
* [https://flix.dev/
* [https://
[[Category:Procedural programming languages]]
| |||