Wanted GHC feature: warn about unused constraints

Consider the following function:

foo :: (Show a, Ord a) => a -> a -> String
foo x y = show x ++ show y

Currently (as of GHC 7.2.1) when compiling this code with -Wall, no warnings are generated. But I’d really love to get a warning like

Foo.hs:1:1: Warning: Unused constraint: Ord a

I see no theoretical impediments here. At the level of fully desugared and elaborated GHC core, it is no harder to tell which constraints are unused than which arguments are unused, because constraints are arguments.

One possible objection is that there is some inherent ambiguity here. For example, consider:

bar :: (Eq a, Ord a) => a -> a -> String
bar x y | x == y    = "yay"
        | otherwise = "boo"

When elaborating bar, GHC has a free choice of where to get the needed (==) method: from the Eq constraint or from the Eq superclass of the Ord constraint. So we might get a warning about Eq being redundant or about Ord being redundant, depending on which one it decides to use. But I don’t see this as a big problem.

I think this could make for a nice project for someone wanting to dig into hacking on GHC. Perhaps I’ll do it myself at some point if no one else takes it on.

Typed type-level programming: status report

A few people have been bugging me (you know who you are ;-) about the current status of the project to allow automatic “lifting” of Haskell data constructors to the type level, to allow for typed type-level programming. I’ve written about it on this blog before (see here and here) and gave a talk about it in September at the Haskell Implementors’ Workshop (video, slides). So, there’s bad news, and there’s good news.

The bad news is that it is still pretty much vaporware (or vapourware I suppose) — there is not yet any actual code anywhere to do any actual automatic lifting! The good news is that it is still definitely being worked on. We (being Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Steve Zdancewic, and I) spent a bunch of time this summer trying to work out the theory of this extension, and I think we have some solid ideas. I then spent quite a lot of time refactoring GHC to make coercions a separate type from types (another interesting story in and of itself) which simply had to be done before we could make progress on this extension. Due to the magnitude of the task, some problems with darcs, and plain old busyness, that refactoring work has only recently been fully merged with the current GHC HEAD, although it is not yet pushed to the HEAD since there are still some kinks to iron out! But once that is done we can get started with the work to actually implement auto-lifting.

Back from Baltimore

I’m finally back in Philly after attending ICFP, the Haskell Symposium, and the Haskell Implementors’ Workshop in Baltimore. I enjoyed meeting every person I met, so if I met you please feel free to instantiate the universal quantifier.

• Here’s a link to my Haskell Symposium paper, Species and Functors and Types, Oh My!. My talk seemed to be well-received, and it was videotaped, but unfortunately I think it’s going into the ACM Digital Library, which you need a subscription to access. Here are the slides, at least, although they don’t make all that much sense by themselves. I had several people ask me what I used to make the slides; it was a combination of inkscape and my diagrams EDSL.
• Here are links to the slides and video of my talk from the Haskell Implementors’ Workshop, Typed type-level functional programming with GHC.

Improving GHC’s constraint solving

So I’ve been here at MSR Cambridge for almost two weeks now (!), working in the Programming Principles and Tools Group with Simon Peyton-Jones and Dimitrios Vytiniotis — and also collaborating with Stephanie Weirich and Steve Zdancewic, who are also in Cambridge. So, what have I been doing?

This week, Simon, Dimitris, and I have been having a major GHC hacking session, implementing the new constraint-solving type inference engine described in their new OutsideIn(X) paper. It’s been a lot of fun — I’ve never hacked on GHC before, and it’s quite a new experience hacking on such a large (and amazing) piece of software. I’ve been working on the constraint canonicaliser, which puts constraints into canonical forms appropriate for the constraint simplifier to work with. As a simple example, the equality constraint (Int, a) ~ (b, Char) gets decomposed into the primitive constraints Int ~ b and a ~ Char. It’s also responsible for flipping and flattening equality constraints so that type function applications only happen on the left-hand side: for example, the constraint F a b ~ G Int (where both F and G are type families), gets rewritten to a pair of constraints F a b ~ c, G Int ~ c, where c is a fresh variable. If we didn’t do this it would lead to problems with termination: for example, the constraint a ~ [F a] could lead to infinite rewriting of a to [F a] to [F [F a]] to… (And before you protest that we ought to just throw out a ~ [F a] on the grounds that it is recursive, note that F a may not mention a at all; for example, perhaps F is defined by F [x] = Int.)

Constraints also include type class constraints and implicit parameter constraints, although there’s much less work to do with those as far as canonicalisation is concerned.

Next week, I’ll likely get back to our other, more ambitious research project, but I’ll write more about that next time. In the meantime, if you’re in or near Cambridge and want to meet up, just drop me a note!