Flix (programming language): Difference between revisions

Revision as of 18:11, 22 June 2024

Latest revision as of 09:34, 8 August 2025

(5 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 48:

<syntaxhighlight lang="flx">

def main(): Unit &\ ImpureIO =

Console.printLineprintln("Hello World!")

</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 60:

<syntaxhighlight lang="flx">

enum Shape {

case Circle(IntInt32), // has circle radius

case Square(IntInt32), // has side length

case Rectangle(IntInt32, IntInt32) // has height and width

}

</syntaxhighlight>

Line 71:

<syntaxhighlight lang="flx">

def area(s: Shape): IntInt32 = match s {

case Circle(r) => 3 * (r * r)

case Square(w) => w * w

Line 83:

<syntaxhighlight lang="flx">

def twice(f: IntInt32 -> IntInt32): IntInt32 -> IntInt32 = x -> f(f(x))

</syntaxhighlight>

Line 114:

<syntaxhighlight lang="flx">

def point2d(): {x: IntInt32, y: IntInt32} = {x = 1, y = 2}

</syntaxhighlight>

Line 120:

<syntaxhighlight lang="flx">

def sum(r: {x: IntInt32, y: IntInt32 | rest}): Int = r.x + r.y

</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).