Flix (programming language): Difference between revisions

Revision as of 08:52, 26 September 2024

Latest revision as of 09:34, 8 August 2025

(4 intermediate revisions by 3 users not shown)

Line 25:

== 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]]. Flix supports [[Uniform Function Call Syntax|uniform function call syntax]] which allows a function call <code>f(x, y, z)</code> to be written as <code>x.f(y, z)</code>. The concurrency model of Flix is inspired by [[Go (programming language)|Go]] and based on [[Communicating sequential processes|channels and processes]]. A process is a light-weight thread that does not share (mutable) memory with another process. Processes communicate over channels which are bounded or unbounded queues of immutable messages.

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.

Line 49:

<syntaxhighlight lang="flx">

def main(): Unit \ IO =

Console.printLineprintln("Hello World!")

</syntaxhighlight>

Line 137:

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>IntInt32</code> and ishas the empty effect set <code>Pure{}</code>, i.e. it is pure:

<syntaxhighlight lang="flx">

1 + 2 : IntInt32 &\ Pure{}

</syntaxhighlight>

whereas the following expression ishas the <code>ImpureIO</code> effect, i.e. is impure:

<syntaxhighlight lang="flx">

Console.printLineprintln("Hello World") : Unit &\ ImpureIO

</syntaxhighlight>

Line 154:

<syntaxhighlight lang="flx">

// The syntax a -> Bool is short-hand for a -> Bool &\ Pure{}

def exists(f: a -> Bool, xs: Set[a]): Bool = ...

</syntaxhighlight>

Line 165:

<syntaxhighlight lang="flx">

//def The syntaxforeach(f: a ~-> Unit is\ short-handIO, forxs: List[a ->]): Unit &\ ImpureIO

def foreach(f: a ~> Unit, xs: List[a]): Unit & Impure

</syntaxhighlight>

Line 174 ⟶ 173:

<syntaxhighlight lang="flx">

if (1 == 2) Console.printLineprintln("Hello World!") else ()

</syntaxhighlight>

Line 182 ⟶ 181:

<syntaxhighlight lang="flx">

def map(f: a -> b &\ e, xs: List[a]): List[b] &\ e

</syntaxhighlight>

Line 192 ⟶ 191:

<syntaxhighlight lang="flx">

def >>(f: a -> b &\ e1, g: b -> c &\ e2): a -> c &\ (e1 and+ e2) = x -> g(f(x))

</syntaxhighlight>

The type and effect signature can be understood as follows: The <code>&gt;&gt;</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>&gt;&gt;</code> is effect polymorphic in the [[Logical conjunction|conjunction]] of <code>e1</code> and <code>e2</code>. If both are pure (their effect is true) then the overall expression is pure (true). Otherwise it is impure.

The type and effect system allows arbitrary booleanset expressions to control the purity of function arguments.

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 which<code>f</code> atare mostdisjoint onefrom isthose of impure<code>g</code>:

<syntaxhighlight lang="flx">

def h(f: a -> b &\ e1, g: b -> c &\ (note2 e1- or e2)e1): Unit

</syntaxhighlight>

If <code>h</code> is called with a function argument <code>f</code> which is impure (false) thenhas the second argument must be pure (true). Conversely, if <code>fIO</code> is pure (true)effect then <code>g</code> maycannot behave pure (true) or impure (false). It is a compile-time error to callthe <code>hIO</code> with two impure functionseffect.

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 &\ ImpureIO =

List.map(x -> 2 * x, 1 :: 2 :: Nil);

Console.printLineprintln("Hello World")

</syntaxhighlight>

Line 241 ⟶ 240:

The following Datalog rules compute the [[transitive closure]] of the edge relation:

<syntaxhighlight lang="flxprolog">

Path(x, y) :- Edge(x, y).

Path(x, z) :- Path(x, y), Edge(y, z).

Line 257 ⟶ 256:

<syntaxhighlight lang="flx">

def main(): #{Edge(IntInt32, IntInt32), Path(IntInt32, IntInt32)} =

let f = #{

Edge(1, 2). Edge(2, 3). Edge(3, 4).

Line 273 ⟶ 272:

<syntaxhighlight lang="flx">

def edges(): #{Edge(IntInt32, IntInt32), Path(IntInt32, IntInt32)} = #{

Edge(1, 2). Edge(2, 3). Edge(3, 4).

}

def closure(): #{Edge(IntInt32, IntInt32), Path(IntInt32, IntInt32)} = #{

Path(x, y) :- Edge(x, y).

Path(x, z) :- Path(x, y), Edge(y, z).

}

def mainrun(): #{Edge(IntInt32, IntInt32), Path(IntInt32, IntInt32)} = solve edges() <+> closure()

</syntaxhighlight>

The un-directed closure of the graph can be computed by adding the rule:

<syntaxhighlight lang="flxprolog">

Path(x, y) :- Path(y, x).

</syntaxhighlight>

Line 294 ⟶ 293:

<syntaxhighlight lang="flx">

def closure(directed: Bool): #{Edge(IntInt32, IntInt32), Path(IntInt32, IntInt32)} =

let p1 = #{

Path(x, y) :- Edge(x, y).

Line 317 ⟶ 316:

</syntaxhighlight>

because in <code>p1</code> the type of the <code>Edge</code> predicate is <code>Edge(IntInt32, IntInt32)</code> whereas in <code>p2</code> it has type <code>Edge(String, String)</code>. The Flix compiler rejects such programs as ill-typed.

==== Stratified negation ====

Line 339 ⟶ 338:

<syntaxhighlight lang="flx">

def main(): #{A(IntInt32), B(IntInt32)} =

if (true)

A(x) :- A(x), not B(x).