Content deleted Content added
m →Examples: lang="flx" |
m →Notable features: lang="flx" |
||
Line 143:
For example, the following expression is of type <code>Int</code> and is <code>Pure</code>:
<syntaxhighlight lang="
1 + 2 : Int & Pure
</syntaxhighlight>
Line 149:
whereas the following expression is <code>Impure</code>:
<syntaxhighlight lang="
Console.printLine("Hello World") : Unit & Impure
</syntaxhighlight>
Line 157:
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 168:
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 177:
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 185:
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 195:
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 205:
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 213:
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 239:
The following edge facts define a graph:
<syntaxhighlight lang="
Edge(1, 2). Edge(2, 3). Edge(3, 4).
</syntaxhighlight>
Line 245:
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:
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:
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 276:
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 291:
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:
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 315:
For example, the following program fragment does not type check:
<syntaxhighlight lang="
let p1 = Edge(123, 456).;
let p2 = Edge("a", "b").;
Line 329:
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:
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)
| |||