I propose unifying functional and logic/relational programming by treating predicates/relations as functions equipped with their support – the set of inputs whose output is non-false. For instance, the logic programming language Datalog, in which all relations are finite, is a language of finitely supported boolean functions. Finite support allows representing the function, not as code, but as data – as a table of input-output pairs – making bulk operations more efficient. If we combine finitely supported functions, represented as data, and higher order functions, represented as code, in the same language, we get what I call finite functional programming. To this end, I demonstrate a simple type system to check finite support by treating variable grounding as a graded effect.

A 30-minute talk slot is fine. I expect to discuss the work-in-progress type system, some issues with it, possible connections with related work that I don’t fully understand and so maybe someone can help me to flesh out, and maybe potential implementation strategies or semantics if there’s time.