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