Content deleted Content added
Narky Blert (talk | contribs) →Polymorphic effects: 2x dab-needed tag |
The Death of UFCS: https://github.com/flix/flix/issues/1500 |
||
| (20 intermediate revisions by 12 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="flx">
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 64 ⟶ 60:
<syntaxhighlight lang="flx">
enum Shape {
case Circle(
case Square(
case Rectangle(
}
</syntaxhighlight>
Line 75 ⟶ 71:
<syntaxhighlight lang="flx">
def area(s: Shape):
case Circle(r) => 3 * (r * r)
case Square(w) => w * w
Line 87 ⟶ 83:
<syntaxhighlight lang="flx">
def twice(f:
</syntaxhighlight>
Line 96 ⟶ 92:
</syntaxhighlight>
Here the call to <code>twice(x -> x + 1)</code> returns a function that will increment its argument two times.
=== Parametric polymorphism ===
Line 118 ⟶ 114:
<syntaxhighlight lang="flx">
def point2d(): {x:
</syntaxhighlight>
Line 124 ⟶ 120:
<syntaxhighlight lang="flx">
def sum(r: {x:
</syntaxhighlight>
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="flx">
1 + 2 :
</syntaxhighlight>
whereas the following expression
<syntaxhighlight lang="flx">
</syntaxhighlight>
Line 158 ⟶ 154:
<syntaxhighlight lang="flx">
// The syntax a -> Bool is short-hand for a -> Bool
def exists(f: a -> Bool, xs: Set[a]): Bool = ...
</syntaxhighlight>
Line 169 ⟶ 165:
<syntaxhighlight lang="flx">
</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="flx">
if (1 == 2)
</syntaxhighlight>
Line 186 ⟶ 181:
<syntaxhighlight lang="flx">
def map(f: a -> b
</syntaxhighlight>
Line 196 ⟶ 191:
<syntaxhighlight lang="flx">
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="flx">
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="flx">
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:
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 261 ⟶ 256:
<syntaxhighlight lang="flx">
def main(): #{Edge(
let f = #{
Edge(1, 2). Edge(2, 3). Edge(3, 4).
Line 277 ⟶ 272:
<syntaxhighlight lang="flx">
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 298 ⟶ 293:
<syntaxhighlight lang="flx">
def closure(directed: Bool): #{Edge(
let p1 = #{
Path(x, y) :- Edge(x, y).
Line 321 ⟶ 316:
</syntaxhighlight>
because in <code>p1</code> the type of the <code>Edge</code> predicate is <code>Edge(
==== Stratified negation ====
Line 343 ⟶ 338:
<syntaxhighlight lang="flx">
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]].
| |||