Ordered overlapping type family instances

I am pleased to announce that I have pushed my implementation of ordered overlapping type family instances to GHC HEAD.

This blog post is a literate Haskell file. Copy and paste into a .lhs file to try out this code. This file will only compile with GHC HEAD, however.

We need some header formalities:

> {-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeOperators #-}
> import Prelude hiding (zipWith)

The Problem

When writing term-level functions, it is natural to write a series of equations, each using a sequence of patterns to select which equation should be triggered when calling the function. Critically for this discussion, the first matching equation is used. Let’s use a particularly favorite function of mine as an example:

> import Prelude hiding (zipWith)
> 
> zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
> zipWith f (a:as) (b:bs) = (f a b):(zipWith f as bs)
> zipWith _ _      _      = []

Let’s try to naively write this function at the type level on promoted lists:

type family ZipWith (f :: a -> b -> c) (as :: [a]) (bs :: [b]) :: [c]
type instance ZipWith f (a ': as) (b ': bs) = (f a b) ': (ZipWith f as bs)
type instance ZipWith f as        bs        = '[]

Urk. We get the following error:

Conflicting family instance declarations:
  ZipWith k k k f ((':) k a as) ((':) k b bs)
  ZipWith k k k f as bs

(The repetition of the variable k is incorrect, and has been reported as GHC bug #7524. This is not the issue we are pursuing here, however.)

The problem is really that type instance declarations are essentially unordered. The order in which they appear in a file is irrelevant to GHC. Relatedly, a programmer can define instances of the same type family in multiple modules. With separate compilation, the lack of ordering and the overlap check are necessary for type soundness. This is quite different from term-level function definition equations. All equations defining the same function not only have to be in the same module, but they must be one right after another.

The particular example here has an easy solution. Because we are matching over a closed kind ([a] at the kind level), we could simply expand out the different cases we wish to match against. However, this solution is not possible when matching over an open kind, such as *. We’ll see a useful example of overlap involving * shortly.

The Solution

GHC HEAD now contains an implementation for ordered overlapping type family instances. The example above can be written thus:

> type family ZipWith (f :: a -> b -> c) (as :: [a]) (bs :: [b]) :: [c]
> type instance where
>   ZipWith f (a ': as) (b ': bs) = (f a b) ': (ZipWith f as bs)
>   ZipWith f as        bs        = '[]

More interestingly, we can now define this:

> type family Equals (a :: k) (b :: k) :: Bool
> type instance where
>   Equals a a = True
>   Equals a b = False

Ordered overlapping type family instances allow us to define a general, write-once use-everywhere Boolean equality at the type level. Yay!

This new form of type family instance also seems to close the biggest known gap between the expressivity of functional dependencies and type families: functional dependencies have long supported overlap (through OverlappingInstances or IncoherentInstances) that type families could not. Although functional dependencies’ overlap requires ordering based on specificity and type families’ overlap is based on an explicit ordering, it would seem that any code that took advantage of functional dependencies and overlap can now be translated to use overlapping type families.

Details

  • type instance where does not work with associated types. Class instances can be sprinkled across modules, and having this form of overlap appear across modules would not be type safe in the presence of separate compilation.
  • type instance where does not work with associated types, even when the overlap is intended to exist just within one instance. There is no great reason for this restriction, but it seemed unimportant. Yell if this matters to you.
  • Choosing which equation in a group to use is somewhat delicate. For example, consider the Equals type family. What if we want to simplify Equals a Int? Well, we can’t. That’s because a might (sometimes) be instantiated to Int, and if we simplified Equals a Int to False, we would have a type soundness issue. So, perhaps counterintuitively, we can’t simplify even Equals a b to False until a and b are known.

This GHC wiki page gives an outline of how to get GHC compiling on your machine so you can play with this feature in HEAD. I don’t imagine it will be in 7.6.2, but I believe it will be in 7.8.1, whenever that is released. Enjoy, and please post any feedback!

Acknowledgments

Many thanks to Simon Peyton Jones, Dimitrios Vytiniotis, and Stephanie Weirich for getting me started and helping me think through some of the finer points.

About these ads

9 thoughts on “Ordered overlapping type family instances

  1. Richard Eisenberg Post author

    AntC tried to post the following, but was unable to. He emailed me instead. Here are his words, verbatim, with his permission:

    Hi Richard,

    Thank you, that’s a great Christmas present. At last we can
    implement HLists and extensible records within type
    families!

    (I would have posted this on your announcement page, but
    ‘Leave a reply’ isn’t letting me.)

    The type-level Equals example is terrific.

    I’m a bit puzzled, though, by your ZipWith example. (I’ll
    try this out when I have a chance.)

    Without invoking your ordered/group instances development,
    can’t we do the following as separate instances?:

    type instance ZipWith f (a ‘: as) (b ‘: bs) = (f a b)
    ‘: (ZipWith f as bs)
    type instance ZipWith f ‘[] bs = ‘[]
    type instance ZipWith f as ‘[] = ‘[]

    The second and third instances don’t overlap the first.
    They do overlap each other, but the result is confluent.

    We’re taking advantage of knowing that if the first instance
    won’t match, then either `as’ is an empty list, or `bs’ (or
    both).

    Is this something to do with the Coincident Overlap
    discussion on the wiki? I think Chak’s discussion that
    refers to is over-ambitious, but (again when I find time)
    I’d try this for the Plus example:

    type instance Plus (Succ m’) (Succ n’) = Succ (Succ
    (Plus m’ n’))
    type instance Plus Zero n = n
    type instance Plus m Zero = m

    AntC

    Reply
    1. Richard Eisenberg Post author

      My response:

      I of course agree that ZipWith can easily be written at the type level without my extension, as I noted in the post. I used it to draw a distinction with term-level programming, but perhaps it was confusing to start with an example that doesn’t require the extension.

      As for your last example, that will work, but more general formulations of Plus don’t. If you try to make a consistent story that allows type family expansion before checking for RHS coincident overlap, you quickly end up needing to write a general automated theorem prover. Or, at least we (Stephanie Weirich, Simon PJ, and I) thought so. I do think some solution to that problem will eventually come to light, but not yet, unfortunately.

      Reply
  2. Andy Adams-Moran

    This is just what I was looking for; thanks! Being able to define a type-level type equality so
    neatly is very powerful. When combined with -XTypeOperators, -XDataKinds, and -XPolyKinds, one can write some truly beautiful type-level functions, safely. It feels like writing Agda with Haskell syntax.

    What if one wanted a more relaxed equivalence? For example, perhaps we’d like to consider any application of type constructor F equivalent:

    > type instance where
    > Equiv a a = True
    > Equiv (F a) (F b) = True
    > Equiv (f a) (f b) = Equiv a b
    > Equiv a b = False

    Does this make sense?

    Reply
  3. Pingback: Coincident Overlap in Type Families | Types and Kinds

  4. jberryman

    I’m super excited about this; thanks for your work! Quick question: what you’ve written about `Equals` and your third “Details” bullet seem to contradict what’s currently in the wiki (the “type family J” example):

    http://www.haskell.org/haskellwiki/GHC/Type_families#Closed_family_simplification

    Is the behavior you describe above correct, or has it changed since you posted this (and gotten more tricky, per the haskell wiki)?

    Sorry to be lazy and ask you instead of immediately trying it on GHC HEAD, but I figure this comment will help future visitors too.

    Reply
    1. Richard Eisenberg Post author

      Yes, things moved on quite a bit since this post, including the concrete syntax. But, I don’t see a contradiction in the spot that you pointed out between this post and that wiki page. The family `Equals` (or `J` from the wiki) will reduce only when GHC is sure that either the types involved are identical or when they are different. Thus, an application like `Equals a Int` won’t reduce, because we don’t know what `a` is!

      You may also want to check out the soon-to-be-published paper on this subject. The latest draft is available at http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms-extended.pdf The first several sections are meant more for practicing programmers, and it might clarify some of the delicate points around closed type families.

      Thanks for your interest!

      Reply
      1. jberryman

        Ah thanks, I misunderstood the wiki page. I’m also really curious if there has been any progress or future plans to implement the type inference enhancements mentioned in the paper, where some closed type family instances may permit inference of part or all of the LHS from the right. That’s something I’m really excited about seeing. Maybe I can even try to get my feet wet hacking GHC, though I suspect that would be pretty ambitious.

  5. Richard Eisenberg

    Short answer: no, there hasn’t been any progress, and there are no concrete plans to move forward here. I’m currently talking with two undergrads about engaging in some related research during the spring semester. Either may end up tackling those problems. But, everything is still wide open, and I’d be happy to advise someone who wants to look closely at any of the open problems mentioned in that paper — please have no fear of entering “my” territory on this!

    GHC hacking is very rewarding and probably not as difficult as you might think. I would probably start with a project that doesn’t involve type inference to get going, but I don’t think these type inference problems are particularly thorny. Then again, when I started thinking about closed type families, I didn’t think they had any thorny issues either!

    Reply

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s