Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Fri 28 Sep 2018 11:00 - 11:30 at Illinois Central - Session 5 Chair(s): Niki Vazou

Many fancy types (e.g., generalized algebraic data types, type families)
require a type checker plugin. These fancy types have a type index
(e.g., type level natural numbers) with an equality relation that is
difficult or impossible to represent using GHC's built-in type equality. The
most practical way to represent these equality relations is through a plugin
that asserts equality constraints. However, such plugins are
difficult to write and reason about.

In this paper, we (1) present a formal theory of reasoning about the
correctness of type checker plugins for type indices, and, (2) apply this
theory in creating Thoralf, a generic and extensible
plugin for type indices that translates GHC constraint problems to queries to
an external SMT solver. By "generic and extensible", we mean the
restrictions on extending Thoralf are slight, and, if some type index could
be encoded as an SMT sort, then a programmer could extend Thoralf by
providing this encoding function.

Fri 28 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:00
Session 5Haskell at Illinois Central
Chair(s): Niki Vazou University of Maryland, USA
10:30
30m
Talk
Type Variables in Patterns
Haskell
Richard A. Eisenberg Bryn Mawr College, USA, Joachim Breitner DFINITY Foundation, Simon Peyton Jones Microsoft, UK
DOI
11:00
30m
Talk
The Thoralf Plugin: For Your Fancy Type Needs
Haskell
Divesh Otwani Haverford College, USA, Richard A. Eisenberg Bryn Mawr College, USA
DOI
11:30
30m
Talk
Suggesting Valid Hole Fits for Typed-Holes (Experience Report)
Haskell
Matthías Páll Gissurarson Chalmers University of Technology, Sweden
DOI