Write a Blog >>
Tue 20 Jun 2017 15:15 - 15:40 at Aula Master - Functional Programming and Correctness Chair(s): Francesco Logozzo

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
25m
Talk
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
25m
Talk
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
25m
Talk
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
25m
Talk
Levity Polymorphism
PLDI Research Papers
Richard A. EisenbergBryn Mawr College, USA, Simon Peyton JonesMicrosoft Research, Cambridge
Media Attached