In addition to what you see below, check out my GitHub page to
see what I've been working on recently.
- Make Haskell dependently typed. We propose an
update to FC, the internal language of GHC,
that brings kind equalities to the language. The new System FC merges types and kinds
and has the (*:*) axiom. The
(and extended version),
was published at ICFP 2013. I have implemented these ideas into
GHC 8.0. (Here is an unpublished paper
about the implementation.) Ongoing work includes adding proper Pi-types, as described in
- GHC Maintenance. As one of the core developers
of GHC, I often perform routine maintenance. I am also currently the Template
Haskell czar, overseeing the continued growth of that component of GHC. I have
implemented or have had a large hand in implementing the following GHC features:
- Levity polymorphism
- Template Haskell updates since 2012
- Closed type families
- Roles and Coercible
- Injective type families
- Visible type application
- The Data.Type modules in the standard library
Below are my less active projects. Most weeks do not involve any work on these,
but issues crop up now and again.
- singletons. This project supports the
singletons package, allowing
a limited form of dependently typed programming in current versions of Haskell. The
newest version of singletons supports the promotion of a wide array of term-level
functions to type families. See the
paper, published at Haskell Symposium, 2014. The original
paper resulting from this work was published
at the Haskell Symposium, 2012. With Jan Stolarek.
- glambda. Glambda is a lambda-calculus interpreter,
written using GADTs extensively. It is meant as a larger case study of how
GADTs can be used to make real, running code safer to run and easier to write.
- Roles. I implemented roles,
as described in our ICFP'14 paper and our draft JFP submission, into GHC.
the GeneralizedNewtypeDeriving bug, as described here. See also the wiki page on the subject. This work was completed while I was preforming an internship at Microsoft Research Cambridge, under the supervision of Simon
- units. This is a library, written using closed
type families, that allows for type-level dimensional analysis, to aid programs
written using units-of-measure. The most detailed description of this project
is in an experience report
published at Haskell Symposium 2014.
The project page is here.
With Takayuki Muranushi.
- Closed type families in
Haskell. What changes are necessary to the surface language and in GHC
to allow closed type families with ordered, overlapping equations? See
the paper (published at POPL'14)
and GHC wiki
page for more info. This feature is part of GHC 7.8 and above.
Peyton Jones, and Stephanie
- System FC in GHC. I maintain a formal specification
of the internal language within GHC here.