Content deleted Content added
Nominated for deletion; see Wikipedia:Articles for deletion/Flix (programming language). |
MOS:HEAD |
||
Line 46:
The following program prints "[["Hello, World!" program|Hello World!]]" when compiled and executed:
<syntaxhighlight lang="
def main(): Unit & Impure =
Console.printLine("Hello World!")
Line 53:
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 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(Int), // has circle radius
Line 69:
The following program fragment uses [[pattern matching]] to destruct a <code>Shape</code> value:
<syntaxhighlight lang="
def area(s: Shape): Int = match s {
case Circle(r) => 3 * (r * r)
Line 77:
</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: Int -> Int): Int -> Int = x -> f(f(x))
</syntaxhighlight>
Line 87:
We can use the function <code>twice</code> as follows:
<syntaxhighlight lang="
twice(x -> x + 1)(0)
</syntaxhighlight>
Line 93:
Here the call to <code>twice(x -> x + 1)</code> returns a function that will increment its argument two times. Consequently, the result of the entire expression is <code>0 + 1 + 1 = 2</code>.
=== Parametric
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 108:
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 [[Record (computer science)|record]] with two fields <code>x</code> and <code>y</code>:
<syntaxhighlight lang="
def point2d(): {x: Int, y: Int} = {x = 1, y = 2}
</syntaxhighlight>
Line 118:
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: Int, y: Int | rest}): Int = r.x + r.y
</syntaxhighlight>
Line 124:
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 130:
</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|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.
Line 138:
For example, the following expression is of type <code>Int</code> and is <code>Pure</code>:
<syntaxhighlight lang="
1 + 2 : Int & Pure
</syntaxhighlight>
Line 144:
whereas the following expression is <code>Impure</code>:
<syntaxhighlight lang="
Console.printLine("Hello World") : Unit & Impure
</syntaxhighlight>
Line 152:
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 & Pure
def exists(f: a -> Bool, xs: Set[a]): Bool = ...
Line 163:
For example, the definition of <code>List.foreach</code> requires that its function argument <code>f</code> is impure:
<syntaxhighlight lang="
// The syntax a ~> Unit is short-hand for a -> Unit & Impure
def foreach(f: a ~> Unit, xs: List[a]): Unit & Impure
Line 172:
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="
if (1 == 2) Console.printLine("Hello World!") else ()
</syntaxhighlight>
Line 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 & e, xs: List[a]): List[b] & e
</syntaxhighlight>
Line 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 & e1, g: b -> c & e2): a -> c & (e1 and e2) = x -> g(f(x))
</syntaxhighlight>
Line 200:
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> of which at most one is impure:
<syntaxhighlight lang="
def h(f: a -> b & e1, g: b -> c & (not e1 or e2)): Unit
</syntaxhighlight>
Line 208:
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 & Impure =
List.map(x -> 2 * x, 1 :: 2 :: Nil);
Line 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"/><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 }}</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]], 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.
Line 234:
The following edge facts define a graph:
<syntaxhighlight lang="
Edge(1, 2). Edge(2, 3). Edge(3, 4).
</syntaxhighlight>
Line 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 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 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(Int, Int), Path(Int, Int)} =
let f = #{
Line 271:
Since Datalog programs are first-class values, we can refactor the above program into several functions. For example:
<syntaxhighlight lang="
def edges(): #{Edge(Int, Int), Path(Int, Int)} = #{
Edge(1, 2). Edge(2, 3). Edge(3, 4).
Line 286:
The un-directed closure of the graph can be computed by adding the rule:
<syntaxhighlight lang="
Path(x, y) :- Path(y, x).
</syntaxhighlight>
Line 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(Int, Int), Path(Int, Int)} =
let p1 = #{
Line 304:
</syntaxhighlight>
==== Type-safe
The Flix type system ensures that Datalog program values are well-typed.
Line 310:
For example, the following program fragment does not type check:
<syntaxhighlight lang="
let p1 = Edge(123, 456).;
let p2 = Edge("a", "b").;
Line 318:
because in <code>p1</code> the type of the <code>Edge</code> predicate is <code>Edge(Int, Int)</code> whereas in <code>p2</code> it has type <code>Edge(String, String)</code>. The Flix compiler rejects such programs as ill-typed.
==== Stratified
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.
Line 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 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(Int), B(Int)} =
if (true)
Line 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>
| |||