Content deleted Content added
→Polymorphic effects: syntaxhighlight error fix |
Narky Blert (talk | contribs) dab-needed tag |
||
Line 20:
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]]{{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 }}</ref><ref>{{cite book |last1=Gong |first1=Qing |title=Extending Parallel Datalog with Lattice |publisher=Pennsylvania State University}}</ref>
== Overview ==
| |||