blog

"Typing Haskell in Haskell" makes the implementation of type systems concrete for programmers; recent developments in type theory have much to offer but are not developed to this depth even in theory. Row types are particularly juicy because one does not lose type inference; we can use the exact same unification approach and need not resort to ordered contexts or focalization.

This is implemented in my Apple compiler. I follow the "Typing Haskell in Haskell" approach, so what follow will only make sense if you have read that paper.

On the type theory side:

\( \vdash {\tt (.x)} : \{\rho~|~x: a\} \rightarrow a \)

The idea is that we can write { x = 1, y = 2 }.x and { x = 1, y = 2, z = 1 }.x without resorting to metaprogramming, typeclasses, etc.

In Haskell:

data Ty = TVar Name | Row Name (Map Name Ty) | ...

data Exp = At Name | ...

At Name is the new bit of syntax for accessing records. The type of At x is then Row ρ [(x, TVar a)] -> TVar a.

To get this working, we simply add several cases to mgu, viz.

• Row a rs unifies with a record R if R has all fields in rs and the leaves of rs unify with the types of the fields of R.
• Row a rs unifies with Row b qs by unifying the leaves of the intersection of rs, qs and then adding \(a \mapsto b \) to the substitution.

Following "Typing Haskell in Haskell":

mgu (Row n rs) ty@(Row m qs) = do
    rs' <- lS (\s (t, t') -> mgu (apply s t) (apply s t')) $ Map.elems $ Map.intersectionWith (,) rs qs
    (@@ rs') <$> varBind n (apply rs' ty)
lS :: Monad m => (Subst -> a -> m Subst) -> Subst -> [a] -> m Subst
lS _ s [] = pure s
lS f s (x:xs) = do
    next <- f s x
    lS f next xs

This is still vague, but hopefully one can see the ease of adding row types to common type systems. Since all interesting type-theoretic properties are preserved, languages should include row polymorphism as a feature.