Typed holes support in Template Haskell

Back in April I found myself in a need for typed holes in Template Haskell. To my disappointment it turned out that typed holes are not implemented in TH. Sadly, this happens too often: a feature is added to GHC but no Template Haskell support is implemented for it. This was the time when I was working on injective type families and I already had some experience in extending TH implementation. I figured that adding support for typed holes should be a trivial task, no more than 30 minutes of coding. I created a feature request on Trac and started coding. I quickly realized that it won’t be that simple. Not that the amount of required work was that extensive. I simply tripped over the way GHC handles names internally. As a result the work got stalled for several months and I only finished it two weeks ago thanks to help from Richard Eisenberg.

My patch allows you to do several interesting things. Firstly, it allows to quote typed holes, ie. expressions with name starting with an underscore:

[d| i :: a -> a
    i x = _ |]

This declaration quote will represent _ using an UnboundVarE constructor. Secondly, you can now splice unbound variables:

i :: a -> a
i x = $( return $ VarE (mkName "_") )
j :: a -> a
j x = $( return $ UnboundVarE (mkName "_") )

Notice that in a splice you can use either VarE or UnboundVarE to represent an unbound variable – they are treated the same.

A very important side-effect of my implementation is that you can actually quote unbound variables. This means that you can now use nested pattern splices, as demonstrated by one of the tests in GHC testsuite:

baz = [| \ $( return $ VarP $ mkName "x" ) -> x |]

Previously this code was rejected. The reason is that:

  1. nested pattern splice is not compiled immediately, because it is possible that it refers to local variables defined outside of the bracket;
  2. the bracket is renamed immediately at the declaration site and all the variables were required to be in scope at that time.

The combination of the above means that the pattern splice does not bring anything into scope (because it is not compiled until the outer bracket is spliced in), which lead to x being out of scope. But now it is perfectly fine to have unbound variables in a bracket. So the above definition of baz is now accepted. When it is first renamed x is treated as an unbound variable, which is now fine, and when the bracket is spliced in, the inner splice is compiled and it correctly brings binding for x into scope. Getting nested pattern splices to work was not my intention when I started implementing this patch but it turned out we essentially got this feature for free.

One stumbling block during my work was typed Template Haskell. With normal, untyped TH I can place a splice at top-level in a file:

$$(return [
   SigD (mkName "m")
        (ForallT [PlainTV (mkName "a")]
                 (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a"))))
 , FunD (mkName "m")
        [Clause [VarP (mkName "x")] (NormalB (VarE (mkName "x"))) [] ]

and this will build a definition that will be spliced into the source code. But converting this into a typed splice, by saying $$(return ...., resulted in compiler panic. I reported this as #10945. The reason turned out to be quite tricky. When Template Haskell is enabled, top-level expressions are allowed. Each such expression is treated as an implicit splice. The problem with typed TH splice is that it doesn’t really make sense at the top-level and it should be treated as an implicit splice. Yet it was treated as an explicit splice, which resulted in a panic later in the compiler pipeline.

Another issue that came up with typed TH was that typed holes cannot be quoted, again leading to panic. I reported this as #10946. This issue has not yet been solved.

The above work is now merged with HEAD and will be available in GHC 8.0.

Week at ICFP: Injective Type Families merged into GHC HEAD

I spent last week at Vancouver, Canada attending Haskell Implementors Workshop, ICFP and the Haskell Symposium. Yesterday I gave a talk on injective type families, described also in my previous post. Slides are on my web page but the talk itself is not yet online. Day prior to the talk I finally managed to merge the injective type families branch, which means that this feature is definitely making it into the next stable release of GHC. (In case you haven’t heard this will be GHC 8.0, not 7.12.)

My next plans include extending injective type families to fully match expressiveness of functional dependencies, as outlined in Section 7.2 of the injectivity paper. I also hope to finally implement support for typed holes in Template Haskell. The patch was supposed to be trivial and I started working on it several months ago. But then I ran into several problems with it and abandoned it to focus on ITFs.

Injective type families for Haskell

For the last few months I have been working on extending Glasgow Haskell Compiler with injective type families. At first this seemed like a fairly simple project but in the end it turned out to be much more interesting than initially thought. (I suppose that’s how research mostly turns out.) There are still some rough edges in the implementation and it will take a few more weeks before my branch gets merged into the master development branch of GHC. But for now there is a draft paper “Injective type families for Haskell” written by me, Simon Peyton Jones, and Richard Eisenberg, that we submitted for this year’s Haskell Symposium. This is not yet the final version of the paper so any feedback will be appreciated.

The idea behind injective type families is to infer the arguments of a type family from the result. For example, given a definition:

type family F a = r | r -> a where
    F Char = Bool
    F Bool = Char
    F a    = a

if we know (F a ~ Bool)1 then we want to infer (a ~ Char). And if we know (F a ~ Double) then we want to infer (a ~ Double). Going one step further from this, if we know (F a ~ F b) then – knowing that F is injective – we want to infer (a ~ b).

Notice that in order to declare F as injective I used new syntax. Firstly, I used “= r” to introduce a name for the result returned by the type family. Secondly, I used syntax borrowed from functional dependencies to declare injectivity. For multi-argument type families this syntax allows to declare injectivity in only some of the arguments, e.g.:

type family G a b c = r | r -> a c

Actually, you can even have kind injectivity, assuming that type arguments have polymorphic kinds.

Obviously, to make use of injectivity declared by the user GHC needs to check that the injectivity annotation is true. And that’s the really tricky part that the paper focuses on. Here’s an example:

type family T a = r | r -> a where
    T [a] = a

This type family returns the type of elements stored in a list. It certainly looks injective. Surprisingly, it is not. Say we have (T [T Int]). By the only equation of T this gives us (T [T Int] ~ T Int). And by injectivity we have ([T Int] ~ Int). We just proved that lists and integers are equal, which is a disaster.

The above is only a short teaser. The paper covers much more: more corner cases, our algorithm for verifying user’s injectivity annotations, details of exploiting knowledge of injectivity inside the compiler and relationship of injective type families to functional dependencies. Extended version of the paper also comes with proofs of soundness and completeness of our algorithm.

  1. ~ means unification. Think of “~” as “having a proof that two types are equal”. []

Staypressed theme by Themocracy