Type families are a recent extension of GHC by which functions over types can be defined by case analysis, much like term-level functions, and appear in type signatures. I will illustrate the use of type families in the context of my type-preserving compiler. I will compare the results with a former solution that uses GADTs to encode type functions as relations, and argue that type families promote a more direct programming style and translates into increased run-time performance. They offer better modularity and require fewer type annotations than type classes, which require that class constraints be propagated between compilation phases.
I will also describe a use of type families to capture more complex data structure invariants. I will mention current limitations that appear with these more advanced uses, in which we need to convince the type checker that the type families we define satisfy certain properties. I will discuss a proposal of a language extension to directly support such properties.
This is joint work with Stefan Monnier.