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

10:30 - 12:00: Haskell 2018 - Session 5 at Illinois Central
Chair(s): Niki VazouUniversity of Maryland, USA
haskellsymp-2018-papers10:30 - 11:00
Richard A. EisenbergBryn Mawr College, USA, Joachim BreitnerDFINITY Foundation, Simon Peyton JonesMicrosoft, UK
haskellsymp-2018-papers11:00 - 11:30
Divesh OtwaniHaverford College, USA, Richard A. EisenbergBryn Mawr College, USA
haskellsymp-2018-papers11:30 - 12:00
Matthías Páll GissurarsonChalmers University of Technology, Sweden