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 Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:40 | Functional Programming and CorrectnessPLDI Research Papers at Aula Master Chair(s): Francesco LogozzoFacebook | ||
14:00 25mTalk | Compiling without continuations PLDI Research Papers 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 25mTalk | FunTAL: Reasonably Mixing a Functional Language with Assembly PLDI Research Papers Daniel PattersonNortheastern University, Jamie PercontiNortheastern University, Christos DimoulasHarvard University, USA, Amal AhmedNortheastern University, USA Media Attached | ||
14:50 25mTalk | HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics PLDI Research Papers Shumo ChuUniversity of Washington, USA, Konstantin WeitzUniversity of Washington, USA, Alvin CheungUniversity of Washington, Dan SuciuUniversity of Washington Media Attached | ||
15:15 25mTalk | Levity Polymorphism PLDI Research Papers Media Attached |