La teoria delle lenti (Hancock, Ordinals and Interactive Programs, 2000) formalizza la corrispondenza intuita da Gentzen, che associa ai tipi su cui un sistema formale può applicare il principio di induzione le funzioni rappresentabili (equivalentemente, i buoni ordini provabili) nel sistema. La generalizzazione di tale corrispondenza, attraverso alcuni concetti e risultati provenienti dalla teoria dei dilatatori, fornisce una prospettiva "dinamica" per lo studio della teoria impredicativa dei tipi (sistema F).