Eta Conversion for the Unit Type - Is Still Not That Simple

Watch a 28-minute conference talk from WITS 2025 workshop where András Kovács from the University of Gothenburg and Chalmers University of Technology explores the challenges of implementing eta-conversion for the unit type in programming languages. Learn why this seemingly simple feature with established formal metatheory is rarely supported in practical implementations, as it requires type-aware conversion that complicates the preferred syntax-directed approach. Discover improved designs proposed by the speaker that promise to be significantly faster than Agda's current implementation (the only major system attempting to support this feature) while guaranteeing unique solutions to unification problems. This presentation was sponsored by ACM SIGPLAN and delivered at the WITS 2025 workshop on January 20, 2025.