Characterizing functions mappable over GADTs
summary
An algorithm takes a term t and a type-formula specification Phi and returns constraints that exactly characterize which functions are mappable over t; it treats mapping relative to a specification Phi (not just the datatype), performs unification when needed, and can produce nontrivial requirements like "only the identity" in examples where constructors fix data (e.g., Nat inside a GADT). The paper includes surprising counterexamples, formal-function intermediates, and an Agda implementation as proof of concept.
AI-written summary · about