Palmer et al. (2024) -- Intensional Functions

The paper

Z. Palmer, N. W. Filardo, and K. Wu, “Intensional functions,” Proceedings of the ACM on Programming Languages, vol. 8, no. OOPSLA2, art. 274, 2024.

doi:10.1145/3689714

A summary of the paper and how gen uses it.

Palmer, Zachary, Nathaniel Wesley Filardo, and Ke Wu. “Intensional Functions.” Proc. ACM Program. Lang. 8, OOPSLA2, Article 274 (October 2024), 26 pages. https://doi.org/10.1145/3689714

Paper Summary

Functions in functional languages are extensional: they support a single elimination form (application) and cannot be compared, hashed, serialized, or subjected to any non-application operation. When algorithms need to deduplicate continuations, cache function results keyed by function identity, or transmit closures across process boundaries, programmers resort to manual defunctionalization (Reynolds 1972) — replacing functions with tagged first-order data and routing all calls through a dispatch function. This transformation is tedious, error-prone, far-reaching (transitively affecting all callers), and obscures program intent.

Palmer et al. introduce intensional functions, a language feature providing two new eliminators beyond application: identify (yielding the program point at which the function was defined) and inspect (producing the values captured in closure). Intensional functions carry a programmer-specified constraint function (e.g., Eq, Ord, Hashable) that bounds what operations can be performed on closure-captured values while simultaneously guaranteeing the function itself satisfies the same constraint. The syntax \%Ord x -> x + y creates an intensional function with Ord constraint; application uses %$ or %@.

The paper’s core formal contribution is the lambda-ITS calculus, a call-by-name lambda calculus with lazy substitution that makes closure environments explicit. Substitutions accumulate in the theta-position of lambda terms rather than being applied eagerly, making environments inspectable at runtime. The key formal result is closure consistency (Definition 5.6): for any two functions sharing the same program point (label l), if their substituted closures are equivalent, then their substituted bodies are equivalent. This is established through a chain of lemmas:

• Lemma 4.3 — function bodies are nonincreasing under evaluation (new environments appear but new code does not)
• Lemma 5.8 — initial programs (unique program points, canonical closures, empty substitutions) are closure consistent
• Lemmas 5.9-5.12 — closure consistency is preserved across evaluation steps
• Theorem 1 — any initial program remains closure consistent throughout execution
• Theorem 2 (Soundness) — the lambda-ITS type system is sound, proven via encoding into System F with GADTs

The practical consequence: conservative function equality by comparing program points and (substituted) closure environments is sound — functions deemed equal under this comparison always exhibit identical behavior. This is formally weaker than semantic equality (functions with different program points may still behave identically) but strong enough for deduplication.

Section 3 introduces intensional monads — a reconstruction of the functor hierarchy using intensional Kleisli arrows. The motivating example is an idempotent Search monad with indexed state: lookup retrieves values from an index, insert adds entries, and continuations bound via itsBind are intensional functions subject to Ord. This enables the monad to deduplicate redundant continuations by comparing their captured closures, pruning redundant computation paths in deductive closure algorithms.

The implementation (Haskell+ItsFn, a GHC 9.2 extension) demonstrates a 25% reduction in code versus manual defunctionalization on the Plume program analysis, at the cost of ~3x runtime overhead attributable to the proof-of-concept encoding (duplicate closure storage, linked-list traversal, unfused constraint dispatch). The authors argue this overhead is an engineering concern addressable by runtime integration, not a theoretical limitation.

Key Concepts

• Program-point identity (S2.2) — each intensional function carries a unique label l corresponding to its definition site in the source program. Two functions with the same l were defined at the same syntactic location.
• Closure inspection (S2.3) — the inspect eliminator yields the function’s captured environment as a list of type-tagged existential values, each carrying proof of the constraint function.
• Conservative equality (S2.3, S5.3) — two intensional functions are equal if they share the same program point AND their closures are element-wise equal. Sound but incomplete (false negatives possible, false positives impossible).
• Constraint functions (S5.1) — single-method typeclasses (Eq, Ord, Hashable) that bound closure-captured values. Both a requirement (all captured values must satisfy) and a guarantee (the function itself satisfies).
• Lazy substitution (S4) — substitutions accumulate in lambda terms’ theta-position rather than being applied eagerly. Bisimilar to traditional substitution but simplifies proofs about closure structure.
• Closure consistency (Def. 5.6) — the invariant that same-program-point functions differ only by substitutions, and equivalent substituted closures imply equivalent substituted bodies. Preserved throughout evaluation (Lemma 5.13).
• Intensional monads (S3) — monads whose bind takes intensional Kleisli arrows, enabling the monad implementation to compare, deduplicate, or otherwise inspect continuations.
• Intensional Search monad (S3) — indexed state with continuation dedup. Continuations watching the same index key with equal closures fire only once, pruning redundant computation in deductive closure algorithms.
• Saturation-aware application (S6.2) — fully-applied intensional functions need not construct closures, avoiding unnecessary constraint obligations at saturated call sites.
• Canonical closure (Def. 5.5) — a deterministic representation of a function’s free variables and free type variables as a packed list, ensuring closure representations are comparable across function instances.

How gen uses this

gen-algebra: intensional functions and conservative equality

mkIntensional hashIdentity registry ctor args (lib/intensional.nix) is an encoder in Palmer’s sense. The author names a constructor ctor in a registry and passes inert arguments args. The registry builds the function, so the closure is derived from the construction and cannot be under-supplied. The result carries the paper’s three eliminators:

• __functor (application), which calls registry.members.${ctor} args.
• name (identify, S2.2), the program point. It equals ctor, so it is constant across a constructor’s instances and is never used as a key on its own.
• closure (inspect, S2.3), which is args.

The identity is minted lazily in __mint, a digest over the registry coordinate, the constructor and the arguments. The minting function hashIdentity is passed in from gen-identity, gen’s one identity mint, which keeps gen-algebra free of dependencies.

conservativeEq a b is Palmer’s conservative equality (S2.3, Fig. 5), a conjunction over identity and closure. Two minted values compare by digest, which covers both conjuncts. Any other pair compares the values themselves under Nix ==, which on lambda-carrying values can only separate more pairs than Fig. 5 does. There is no name-only arm: comparing the program point alone would call two values with different closures equal, the direction S2.3 forbids. identityOf reads a value’s identity regime (minted, unmintable, or unmigrated), and isExact tells a caller whether the identity it got is an exact key.

gen-aspects: guards as first-order data

• Guard defunctionalization (S5.1) — lib/guard.nix gives guards a closed predicate vocabulary with one global applyGuard. The predicate is first-order data, so an aspect’s identity never has to hash a closure.
• Context closures refused — a raw function such as { host, ... }: { nixos = ...; } is told apart from a module function by canTake, which reads its formals without calling it, and is refused by name: it crosses the gen-rules door, which lowers it to a door node.
• Diamond dedup (S5.3, Lemma 5.12) — an aspect’s identity is its path key (lib/identity.nix). When one aspect is included through several paths, equal identities deduplicate its contributions.

gen-dispatch: rule identity

fromFunction turns a function into a rule. When the function is intensional (it has name, __functor and closure), the rule’s identity is derived from its minted identity. That identity is the rule’s override handle: a later rule can override it by identity. An unminted function gets no handle, and overriding it fails with an error naming it as an anonymous rule. Using the program-point name instead would give every instance of one constructor the same handle, so an override would replace the wrong rule.

gen-select: identified selectors

• sel.when fn wraps a lambda as a selector.
• isIdentified is true when a when selector wraps an intensional function (the name, __functor, closure shape), the paper’s runtime distinction between intensional and extensional functions.
• selectorEq compares two identified when selectors with gen-algebra’s conservativeEq, and returns false for any unidentified when selector, as extensional functions cannot be compared.

Further directions

Unexploited Ideas

Constraint function polymorphism (S2.4): The paper supports polymorphic constraint functions (\%c x y -> ... where c is a type variable). gen uses one fixed constraint on closures: they must be inert values the identity mint can encode. Parameterizing mkIntensional over constraint strategies could allow domain-specific equality.

Intensional monads (S3): The paper’s intensional monad reconstruction applies to any monad. Intensional State, Writer, or Reader monads could enable inspection and dedup of monadic computations, e.g. inspectable configuration transformations.

Saturation-aware application (S6.2): The paper’s optimization avoids constructing closures when all arguments are applied at once. In Nix, this maps to skipping mkIntensional wrapping when a function is called immediately rather than stored for comparison.

Runtime type comparison for heterogeneous closures (S5.1, E-Like/E-Unlike rules): The paper’s tyrep t1 ~ tyrep t2 ? e3 : e4 enables branch-aware type comparison of closure elements. This could let gen compare closures holding heterogeneous Nix values, including functions, where structural == gives no useful answer.

Research Directions

Nix as an intensional language: builtins.functionArgs already provides a limited form of function inspection (formal parameter names and whether each has a default). Whether Nix’s evaluation model (lazy, pure, attrset-based closures) could support deeper intensional functions without language changes is open.

Intensional identity and incremental evaluation: The paper’s Theorem 1 proves that identity is stable across evaluation steps. gen-identity’s identities are consistent within one evaluation and may differ across evaluations (a lazy source path mints a per-evaluation identity). Knowing which identities stay valid across evaluations would decide which cached results could be reused across them, connecting Palmer’s work to Mokhov et al. (2018).

Convergence bounds from intensional structure: Intensional identity bounds the number of distinct continuations (one per program point and closure). Formalizing this could yield termination bounds for gen’s fixpoint loops over rules, bounded by the number of identified rules.

Composition of intensional identity: When intensional functions are composed (f . g), what is the identity of the composition? The paper does not address this. A theory of compositional identity would let composed rules and composed attribute equations keep an identity, which they lose today.