Promoting functions to type families in Haskell

It’s been very quiet on the blog these past few months not because I’m spending less time on functional programming but precisely for the opposite reason. Since January I’ve been working together with Richard Eisenberg to extend his singletons library. This work was finished in June and last Friday I gave a talk about our research on Haskell Symposium 2014. This was the first time I’ve been to the ICFP and Haskell Symposium. It was pretty cool to finally meet all these people I know only from IRC. I also admit that the atmosphere of the conference quite surprised me as it often felt like some sort of fan convention rather than the biggest event in the field of functional programming.

The paper Richard and I published is titled “Promoting Functions to Type Families in Haskell”. This work is based on Richard’s earlier paper “Dependently typed programming with singletons” presented two years ago on Haskell Symposium. Back then Richard presented the singletons library that uses Template Haskell to generate singleton types and functions that operate on them. Singleton types are types that have only one value (aside from bottom) which allows to reason about runtime values during compilation (some introduction to singletons can be found in this post on Richard’s blog). This smart encoding allows to simulate some of the features of dependent types in Haskell. In our current work we extended promotion capabilities of the library. Promotion is only concerned with generating type-level definitions from term-level ones. Type-level language in GHC has become quite expressive during the last couple of years but it is still missing many features available in the term-level language. Richard and I have found ways to encode almost all of these missing features using the already existing type-level language features. What this means is that you can write normal term-level definition and then our library will automatically generate an equivalent type family. You’re only forbidden from using infinite terms, the do-notation, and decomposing String literals to Chars. Numeric literals are also very problematic and the support is very limited but some of the issues can be worked around. What is really cool is that our library allows you to have partial application at the type level, which GHC normally prohibits.

You can learn more by watching my talk on YouTube, reading the paper or the singletons documentation. Here I’d like to add a few more information that are not present in the paper. So first of all the paper was concerned only with promotion and didn’t say anything about singletonization. But as we enabled more and more language constructs to be promoted we also made them singletonizable. So almost everything that can be promoted can also be singletonized. The most notable exception to this rule are type classes, which are not yet implemented at the moment.

An interesting issue was raised by Adam Gundry in a question after the talk: what about difference between lazy term-level semantics and strict type-level semantics? You can listen to my answer in the video but I’ll elaborate some more on this here. At one point during our work we were wondering about this issue and decided to demonstrate an example of an algorithm that crucially relies on laziness to work, ie. fails to work with strict semantics. I think it’s not straightforward to come up with such an algorithm but luckily I recalled the backwards state monad from Philip Wadler’s paper “The essence of functional programming”1. Bind operator of that monad looks like this (definition copied from the paper):

m `bindS` k = \s2 -> let (a,s0) = m s1
                         (b,s1) = k a s2
                     in  (b,s0)

The tricky part here is that the output of call to m becomes input to call to k, while the output of call to k becomes the input of m. Implementing this in a strict language does not at all look straightforward. So I promoted that definition expecting it to fail spectacularly but to my surprised it worked perfectly fine. After some investigation I understood what’s going on. Type-level computations performed by GHC are about constraint solving. It turns out that GHC is able to figure out in which order to solve these constraints and get the result. It’s exactly analogous to what happens with the term-level version at runtime: we have an order of dependencies between the closures and there is a way in which we can run these closures to get the final result.

All of this work is a small part of a larger endeavour to push Haskell’s type system towards dependent types. With singletons you can write type-level functions easily by writing their definitions using the term-level language and then promoting these definitions. And then you can singletonize your functions to work on singleton types. There were two other talks about dependent types during the conference: Stephanie Weirich’s “Depending on Types” keynote lecture during ICPF and Richard’s “Dependent Haskell” talk during Haskell Implementators Workshop. I encourage everyone interested in Haskell’s type system to watch both of these talks.

  1. The awful truth is that this monad does not really work with the released version of singletons. I only realized that when I was writing this post. See issue #94 on singletons bug tracker. []

5 Responses to “Promoting functions to type families in Haskell”

  1. Adam Gundry says:

    Thanks for this, I enjoyed your talk and it’s amazing to see the progress you and Richard have made on this work. I was meaning to catch you afterwards to talk more about the semantics question, but there was just too much happening!

    You’re right that I was oversimplifying in my question: the type-level reduction order isn’t really strict, it is more like a (pattern-matching variant of) full beta-reduction. My point is that for proper dependent pi-types, what we’d really like is some kind of agreement between the two reduction orders, but that’s hard to achieve with type families as currently formulated.

  2. Jan Stolarek says:

    Well, we can always have an email (or comment) conversation although that’s not the same as talking face to face :-)

    for proper dependent pi-types, what we’d really like is some kind of agreement between the two reduction orders

    Yes, you’re probably right. I think Richard has more to say about this one as he’s the one implementing dependent Haskell.

  3. Gershom Bazerman says:

    Here is a post I sent to -cafe some years ago describing the type of problem that Adam is talking about: http://www.haskell.org/pipermail/haskell-cafe/2011-July/093974.html

    I understand test cases were built out of this and for this particular issue performance is better in both formulations. However, it definitely seems that we still do not have a clear guide as to _which_ reduction order we can/should necessarily expect. As my example shows, this can certainly lead to surprises in compile-time performance. I hope this example can help in examining the issue.

    Thanks for the enjoyable talk and exciting progress.

  4. Jan Stolarek says:

    Gershom, these are brilliant examples! The truth is we did not investigate the performance of algorithms after promotion. Our focus was to encode as much features as possible without too much regard to performance, since this is mostly intended as a research-grade solution. It seems that I might have given the wrong answer to Andres Löh by stating that the computational complexity after promotion should not change. I’m not sure if any of the issues demonstrated in your mail to H-Cafe occur in our code but at least now I have a concrete example that demonstrates that complexity of an algorithm might change after promoting it to the type level.

    One thing that I did not mention in the presentation due to time limitations was that we also perform a pre-processing step that simplifies language features that are just syntactic sugar into simpler expressions. For example guards are turned into case expressions and where clauses are turned into let statements. That’s why in the end we’re only concerned with promoting case expressions, let statements and lambdas. This is similar to how GHC compiles Haskell into Core. During this desugaring some of the original source code expressions might be turned into suboptimal ones which might affect performance of the promoted code. This desugaring is also a direct cause of the backwards state monad not promoting with the released version of singletons. In the earlier stages of our work we did not have this desugaring step and this monad promoted perfectly fine.

  5. Jan Stolarek says:

    I did some performance measurements. Joachim Breitner suggested that functions like scanr can become slower due to loss of sharing. Here’s how compilation time depends on the size of input to promoted scanr:

    8: ~0.48s
    16: ~0.51s
    32: ~0.7s
    64: ~1.6s
    128 ~ 6.4s
    256 ~ 94s (sic!)
    300 ~ 154s

    Last two results look bad. So it seems that my answer to Andres was wrong – computational complexity does change. It is however not yet clear to me whether this results from our preprocessing, which turns scanr into something possibly slower, or from the promotion itself.

Leave a Reply

(required)

Staypressed theme by Themocracy