Haskell with only one type family
In this post, we will implement open type families with a single actual type family.^{1} Surprisingly, this endeavor leads to increased expressivity: type families become firstclass.
Check out my very creatively named package: firstclassfamilies.
The result is a form of defunctionalization (I call “evalstyle”), to be compared later with a more common one (“applystyle”). I will not assume knowledge of it in this post, but you can read more about it over there: Defunctionalization for the win.
Extensions and imports for this Literate Haskell file
{# LANGUAGE
DataKinds,
PolyKinds,
TypeFamilies,
TypeInType,
TypeOperators,
UndecidableInstances #}
module OneTypeFamily where
import Data.Kind (Type)
import GHC.TypeNats (Nat, type (+))
import GHC.TypeLits (TypeError, ErrorMessage(..))
Summary
Type families are defined by patternmatching. We are going to replace all type families with a single one that matches on an encoding of a type family applied to its arguments.
For example, the following family, a typelevel fst
:
type family Fst' (xy :: (a, b)) :: a
type instance Fst' '(x, y) = x
will be replaced with this data
type Fst
where the type constructor represents the Fst'
type family, together with a type instance
clause for a single general type family, called Eval
:
 fst :: (a, b) > a
data Fst (xy :: (a, b)) :: Exp a
type instance Eval (Fst '(x, y)) = x
The Eval
type family
As its name indicates, the type family Eval
evaluates applied type families. More generally, we will see that Eval
can also work with complex expressions, hence the name of the kind Exp
.
type family Eval (e :: Exp a) :: a
The kind Exp a
of an expression is indexed by the kind a
of the result of its evaluation. The kind of expressions Exp
is actually defined as:
type Exp a = a > Type
Instead of declaring a type family, we introduce a new expression constructor by declaring a data
type, such as Fst
above. The inhabitants of Fst
don’t matter (in practice we leave those types empty). We only use data
as a way to introduce new symbols in the typelevel language that we can patternmatch on; we sometimes call them “defunctionalized symbols”: symbols are not actually functions but they stand for them. Essentially, we use Exp
as an “extensible GADT”, whose constructors are type constructors.
Here are two more examples of expressions encoding some common functions:
 snd :: (a, b) > b
data Snd :: (a, b) > Exp b
type instance Eval (Snd '(x, y)) = y
 fromMaybe :: a > Maybe a > a
data FromMaybe :: a > Maybe a > Exp a
type instance Eval (FromMaybe x0 'Nothing ) = x0
type instance Eval (FromMaybe x0 ('Just x)) = x
Exercise
Translate this type family using Eval
:
type family Length' (xs :: [a]) :: Nat
type instance Length' '[] = 0
type instance Length' (x ': xs) = 1 + Length' xs
Expected result in ghci
:
λ> :kind! Eval (Length '[1,2,3])
(...)
3
That is all there is to it, to have type families with only one type family.
From now on, only type family signatures (actually, the data
type) will be given, leaving the Eval
instances as exercises for the reader.
Firstclass type families
Encoding type families with type constructors allows them to be passed around without applying them, which is not possible in their original form. Hence we will call this new thing “firstclass type families”, as opposed to “regular type families”. And indeed, we can define higherorder type families, such as Map
, where the first parameter is a unary type family a > Exp b
:
data Map :: (a > Exp b) > [a] > Exp [b]
Expected result in ghci
:
λ> :kind! Eval (Map Snd '[ '(1, 2), '(3, 4) ])
(...)
'[2, 4]
Of course that is meant to correspond to map
:
map :: (a > b) > [a] > [b]
But those Exp
constructors are in quite familiar places. Doesn’t it look like…
traverse :: Applicative m => (a > m b) > [a] > m [b]
Did you notice Exp
is a monad?
data (>>=) :: Exp a > (a > Exp b) > Exp b
data Pure :: a > Exp a
Composition of type families is Kleisli composition:
data (>=>) :: (a > Exp b) > (b > Exp c) > a > Exp c
The monad laws should hold when we observe the result with Eval
:
Eval (m >>= Pure) = Eval m
Eval (Pure x >>= k) = Eval (k x)
Eval ((m >>= h) >>= k) = Eval (m >>= (h >=> k))
We can play with a few more Functor
/Applicative
/Monad
combinators.
data (<$>) :: (a > b) > Exp a > Exp b
data (<*>) :: Exp (a > b) > Exp a > Exp b
data Join :: Exp (Exp a) > Exp a
Lazy typelevel functional programming
Thus, firstclass type families bring a certain amount of functional programming to the type level. Moreover, with the control we have over Eval
uation of Exp
ressions, we can emulate some lazy functional programming patterns.
This is a big deal, because type families are strict^{2}. For example, consider this If
type family:^{3}
type family If (b :: Bool) (x :: k) (y :: k) :: k
type instance If 'True x _ = x
type instance If 'False _ y = y
What happens if we compile the following snippet?
type X =
If 'True
()TypeError ('Text "This shouldn't happen")) (
The condition is True
, so it seems the result should be the first branch ()
, but the error in the second branch is still evaluated:
error:
• This shouldn't happen
• In the type synonym declaration for ‘X’

218  type X =
 ^^^^^^^^...
The old solution with regular type families is to specialize If
manually, but this is certainly cumbersome to do for every conditional:
type family IfThis (b :: Bool) :: Type
type instance IfThis 'True = ()
type instance IfThis 'False = TypeError ('Text "This shouldn't happen")
type Y = IfThis 'True
Using firstclass type families, we don’t need to change If
at all.^{4} Instead, we first make an Exp
to delay the evaluation of a TypeError
.
data TypeError' :: ErrorMessage > Exp a
Now, the branches of If
are expressions, and we will unpack only the one we need with Eval
.
type Z = Eval
If 'True
(Pure ())
(TypeError' ('Text "This shouldn't happen"))) (
Compilation succeeds, evaluating Z
to ()
(if you have Pure
defined).
At this point, you may know enough to really use firstclass type families.
Apply and Eval
As mentioned at the beginning, this is a kind of defunctionalization, closely related to another variant that you may have come across elsewhere, such as in Defunctionalization for the win or in Higherkinded data. Here is a brief explanation.
The original motivation was to have firstclass functions, so Exp
is replaced with this kind (~>)
of “defunctionalized function symbols”:
type a ~> b = a > b > Type
(Actually, looking at singletons, (~>)
is defined a bit differently for historical reasons, I believe, but that is a minor detail.)
Now the one type family is descriptively called Apply
:
type family Apply (f :: a ~> b) (x :: a) :: b
 Example
data Fst_ :: (a, b) ~> a
type instance Apply Fst_ '(x, _) = x
Eval
separates “application” (via type constructor application) and “evaluation”, whereas they happen simultaneously in Apply
. In that sense, Eval
seems like a more elementary presentation of defunctionalization. Nonetheless, the two styles are equivalent in expressivity.
Equivalence between Apply and Eval
We can translate one style of defunctionalization into the other and vice versa.
First, we can define Eval_
in terms of Apply
, representing Exp a
expressions with applystyle constant functions () ~> a
.
type Exp_ a = () ~> a
type Eval_ (e :: Exp_ a) = Apply e '()
And second, we can define Apply_
using Eval
, representing a ~> b
with Kleisli arrows a > Exp b
.
type Apply_ (f :: a > Exp b) (x :: a) = Eval (f x)
Note that we literally have (a ~> b) = (a > Exp b)
here, so we can directly reuse the same defunctionalized symbols in this second translation.
Conclusion
Converting regular type families to firstclass type families is so straightforward, I’m surprised to not have seen any discussion about this “evalstyle” defunctionalization before.
Feel free to share any idea or issue you encounter with firstclassfamilies!
An idea reminiscent of Haskell with only one typeclass.↩︎
The truth is more complicated (and I don’t know the details well), but that will be a good enough approximation for the purposes of this post,↩︎
I also talk about it in another post on typelevel programming.↩︎
I find this
If
quite nice. I’m not sure making it a firstclass type family is worth the extra steps. “One type family” is only a nice title.↩︎