On the Rôle of Minimal Typing Derivations in Type-driven Program Transformation

Standard inference algorithms for type systems involving ML-style polymorphism aim at reconstructing most general types for all let-bound identifiers. Using such algorithms to implement modular program optimisations by means of type-driven transformation techniques generally yields suboptimal results. We demonstrate how this defect can be made up for by using algorithms that target at obtaining so-called minimal typing derivations instead. The resulting approach retains modularity and is applicable to a large class of polyvariant program transformations.