Flix (programming language): Difference between revisions

Revision as of 01:33, 10 January 2021

Revision as of 19:16, 16 January 2021

Line 21:

The Flix type and effect system supports [[Hindley–Milner type system|Hindley-Milner]]-style [[type inference]]. The system separates pure and impure code: if an expression is typed as pure then it cannot produce an effect at run-time. Higher-order functions can enforce that they are given pure (or impure) function arguments. The type and effect system supports [[effect polymorphism]]<ref>{{cite journal |last1=Lucassen |first1=J. M. |last2=Gifford |first2=D. K. |title=Polymorphic effect systems |journal=Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '88 |date=1988 |pages=47–57 |doi=10.1145/73560.73564|isbn=0897912527 |s2cid=13015611 }}</ref><ref>{{cite journal |last1=Leijen |first1=Daan |title=Koka: Programming with Row Polymorphic Effect Types |journal=Electronic Proceedings in Theoretical Computer Science |date=5 June 2014 |volume=153 |pages=100–126 |doi=10.4204/EPTCS.153.8|arxiv=1406.2061 |s2cid=14902937 }}</ref> which means that the effect of a higher-order function may depend on the effect(s) of its argument(s).

Flix supports [[Datalog]] programs as [[First-class citizen|first-class]] values. A Datalog program value, i.e. a collection of Datalog facts and rules, can be passed to and returned from functions, stored in data structures, and composed with other Datalog program values. The [[Minimal model program|minimal model]]{{dn|date=December 2020}} of a Datalog program value can be computed and is itself a Datalog program value. In this way, Flix can be viewed as a [[metaprogramming|meta programming]] language for Datalog. Flix supports [[Stratification (mathematics)#In mathematical logic|stratified negation]] and the Flix compiler ensures stratification at compile-time.<ref name="Programming Flix - Fixpoints">{{cite web |title=Programming Flix - Fixpoints |url=https://doc.flix.dev/fixpoints/ |website=flix.dev}}</ref> Flix also supports an enriched form of Datalog constraints where predicates are given [[Lattice (order)|lattice]] semantics.<ref>{{cite journal |last1=Madsen |first1=Magnus |last2=Yee |first2=Ming-Ho |last3=Lhoták |first3=Ondřej |title=From Datalog to flix: a declarative language for fixed points on lattices |journal=ACM SIGPLAN Notices |date=August 2016 |volume=51 |issue=6 |pages=194–208 |doi=10.1145/2980983.2908096}}</ref><ref>{{cite journal |last1=Madsen |first1=Magnus |last2=Lhoták |first2=Ondřej |title=Safe and sound program analysis with Flix |journal=Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis - ISSTA 2018 |date=2018 |pages=38–48 |doi=10.1145/3213846.3213847|isbn=9781450356992 |s2cid=49427988 }}</ref><ref>{{cite journal |last1=Keidel |first1=Sven |last2=Erdweg |first2=Sebastian |title=Sound and reusable components for abstract interpretation |journal=Proceedings of the ACM on Programming Languages |date=10 October 2019 |volume=3 |issue=OOPSLA |pages=1–28 |doi=10.1145/3360602|s2cid=203631644 |doi-access=free }}</ref><ref>{{cite book |last1=Gong |first1=Qing |title=Extending Parallel Datalog with Lattice |publisher=Pennsylvania State University}}</ref>

== Overview ==

Line 171:

The requirement that <code>f</code> must be impure ensures that the code makes sense: It would be meaningless to call <code>List.foreach</code> with a pure function since it always returns <code>Unit</code>.

The type and effect is [[sound]]{{dn|date=January 2021}}, but not [[complete]]{{dn|date=January 2021}}. 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="flx">

Line 195:

</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]]{{dn|date=January 2021}} 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 boolean expressions to control the purity of function arguments.

Line 231:

=== First-class datalog constraints ===

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 |doi-access=free }}</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 program|minimal model]]{{dn|date=January 2021}}, 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.

The following edge facts define a graph: