Granite: Compositional Functional Logic Programming
summary
Granite puts a join as semilattice primitive at the language core, letting parallel executions merge by associative commutative idempotent joins; it encodes deterministic parallelism like LVars, cyclic datatypes and Datafun-style functional logic, and open recursion via joined functions to extend mutually recursive definitions. Evaluation uses Datalog-style least-fixpoint iteration (tabled recursion) to compute transitive closure and reachability and to model distributed protocols; an interpreter in Haskell and a mechanized Iris semantics exist, and examples (parallel-or, bookshop two-node) work but the runtime sometimes approximates nontermination.
AI-written summary · about
chapters (17)
- 0:00Granite language intro
- 1:25Join operation in Granite
- 3:32Parallel or with joins
- 6:22Recursive functions with joins
- 7:27Compositionality with families
- 7:48Evaluating recursive definitions
- 11:21Cyclic graphs in Granite
- 13:05Distributed systems modeling
- 18:44Bookshop eventual consistency
- 23:43Current work and future
- 24:50Summary and closing
- 25:10Q&A implementation
- 26:12Q&A mutual recursion
- 27:17Q&A transitive closure
- 28:41Q&A nested fix points
- 29:06Granite vs Datalog
- 30:11Q&A parallel or recursion
related talks
49mQuantitative program reasoning in Granule via graded modal types
47mLogic Programming à la Carte
28mElements of Logic Programming in a Concatenative Functional Language
17mDenotation-based Compositional Compiler Verification
26mA Rule-Based Approach for Designing and Composing Abstract Domains
12mOn the power of syntactic methods: It is all syntax after all…
49mSemantic Foundations for Probabilistic Programming
18mEpistemic Logic for Polyglots (Short Paper)