Post #2196148
2026-05-07 16:58 UTC
I have a new paper with @mwillsey!
"Finite Functional Programming" (https://arxiv.org/abs/2604.26161) combines functional programming with relational/tensor algebra using functions of finite support: Datalog relations are finite boolean functions; tensors are finite real-valued funs. We ensure finite support of λ-terms using graded effects to check grounding, and relevance types (the "use at least once" cousin of linearity) to check relational/tensor operations preserve "absence" appropriately.
Replies (1)
-
@rntz@recurse.social 2026-05-07 16:59
I have lots of future work in mind here: I hope to implement this with indexed streams (https://arxiv.org/abs/2507.06456) / fairly seekable iterators (https://arxiv.org/abs/2510.26016v1); and to generalize from finiteness to other degree constraints (https://arxiv.org/pdf/2504.02770), eg functional dependencies and cardinality constraints, cf https://recurse.social/@rntz/116529665044883799