kirancodes.me
To Proof Maintenance & Beyond!

Levity polymorphism

Richard A. Eisenberg, Simon Peyton Jones

Abstract

Parametric polymorphism is one of the linchpins of modern typed programming, but it comes with a real performance penalty. We describe this penalty; offer a principled way to reason about it (kinds as calling conventions); and propose levity polymorphism. This new form of polymorphism allows abstractions over calling conventions; we detail and verify restrictions that are necessary in order to compile levity-polymorphic functions. Levity polymorphism has created new opportunities in Haskell, including the ability to generalize nearly half of the type classes in GHC's standard library.

DOI 10.1145/3062341.3062357

Related papers