Flix (programming language): Difference between revisions

Revision as of 20:46, 1 October 2020

Revision as of 01:03, 7 October 2020

Line 14:

'''Flix''' is a [[functional programming|functional]], [[imperative programming|imperative]], and [[logic programming|logic]] [[programming language]] developed at [[Aarhus University]], with funding from the [[Danish_Council_for_Independent_Research|Independent Research Fund Denmark]]<ref>{{cite web |title=Forskningsprojekter |url=https://dff.dk/forskningsprojekter?SearchableText=functional+and+declarative+logic+programming&period%3Alist=all&instrument%3Alist=all&filed_method%3Alist=all |website=Danmarks Frie Forskningsfond |language=da}}</ref>, and by a community of [[open source]] contributors<ref>{{cite web |title=Flix Authors |url=https://github.com/flix/flix/blob/master/AUTHORS.md |website=GitHub |language=en}}</ref>. The Flix language supports [[algebraic data types]], [[pattern matching]], [[parametric polymorphism]], [[currying]], [[higher-order functions]], [[extensible records]]<ref>{{cite journal |last1=Leijen |first1=Daan |title=Extensible records with scoped labels |journal=Trends in Functional Programming}}</ref>, [[Communicating_sequential_processes|channel and process-based concurrency]], and [[tail call elimination]]. Two notable features of Flix are its type and effect system<ref name="oopsla2020a">{{cite journal |last1=Madsen |first1=Magnus |last2=van de Pol |first2=Jaco |title=Polymorphic Types and Effects with Boolean Unification|journal=Proceedings of the ACM on Programming Languages (OOPSLA 2020) |date=2020}}</ref> and its support for first-class Datalog constraints<ref name="oopsla2020b">{{cite journal |last1=Madsen |first1=Magnus |last2=Lhoták |first2=Ondřej |title=Fixpoints for the Masses: Programming with First-class Datalog Constraints |journal=Proceedings of the ACM on Programming Languages (OOPSLA 2020) |date=2020}}</ref>.

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 symposiumSymposium on Principles of programming languagesProgramming 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]] 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>{{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 }}</ref><ref>{{cite book |last1=Gong |first1=Qing |title=Extending Parallel Datalog with Lattice |publisher=Pennsylvania State University}}</ref>.

== Overview ==

Line 28:

Monomorphization avoids [[Value_type_and_reference_type|boxing]] of primitive values at the cost of longer compilation times and larger executable binaries. Flix has some support for interoperability with programs written in [[Java programming language|Java]]<ref>{{cite web |title=Programming Flix - Interoperability |url=https://doc.flix.dev/interoperability/ |website=flix.dev}}</ref>.

Flix supports [[tail call elimination]] which ensures that function calls in tail position never consume stack space and hence cannot cause the call stack to overflow<ref>{{cite journal |last1=Madsen |first1=Magnus |last2=Zarifi |first2=Ramin |last3=Lhoták |first3=Ondřej |title=Tail call elimination and data representation for functional languages on the Java virtual machine |journal=Proceedings of the 27th International Conference on Compiler Construction - CC 2018 |date=2018 |pages=139–150 |doi=10.1145/3178372.3179499|isbn=9781450356442 |s2cid=3432962 }}</ref>. Since the [[Java_bytecode_instruction_listings|JVM instruction set]] lacks explicit support for tail calls, such calls are emulated using a form of reusable stack frames<ref>{{cite journal |last1=Tauber |first1=Tomáš |last2=Bi |first2=Xuan |last3=Shi |first3=Zhiyuan |last4=Zhang |first4=Weixin |last5=Li |first5=Huang |last6=Zhang |first6=Zhenrui |last7=Oliveira |first7=Bruno C. D. S. |title=Memory-Efficient Tail Calls in the JVM with Imperative Functional Objects |journal=Programming Languages and Systems |series=Lecture Notes in Computer Science |date=2015 |volume=9458 |pages=11–28 |doi=10.1007/978-3-319-26529-2_2|isbn=978-3-319-26528-5 }}</ref>. Support for tail call elimination is important since all iteration in Flix is expressed through [[recursion]].

The Flix compiler disallows most forms of unused or redundant code, including: unused local variables, unused functions, unused formal parameters, unused type parameters, and unused type declarations, such unused constructs are reported as compiler errors<ref>{{cite web |title=Redundancies as Compile-Time Errors |url=https://flix.dev/blog/redundancies-as-compile-time-errors/ |website=flix.dev}}</ref>. [[Variable shadowing]] is also disallowed. The stated rationale is that unused or redundant code is often correlated with erroneous code<ref>{{cite journal |last1=Engler |first1=D. |title=Using redundancies to find errors |journal=IEEE Transactions on Software Engineering |date=October 2003 |volume=29 |issue=10 |pages=915–928 |doi=10.1109/TSE.2003.1237172}}</ref>.

Line 226:

=== First-class Datalog Constraints ===

Flix supports [[Datalog]] programs as first-class values<ref name="oopsla2020b"/><ref>{{cite web |title=Programming Flix - Fixpoints |url=https://doc.flix.dev/fixpoints/ |website=flix.dev}}</ref><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 }}</ref>. A Datalog program is a logic program that consists of a collection of unordered [[Fact|facts]] and [[Horn_clause|rules]]. Together, the facts and rules imply a [[minimal model]], 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: