Implicit Polarized F: local type inference for impredicativity

Henry Mercer, Cameron Ramsay, Neel Krishnaswami

System F, the polymorphic lambda calculus, features the principle of impredicativity: polymorphic types may be (explicitly) instantiated at other types, enabling many powerful idio…