Levity Polymorphism
Parametric polymorphism is one of the lynchpins of modern typed programming. A function that can work seamlessly over a variety of types simplifies code, helps to avoid errors introduced through duplication, and and is easy to maintain. However, polymorphism comes at a very real cost, one that each language with support for polymorphism has paid in different ways. This paper describes this cost, proposes a theoretically simple way to reason about the cost—that kinds, not types, are calling conventions—and details one approach to dealing with polymorphism that works in the context of a language, Haskell, that prizes both efficiency and a principled type system.
This approach, levity polymorphism, allows the user to abstract over calling conventions; we detail and verify restrictions that are necessary in order to compile levity-polymorphic functions. Levity polymorphism has opened up surprising new opportunities for library design in Haskell.
Tue 20 Jun
14:00 - 15:40: PLDI Research Papers - Functional Programming and Correctness at Aula Master Chair(s): Francesco LogozzoFacebook | ||||||||||||||||||||||||||||||||||||||||||
14:00 - 14:25 Talk | Luke MaurerUniversity of Oregon, USA, Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft Research, Cambridge Media Attached | |||||||||||||||||||||||||||||||||||||||||
14:25 - 14:50 Talk | Daniel PattersonNortheastern University, Jamie PercontiNortheastern University, Christos DimoulasHarvard University, USA, Amal AhmedNortheastern University, USA Media Attached | |||||||||||||||||||||||||||||||||||||||||
14:50 - 15:15 Talk | Shumo ChuUniversity of Washington, USA, Konstantin WeitzUniversity of Washington, USA, Alvin CheungUniversity of Washington, Dan SuciuUniversity of Washington Media Attached | |||||||||||||||||||||||||||||||||||||||||
15:15 - 15:40 Talk | Media Attached |