flix/flix

The Flix Programming Language

Flix is a statically typed functional, imperative, and logic programming language.

We refer you to the official Flix website (flix.dev) for more information about Flix.

Example

Building

See docs/BUILD.md.

License

Flix is available under the Apache 2.0 license.

Sponsors

We kindly thank EJ Technologies for providing us with JProfiler and JetBrains for providing us with IntelliJ IDEA.

flix's Issues

Efficient solver

Reduce Interpreter Overhead

The Solver and Indexed Collections are now fairly optimized.

Thus now the Interpreter is becoming visible in the profiler. Currently it uses 28% of the time on the SUBench.

We should look for cheap optimization opportunities.

Implement set literals, expressions and operations in interpreter.

See title.

Never use wildcard pattern matches in compiler/runtime

We should avoid code like this:

def foo(e: Expression) = e match {
  case ... =>
  case _ => 
}

Since when a new type of expression is added the compiler will not issue any warnings about a missing case!

Typechecking NativeParity fails

>> No lattice declared for '#ca.uwaterloo.flix.util.misc.NativeParity'.

32|    lat VarPointsTo(localVal: Int, value: #ca.uwaterloo.flix.util.misc.NativeParity<>);
                                      ^^^^^
Tip: Associate a lattice with the type.

But the lattice is defined.

Performance Table

Fill out the performance table in the paper.

"SLOC" is number of lines of code taken from the original POPL 11 Strong Update paper.
"Input Facts" is the number of input facts.
"Total Facts" is the sum of the size of all the relations.
"Time" (under Flix) is the solver time.

If a benchmark doesn't work just put "err" in the cols. (or fix it, if possible).
If the analysis times out (lets say we give it at most 15min) then put "timeout" and don't look at any larger programs.

IFDS/IDE

Implement IFS/IDE in Flix

Revisit the int/str/tag caches

Right now we're using regular HashMaps to cache Value.Int, Value.Str, and Value.Tag. (See #7.)

This is a problem because the cache will continue growing and eat up all our memory.

We'll want to use a smarter hash, either by using something from a library, or implementing our own cache that uses weak or soft references. (A WeakHashMap isn't exactly what we want -- the keys and not the values are held by weak references).

Implement evalHeadTerm, evalBodyTerm, eval2 and evalCall

In an efficient way, convince yourself they are correct and write unit tests.

negative integer constants

Flix program:

  rel foo(i: Int)
  foo(-1).

Output:

Exception in thread "main" java.lang.RuntimeException: Invalid input '-', expected AscribeTerm or BaseTerm (line 3, column 7):
  foo(-1).
      ^

Support iteration over sets in rules

We want to be able to write something like:

R(a) :- A(x, y, z), a <- f(x,  y, z).

Implement newtype

Basically Haskell's newtype (so not a type alias). See how Haskell implements this.

See: http://learnyouahaskell.com/functors-applicative-functors-and-monoids#the-newtype-keyword

Annotations for strictness, monotonicity, etc.

In a program:

lat IntVar(x: Var, v: Parity);

IntVar(x, sum(v1, v2)) :-  ...

The sum function must be monotone and strict.
It may be distributive (and I guess have other properties we have not yet looked at).

We can infer that it must be strict and monotone, but I think we should allow and even require explicit "type" annotations to state so. My reason is the same for requiring functions to be type-annotated: It tells you about the behaviour of function and it is modular.

So, we could allow or enforce that you write:

def sum(e1: @strict @mono Parity, e2: @strict @mono Parity): Parity = ...

A short hand might be:

@strict @mono
def sum(e1: Parity, e2: Parity): Parity = ...

If all arguments must be strict and monotone.

The meaning of these annotations could be any mixture of:

(1) The compiler checks that any function used in a rule is declared @strict and @mono.
(2) The compiler uses the annotations to decide what functions are subject to the verifier. (So, if you put the annotation, the compiler tries to verify it. If you leave it out, the compiler does nothing).
(3) The compiler is allowed to use distributiveness if the @distributive annotation is present, and so on for other properties.

ArrayIndexOutOfBoundsException when running SUdatalog2

Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: 2
    at ca.uwaterloo.flix.runtime.Solver$$anonfun$ca$uwaterloo$flix$runtime$Solver$$cross$1$1.apply(Solver.scala:196)
    at ca.uwaterloo.flix.runtime.Solver$$anonfun$ca$uwaterloo$flix$runtime$Solver$$cross$1$1.apply(Solver.scala:190)
    at scala.collection.Iterator$class.foreach(Iterator.scala:750)
    at scala.collection.AbstractIterator.foreach(Iterator.scala:1202)
    at ca.uwaterloo.flix.runtime.Solver.ca$uwaterloo$flix$runtime$Solver$$cross$1(Solver.scala:190)
    at ca.uwaterloo.flix.runtime.Solver.evalBody(Solver.scala:252)
    at ca.uwaterloo.flix.runtime.Solver.solve(Solver.scala:92)
    at ca.uwaterloo.flix.Flix$$anonfun$fromPaths$1.apply(Flix.scala:41)
    at ca.uwaterloo.flix.Flix$$anonfun$fromPaths$1.apply(Flix.scala:40)
    at ca.uwaterloo.flix.util.Validation$class.map(Validation.scala:20)
    at ca.uwaterloo.flix.util.Validation$Success.map(Validation.scala:250)
    at ca.uwaterloo.flix.Flix$.fromPaths(Flix.scala:40)
    at ca.uwaterloo.flix.Main$.main(Main.scala:20)
    at ca.uwaterloo.flix.Main.main(Main.scala)

I tried with 470.lbm and 256.bzip2 as inputs.

Type aliases

How do I make a type alias?

In the old Flix, I had:

//(def-type Object Str)
//(def-type Variable Str)
//(def-type Location Str)

That creates three new types that are considered distinct by the type
checker, but they are implemented internally as strings. Is this
possible in the new Flix language?

Support Native Fields and Methods in Rules

For example,

P(#foo.bar.baz)

or

P(#foo.bar.baz(x)) :- #filter.me(x, y, z).

Intern Values

Wildcard allowed in TypedAst.Term.Body?

In #16, the implementation for TypedAst.Term.Body.Wildcard is not yet implemented because there might be a mistake in the AST.

Interoperability

The current JVM interop was bolted on in a week, so we should do something better. For example, the Flix program could be written with a mapping of Flix names to native names (i.e. native declarations).

The current implementation uses reflection and only works with static methods/values.

In the old Flix, we passed objects with apply: Value => Value defined which could be directly called by Flix.

Other considerations: JVM type erasure and annotating Flix types, whether we want to expose the concept of Flix values to native methods (we probably don't want to do this).

Possible bug in interpreter?

Evaluating the following (from Parity.flix)

// we can test whether a number may be zero:
def isMaybeZero(e: Parity): Bool = match e with {
    case Parity.Bot    => false;
    case Parity.Odd    => false;
    case Parity.Even   => true;
    case Parity.Top    => true;
};

with the argument Parity.Even seems to yield false.

Can you confirm?

IndexedLattice NoSuchElementException:

When compiling the following flix file, I get the following exception:

namespace SU {

//// Inputs
//// =========
  rel AddrOf(variable: Str, object: Str)
  rel Copy(to: Str, from: Str)
  rel Store(label: Str, to: Str, from: Str)
  rel Load(label: Str, to: Str, from: Str)
  rel CFG(label: Str, to: Str, from: Str)

//// Outputs
//// =========
  rel Pt(variable: Str, target: Str)
  rel PtSU(location: Str, object: Str, target: Str)

//// Other types
//// =========
  enum SULattice {
    case Top,
    case Single(Str),
    case Bottom
  }

  lat SUBefore(location: Str, object: Str, target: SULattice<>)
  lat SUAfter(location: Str, object: Str, target: SULattice<>)

  rel PtH(object: Str, target: Str)
  rel KillEmpty(location: Str)
  rel KillNot(location: Str, object: Str)
  rel AllObject(object: Str)
  rel NonStore(location: Str)
}

Exception in thread "main" java.util.NoSuchElementException: key not found: Enum(Map(Top -> Tag(/SU::SULattice,Top,Unit), Single -> Tag(/SU::SULattice,Single,Str), Bottom -> Tag(/SU::SULattice,Bottom,Unit)))
    at scala.collection.MapLike$class.default(MapLike.scala:228)
    at scala.collection.AbstractMap.default(Map.scala:59)
    at scala.collection.MapLike$class.apply(MapLike.scala:141)
    at scala.collection.AbstractMap.apply(Map.scala:59)
    at ca.uwaterloo.flix.runtime.datastore.IndexedLattice$$anonfun$2.apply(IndexedLattice.scala:21)
    at ca.uwaterloo.flix.runtime.datastore.IndexedLattice$$anonfun$2.apply(IndexedLattice.scala:20)
    at scala.collection.immutable.List.map(List.scala:273)
    at ca.uwaterloo.flix.runtime.datastore.IndexedLattice.<init>(IndexedLattice.scala:20)
    at ca.uwaterloo.flix.runtime.datastore.DataStore$$anonfun$2.apply(DataStore.scala:39)
    at ca.uwaterloo.flix.runtime.datastore.DataStore$$anonfun$2.apply(DataStore.scala:33)
    at scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:778)
    at scala.collection.immutable.HashMap$HashMap1.foreach(HashMap.scala:221)
    at scala.collection.immutable.HashMap$HashTrieMap.foreach(HashMap.scala:428)
    at scala.collection.immutable.HashMap$HashTrieMap.foreach(HashMap.scala:428)
    at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:777)
    at ca.uwaterloo.flix.runtime.datastore.DataStore.<init>(DataStore.scala:33)
    at ca.uwaterloo.flix.runtime.Solver.<init>(Solver.scala:64)
    at ca.uwaterloo.flix.Flix$.solve(Flix.scala:34)
    at ca.uwaterloo.flix.Main$.main(Main.scala:9)
    at ca.uwaterloo.flix.Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:497)
    at com.intellij.rt.execution.application.AppMain.main(AppMain.java:140)

Implement proper semi naive evaluation and tuple-at-a-time

Strong Update Analysis

I want to implement the SU analysis using the efficient encoding with a lattice of type: Option[Map[Loc, Set[X]]] (If I recall correctly.). Ondrej, can you please:

(1) Specify what set and map operations you need [1].
(2) Sketch an implementation.

We already have some set stuff, which you can see here:
https://github.com/magnus-madsen/flix/blob/master/main/src/ca/uwaterloo/flix/language/ast/Operator.scala

Specify formal semantics of Flix

parser rejects function with no parameters

In IDE.flix, I replaced the Identity relation with an id() function that takes zero arguments (6011adf).

Now the parser runs for a very long time, but eventually it errors out with:

-- PARSE ERROR ------------------------------------------------- examples/analysis/IDE.flix

Invalid input ')', expected AscribeTerm or BaseTerm (line 120, column 23):
JumpFn(d3,start,d3,id()) :-
                      ^

type checking fails to check arity

I have the following:

  rel Pt(variable: Str, target: Str)
KillEmpty(l) :- Store(l,p,q), Pt(p,a,b).

Notice that the arity of Pt is 2, but in the rule, it appears with three arguments. Flix silently ignores the error.

Nested Sets and Aggregates/Unfolds

The current version of Flix supports neither set terms/expressions nor aggregates/unfolds.

The literature is rich on aggregation in Datalog and the like, and I was hoping we could leave this for future work.

Unfortunately, the IFDS/IDE and SU analyses all seem to need this.

In the case of IFDS/IDE we need a mechanism which can evaluate a native method which returns a set of tuples and unfold that into a collection (relation/lattice).

In SU the issue is that to give a monotone function we must compute the intersection of Singleton(s) and the flow insensitive set of pointers. However, to get this set, we must either have aggregation or set terms/expressions.

Write Flix benchmark programs

Write several small Flix programs which use a large set of facts to benchmark Flix performance.

Support Sets in Value / Interpreter

We need to support sets in our implementation. At least in some limited form.

The first step is to decide what set operations we want in the first implementation.

Pattern matching in cases

How do I do deep pattern matching in a match/case?

  enum SULattice {
    case Top,
    case Single(Str),
    case Bottom
  }

  def leq(e1: SULattice, e2: SULattice): Bool = match (e1, e2) with {
    case (Bottom, _) => true;
    case (_, Top) => true;
    case (Single(s1), Single(s2)) => s1 == s2;
    case _ => false;
  }

I get the parse error:

Exception in thread "main" java.lang.RuntimeException: Invalid input '(', expected "::", '.', ''', AlphaNum, '_' or optWS (line 27, column 17):
    case (Single(s1), Single(s2)) => s1 == s2;
                ^

Definition of rel/lat

Allow users to define relations and lattices like:

rel SumOp(result: Int, left: Int, right: Int);
lat VarPointsTo(localVal: Int, value: Parity<>);

IDE analysis include Bottom in results

The IDE analysis that I've committed runs correctly (same as with the old Flix) except for one thing. The results for the Result relation contain the line:

| n1    | x    | /IDE::Value.Bot(()) |

Shouldn't it be impossible to ever have bottom as an explicit lattice value (since bottom is the silent default)? If this is correct, then what is the distinction between a relation that maps a key to an explicit bottom and a relation that doesn't map that key to anything?

Flix interface

Improve the Flix class s.t. it can be used for unit tests.

SU analysis on LLVM/SPEC benchmarks

I have found the input relations from the SU POPL 2011 and committed them to git.

The main program for them is SUbench.flix, slightly extended from SU.flix.

I am not yet sure whether it give correct results. I have some suspicion that they're incorrect. For comparison, I need to run the same input relations through LogicBlox, and my LB licence key expired. I have requested and am waiting for a new LB key.

The smallest benchmark is 470 lbm. In C++ (LLVM), the analysis time is 0.05 s. In Flix, the analysis time is 3.5 s. If I remember correctly, in LB, the time was on the order of one minute.

The second-smallest benchmark is 256 bzip2. In C++ (LLVM), the analysis time is 0.08 s. In Flix, the analysis time is 4.6 s. If I remember correctly, LB did not complete on this input.

Pretty printing

Can we come up with a uniform place to put all pretty printing, that doesnt involve attaching it to ast nodes, types or values themselves?

Native Tuples

We should support boxing to/from Scala's scala.Tuple2 to Flix' Value.Tuple when used with native functions.

Thread-safe Interpreter

At some point the solver will be multi-threaded, so the interpreter must also be thread-safe. This includes making Value thread-safe.

Specialize the interpreter to primitive types.

Expressions in head terms

If we only allow variables in the head terms, but allow a where clause in the rule for complicated expressions, we would have something like this:

A(y, x) :- B(w), ...
    where
      y = f(g(w))
      z = ...
      x = w

We probably want the variables in the head and the body to be disjoint.

Other considerations: deconstruction/pattern matching in the where clause, looping (<-), lattices.

Flix output not a fixed point (violates one of the rules)

I have implemented the SU analysis in b5ef325. When I run it, the final result violates one of the rules.

Notice the rule SUAfter(l,a,t) :- SUBefore(l,a,t), KillEmpty(l).

Notice that the SUBefore output contains: | l7 | a | /SU::SULattice.Singlec |

Notice that the KillEmpty output contains: | l7 |

But the SUAfter output contains: | l7 | a | /SU::SULattice.Singlee |

But Single(c) is not <= Single(e). Therefore, the output should contain their join: l7, a, Top.

use binary indexes in IndexRelation /IndexLattice

Replace every occurrence of Seq[Int] by a binary encoding of the same sequence.

Look for an IntMap implementation which doesn't use boxing.

Flix values from JVM code

Allow the user to write a JVM function that returns a Flix value.

For example,

In Java:

class Main {
  public static ca.uwaterloo.flix.runtime.Value.Int Foo  = ca.uwaterloo.flix.runtime.Value.mkInt(1)
}

In Flix:

val x: Int = #Main.foo

Refering to inner classes in native code

I can't seem to refer to inner classes:

// Flix
def scalaHi(i: Int): #ca.uwaterloo.flix.runtime.Value.Int =
    #ca.uwaterloo.flix.util.misc.ScalaNative.hi(i)

- REFERENCE ERROR -------------------------------------------------- ./examples/misc/NativeTest.flix

>> The class name: 'ca.uwaterloo.flix.runtime.Value.Int' was not found.

328|    def scalaHi(i: Int): #ca.uwaterloo.flix.runtime.Value.Int =
                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Tip: Check your class path.

Also, the error is printed twice.

This isn't a blocking issue, because scalaHi should return an Int, not a #ca.uwaterloo.flix.runtime.Value.Int. But we should fix this at some point.

unresolved type when referencing enum type

I have:

  enum Value {
    case Top,
    case Cst(Int),
    case Bot
  }
  enum Transformer {
    case BotTrans,
    case NonBotTrans(Int,Int,Value)
  }

I get:

>> Unresolved reference to type '?Value'.

33|    case NonBotTrans(Int,Int,Value)
                                ^^^^^

Native stuff

We need to support Flix accessing native Java/Scala fields/methods/classes.

Proposed syntax:

    val edges: Native = #ca.uwaterloo.Foo;

    VarPointsTo(x, y) :- y \in edges(x).

    let #ca.uwaterloo.Foo<> = (#ca.uwaterloo.Bot, #ca.uwaterloo, ...)

    def foo(x: #ca.uwaterloo.Foo): #ca.uwaterloo.Foo

    lat Foo(k: Int, #ca.uwaterloo.Foo<>)

• Extend front-end
  • parser
  • weeder
  • namer
  • typer
• Extend backend
  • interpreter
  • value

Compute source positions more efficiently.

The Parser contains the following code:

  @Unoptimized
  def SP: Rule1[SourcePosition] = {
    val position = Position(cursor, input)
    val line: String = input.getLine(position.line)
    rule {
      push(SourcePosition(source, position.line, position.column, line))
    }
  }

The call to Position(cursor, input) scans through the entire input to compute the line and column number. Since this is called thousands upon thousands times during the parse it really slows down the parser.

A better solution is to pre-compute some kind of map from offsets to line numbers.

Improvements to the Interpreter

• Thrown an exception if no rule matches in matchRule.
• Use only a single mutable map in unify. (The pattern is linear).
• Avoid ++, map, zip in evalCall.
• Write special code to handle this case in the solver:

      val args = terms.map(t => Interpreter.evalBodyTerm(t, row))
      val result = Interpreter.evalCall(lambda.exp, args, sCtx.root, row).toBool

• Add arrays

Lattice definitions

Required operators: Bot, Leq, Lub
Sort of optional: Top, Glb
Optional: Norm, Narrow, Widen

Also decide on syntax, e.g.:
let Parity<>.leq = leq or leq[Parity] = leq

Performance

• TypedAst -> A Normal Form IR
• CodeGen for Integer expressions.
• CodeGen for functions.
• CodeGen for rules.
• Integer representation of values.

repeated variables in match cases

In the old Flix, you could write:

        (case <(NonBotTrans <a b c1>) (NonBotTrans <a b c2>)> ...)
        (case <(NonBotTrans <a1 b1 c2>) (NonBotTrans <a2 b2 c2>)> ...)

The first case would match only if the two NonBotTrans'es had the same values of their first and second parameter. The second case would match only if the two NonBotTrans'es had the same value of their third parameter. There was no additional case, so if neither of these were true, we would get a runtime error.

Are there any plans to support this in the new Flix?

I can rewrite with if statements. It's more messy.

Also, is there a way to do assert(false) (to indicate an error at runtime)?