We unify functional and logic programming by treating predicatesas functions equipped with their support: the set of inputs whose output is nonzero. Datalog, for instance, is a language of finitely supported boolean functions. Finite support allows representing functions as input-output tables. Generalizing from boolean functions to other pointed sets neatly handles aggregation and weighted logic programming. We refer to the combination of finitely supported functions, represented as data, with higher order functions, represented as code, as finite functional programming. We give a simple type system to check finite support, using graded effects to check variable grounding and relevance types to model pointed sets.

翻译：我们将谓词视为带有支撑集（输出非零的输入集合）的函数，从而统一了函数式与逻辑编程范式。例如，Datalog 是一种有限支撑布尔函数语言。有限支撑使得函数可以表示为输入-输出表。从布尔函数推广到其他带基点集合，可以优雅地处理聚合与加权逻辑编程。我们将基于数据的有限支撑函数与基于代码的高阶函数相结合，称为有限函数式编程。我们给出一个简单的类型系统来检查有限支撑，使用分级效果检查变量接地性，并通过相关性类型对带基点集合进行建模。