Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Wed 26 Sep 2018 16:52 - 17:15 at Stifel Theatre - Dependent Types Chair(s): David Thrane Christiansen

Dependently typed languages are well known for having a problem with code reuse. Traditional non-indexed algebraic datatypes (e.g. lists) appear alongside a plethora of indexed variations (e.g. vectors). Functions are often rewritten for both non-indexed and indexed versions of essentially the same datatype, which is a source of code duplication.

We work in a Curry-style dependent type theory, where the same untyped term may be classified as both the non-indexed and indexed versions of a datatype. Many solutions have been proposed for the problem of dependently typed reuse, but we exploit Curry-style type theory in our solution to not only reuse data and programs, but do so at zero-cost (without a runtime penalty). Our work is an exercise in dependently typed generic programming, and internalizes the process of zero-cost reuse as the identity function in a Curry-style theory.

Wed 26 Sep
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

16:30 - 17:15: Dependent TypesResearch Papers at Stifel Theatre
Chair(s): David Thrane ChristiansenGalois, USA
16:30 - 16:52
Elaborating Dependent (Co)pattern Matching
Research Papers
Jesper CockxChalmers | University of Gothenburg, Andreas AbelGothenburg University
16:52 - 17:15
Generic Zero-Cost Reuse for Dependent Types
Research Papers
Larry Diehl, Denis FirsovUniversity of Iowa, USA, Aaron StumpThe University of Iowa, USA