My Haskell-related research is mainly situated at the intersection between Functional and Constraint Programming. Topics are:
The aim of this project is to model the generic aspects of Constraint Programming in Haskell. You find more information on the MCP page.
Limitations of monad stacks get in the way of developing highly modular programs with effects. This pearl demonstrates that Functional Programming's abstraction tools are up to the challenge. Of course, abstraction must be followed by clever instantiation: Huet's zipper for the monad stack makes components jump through unanticipated hoops.
Advice is a mechanism, widely used in aspect-oriented languages, that allows one program component to augment or modify the behavior of other components. When advice and other components are composed together they become tightly coupled, sharing both control and data flows. However this creates important problems: modular reasoning about a component becomes very difficult; and two tightly coupled components may interfere with the control and data flows of each other.
This paper presents EffectiveAdvice, a disciplined model of advice, inspired by Aldrich's Open Modules, that has full support for effects. With EffectiveAdvice, equivalence of advice, as well as base components, can be checked by equational reasoning. The paper describes EffectiveAdvice as a Haskell library in which advice is modeled by mixin inheritance and effects are modeled by monads. Interference patterns previously identified in the literature are expressed as combinators. Parametricity, together with the combinators, is used to prove two harmless advice theorems. The result is an effective semantic model of advice that supports effects, and allows these effects to be separated with strong non-interference guarantees, or merged as needed.
Ongoing work concerns the simplification of type checking for Haskell's extensive type system, and adding new extensions. This is joint work with Martin Sulzmann, Simon Peyton Jones Manuel Chakravarty, Stefan Monnier, Louis-Julien Guillemette, Dimitrios Vytiniotis and Dominic Orchard.
Haskell's multi-parameter type classes, together with functional dependencies, allow the specification of complex type-level operations, and the recent introduction of open type families in GHC makes such type-level programming even more accessible and flexible. But type-level code is special in that its correctness is crucial to the safety of the program; so except in those cases simple enough for the type checker to see trivially that the code is correct (or harmless), type-level programs need to come with their specification and correctness proof. In this article, we propose an extension to Haskell that allows the specification of invariants for type classes and open type families, together with accompanying evidence that those invariants hold. To accommodate the open nature of type classes and type families, the evidence itself needs to be open and every subcase of the proof can be provided independently from the others.
We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the paper is that we identify and characterise the key technical challenge of entailment checking; and we give a novel, decidable, sound, and complete algorithm to solve it, together with some practically-important variants. Our system is implemented in GHC, and is already in active use.
We present a new extension of the Haskell type system: functional programming at the type-level, with type functions. Type functions interact in interesting ways with Haskell's two other type system features: type classes and GADTs. Moreover, we show how they can be used to substitute functional dependencies. The typechecker's job now requires full-blown equational reasoning rather than simple Herbrand term unification. With some reasonable conditions on the type functions we can show that typechecking is still decidable; our algorithm constructs a strongly normalizing TRS. As a side effect of rewriting we generate proof terms, which serve as coercions for System FC. The whole system has been implemented in GHC and will be available shortly.
Haskell-style functional dependencies allow the programmer to influence the type inference process by automatically deriving type improvement rules from class and instance declarations. Previous work demands that the dependency must fully cover all type parameters of a type class to guarantee confluence. Confluence is an important property to ensure that type inference is well-behaved. We restore confluence for non-full functional dependencies by giving a novel encoding of functional dependencies in terms of type families as supported by the Glasgow Haskell Compiler. We compare our method against another alternative constraint-propagation encoding due to Claus Reinke. Our work provides new insights in the connection between functional dependencies and type families, and in the relative trade-offs of rewriting based or constraint-propagation based type inference approaches.