"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.

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.