Finite functional programming via graded effects and relevance types
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.
Sun 12 OctDisplayed time zone: Perth change
11:00 - 12:30 | |||
11:00 30mTalk | Contractions Are Abstractions - Towards Effective Memory Management in ReML HOPE Martin Elsman University of Copenhagen | ||
11:30 30mTalk | Finite functional programming via graded effects and relevance types HOPE Michael Arntzenius UC Berkeley | ||
