Handling properly calculi with sum types and case expressions is a difficult task as soon as one wants to take into account the commuting conversions that are so useful in performing program optimizations: there is no canonical rewriting system for calculi including such features, and performing optimization via partial evaluation was an open problem. In this paper we present a notion of canonical form for a lambda calculus with sum types, and we prove, via a sophisticated categorical construction, that any program has an equivalent canonical form.
We then use ideas coming form the categorical contruction to
present for the first time a type directed partial evaluator
able to construct the canonical form associated to any well-typed program.
