Notice

The website of Tom Schrijvers has moved to http://people.cs.kuleuven.be/~tom.schrijvers. Please adjust any links you maintain as this copy will be taken down shortly.


Haskell

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

  • Monadic Constraint Programming: constraint programming in Haskell
  • The Monad Zipper: modular components with effects
  • EffectiveAdvice: reasoning about component interference
  • Types: type checking, type inference, type system design

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.

  • Monads, Zippers and Views: Virtualizing the Monad Stack, T. Schrijvers, B. Oliveira. Download pdf
  • Modular Components with Monadic Effects, T. Schrijvers, B. Oliveira. Presented at IFL 2010. Download pdf
  • Functional Pearl: The Monad Zipper, T. Schrijvers, B. Oliveira. Unpublished draft. Download pdf
  • Hackage release of Monatron, with the Monad Zipper.

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, B. Oliveira, T. Schrijvers, W. Cook. Download pdf
  • 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. Download pdf

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.

  • OutsideIn(X): Modular type inference with local assumptions D. Vytiniotis, S. Peyton Jones, T. Schrijvers, M. Sulzmann. To appear in JFP. Download pdf
  • Let Should Not Be Generalized, D. Vytiniotis, S. Peyton Jones, T. Schrijvers. Accepted at TLDI 2010. Download pdf
  • Haskell Type Constraints Unleashed, D. Orchard, T. Schrijvers. Accepted at FLOPS 2010. Download pdf
  • Complete and Decidable Type Inference for GADTs, T. Schrijvers, S. Peyton Jones, M. Sulzmann, D. Vytiniotis. Presented at ICFP 2009. Download pdf ,seminar at Radboud University
  • Type Invariants for Haskell, T. Schrijvers, L.-J. Guillemette, S. Monnier. Presented at PLPV 2009. Download pdf,slides [Details]
  • Type Checking with Open Type Functions, T. Schrijvers, S. Peyton Jones, M. Chakravarty, M. Sulzmann. Presented at ICFP 2008. Download pdf ,slides [Details]
    • 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 pptx [Details]
  • 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. Download pdf
    • Restoring Confluence for Functional Dependencies, T. Schrijvers, M. Sulzmann. Accepted at TFP 2008. Download pdf,abstract, slides [Details]
  • Type inference for GADTs via Herbrand constraint abduction, M. Sulzmann, T. Schrijvers, P. J. Stuckey. Now available as a technical report. Download pdf