Haskell

Overview

My Haskell-related research is mainly situated at the intersection between Functional and Constraint Programming. Topics are:

• types: type checking, type inference, type system design
• EffectiveAdvice: reasoning about component interference
• monadic constraint programming

Monadic Constraint Programming

The aim of this project is to model the generic aspects of Constraint Programming in Haskell. You find more information on the MCP page.

EffectiveAdvice

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.

• EffectiveAdvice: Disciplined Advice with Explicit Effects, T. Schrijvers, K.U.Leuven PLT seminar. [slides]
• EffectiveAdvice: Overview, background and proofs, B. Oliveira, T. Schrijvers, W. Cook. [technical report]

Types

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.

Material

• Let Should Not Be Generalized, D. Vytiniotis, S. Peyton Jones, T. Schrijvers. Accepted at TLDI 2010.
• Haskell Type Constraints Unleashed, D. Orchard, T. Schrijvers. [draft pdf]
• Complete and Decidable Type Inference for GADTs, T. Schrijvers, S. Peyton Jones, M. Sulzmann, D. Vytiniotis. Presented at ICFP 2009. [draft ,seminar at Radboud University]
• Type Invariants for Haskell, T. Schrijvers, L.-J. Guillemette, S. Monnier. Presented at PLPV 2009. [pdf,slides] [Details] [Hide details]

  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.

• Type Checking with Open Type Functions, T. Schrijvers, S. Peyton Jones, M. Chakravarty, M. Sulzmann. Presented at ICFP 2008. [pdf ,slides] [Details] [Hide details]

  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.

  • Towards Open Type Functions for Haskell, T. Schrijvers, M. Sulzmann, S. Peyton Jones, and M. Chakravarty. Presented at IFL 2007. [slides] [slides with Haskell intro] [IFL paper] [GHC Documentation] [Examples] [pptx] [Details] [Hide details]

    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.

• Unified Type Checking for Type Classes and Type Families, T. Schrijvers, M. Sulzmann. Presented at the ICFP 2008 poster session. [abstract, poster design]
• Confluence for Non-Full Functional Dependencies, T. Schrijvers, M. Sulzmann. Accepted for the TFP 2008 post-proceedings. [full paper]
  • Restoring Confluence for Functional Dependencies, T. Schrijvers, M. Sulzmann. Accepted at TFP 2008. [full paper,abstract, slides] [Details] [Hide details]

    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.

• Type inference for GADTs via Herbrand constraint abduction, M. Sulzmann, T. Schrijvers, P. J. Stuckey. Now available as a technical report. [report]