A type system for finitely supported functions via pointed sets (Part 2)

Abstract

Finite maps, in the form of dictionaries, associative arrays, or tables, are a key data type in most language’s standard libraries, but constructing and manipulating them is generally very explicit and loopful. In this talk I’ll demonstrate work in progress on a type system that can guarantee that functions written directly as lambda-expressions are finitely supported, and therefore can be represented as tables. This yields a higher-level, more declarative syntax, similar to logic programming languages or database query languages.
The semantics of my language live in Set, the category of pointed sets and point-preserving maps. In order to define the support of a function f: A → B, one needs a point nil ∈ B; then support f = {x ∈ A : f x ≠ nil}. In fact, finitely supported maps form a graded monad on Set; they are graded by their domain A. To fully flesh out the semantics and type system, I also need the free/forgetful adjunction between Set and Set*.
Unfortunately the typing rules get quite complex. I’d like to know if there’s a simpler way to accomplish the same goals, or a simpler or more general framework for presenting the type system itself.
Paper preprint for the interested: https://www.rntz.net/files/finite-functional-programming.pdf