Finite functional programming via graded effects and relevance types
summary
Proposes treating relations as functions equipped with their support so Datalog-style relations become finitely supported maps that can be represented as tables and queried like database joins. Gives a concrete type discipline: pointed sets, nil-preserving functions, graded (co)monads and a relevance-context (use-at-least-once) typing that enforces finite support and lets operations like exists, sum and joins run as table operations. Work-in-progress type rules handle currying, two product forms and aggregations; no full implementation yet, but prior macros at RelationalAI motivate feasibility.
AI-written summary · about
chapters (10)
- 0:00Finite functional programming intro
- 1:25Higher-order relational motivation
- 6:03Finitely supported functions
- 11:30Graded effects and co-monads
- 14:17Point-preserving maps and relevance
- 23:48Typing rules for support maps
- 31:34Examples vs relevance typing
- 37:59Aggregations in weighted logic
- 40:08Recursion challenges in relational
- 48:25Q&A
related talks
50mFunctional Programming with Effects
43mFunctional Programming with Effects
27mThe Relative Monadic Metalanguage
21mGraded Monoids for Dependently Typed Array Programming
33mExtensible Effects: A Leaner Cake for Purely Functional Code
46mFunctional effects in perspective
16mSyntax-Generic Operations, Reflectively Reified (Extended Abstract)
14mFundamentalist Functional Programming