First Class Type Families

[BebeSparkelSparkel]

In Data.Vinyl.Tutorial.Overview, it is stated that "Unfortunately, type families aren't first class in Haskell". What are your thoughts on Li-yao Xia's First-class type families being applicable Vinyl?

There is an in depth explanation in Sandy Maguire's Thinking with Types Chapter 10 First Class Families.

[acowley]

I may be misunderstanding, but that is the technique used in Vinyl. The tutorial uses a type family ElF in a similar way to Eval. Vinyl was one of the first explorers of this technique in Haskell, though this way of resolving tags to types doesn’t get exercised so much in common usage today.

[BebeSparkelSparkel]

Do you know where I could learn more about the more common ways of accomplishing this today?

[acowley]

Sorry, I meant that using this capability in Vinyl is not emphasized. Instead, users gravitate towards using Vinyl for anonymous records. The same underlying record type then lets you access fields by name, but what we call the “interpretation functor” is not doing anything interesting. In a Vinyl FieldRec, the interpretation functor is not a defunctionalized type family as we’ve been discussing, but just a GADT.

Vinyl’s emphases are interesting, but more broadly I think these techniques are not widely adopted in part because of the ceremony needed to use them. Why do we need the separate data type and Eval? Because type families are not first class in Haskell.

The result is that the slight gain in type-level expressiveness you can achieve is always weighed against the clunky code. The frustration for potential users is that there isn’t an obvious reason why we can’t work with type level functions (ie type families) as easily as we can value level functions, so the ceremony needed for doing so is a persistent irritant. This is not to say that changing GHC to do this actually is easy, and in fact this will change with Dependent Haskell which has loomed on the horizon for many years.