This wiki page is by Nicolas Frisby (nfrisby).
Overview
I've been recently developing a coxswain
library that defines row types and implements row unification.
My motivations are as follows.
 I think the Haskell community is hungry for row types, especially records and variants.
 I'm pretty familiar with the Core simplifier, but not the GHC type checker. The OutsideIn JFP is a wonder (!), but it's just too much for me to internalize without getting my hands dirty. So this plugin seemed like a wonderful way to learn.
 I think the plugin API is important, and I wanted to get a sense of its current state and capabilities, both for my knowledge and as feedback to its owners.
This wiki page outlines the basic design and intended use of the library, use cases I envision, a rough bibliography, my plugin architecture, my notes about the type checker plugin API, and my open questions.
(DISCLAIMER In the following text, I make lots of claims about what the plugin does and doesn't do. But it's very much a work in progress (remember, I'm using it to learn). I don't have anything that's anywhere close to approaching a proof of its correctness.)
The plugin code is on GitHub, BSD3. https://github.com/nfrisby/coxswain
Plugin Debug Options
The plugin understands a couple debugging options, if you want to inspect what it's doing to constraints.

fpluginopt=Coxswain:summarize
This will dump out the "beforeandafter" constraints of each time GHC gives the plugin a "task" (e.g. solve the Wanted constraints in some definition's RHS). 
fpluginopt=Coxswain:trace
This will dump out the constraints and the contradictory or solved/new constraints that the plugin finds every time GHC invokes the plugin (i.e. multiple times per "task"). 
fpluginopt=Coxswain:logfile=<file>
This will write that output to the specified file instead of to the default ofstderr
.
Demonstration
Comparison to the Nice Elm Overview
To get a basic sense of what the library feels like, the following code block imitates the wellwritten and beginnerfriendly documentation page about records in Elm. It imports the Data.Sculls.Symbol
module from the sculls
package, which is my current draft of record types on top of the coxswain
row types.
(Please forgive my punny names. Naming is one of the most fun parts for me. If this were to gain enough momentum and "official" adoption, I would suggest renaming it to something plain, like rowtypes
and the RowTypes
module and recordtypes
and the Data.Record
e.g. module.)
{# LANGUAGE BangPatterns #}
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE OverloadedLabels #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{# OPTIONS_GHC fplugin=Coxswain #}
{# OPTIONS_GHC fconstraintsolveriterations=100 #}
module Elm where
import Data.Sculls.Symbol
import GHC.TypeLits (type (+))
import Text.Read (readMaybe)
 What is a Record?
frag1 = mkR .* #x .= 3 .* #y .= 4
frag2 = mkR .* #title .= "Steppenwolf" .* #author .= "Hesse" .* #pages .= 237
 Access
point2D = mkR
.* #x .= 0
.* #y .= 0
point3D = mkR
.* #x .= 3
.* #y .= 4
.* #z .= 12
 PEOPLE
bill = mkR
.* #name .= "Gates"
.* #age .= 57
steve = mkR
.* #name .= "Jobs"
.* #age .= 56
larry = mkR
.* #name .= "Page"
.* #age .= 39
people =
[bill
, steve
, larry
]
 Access
frag3 = (
point3D `dot` #z
,
bill `dot` #name
,
(`dot` #name) bill
,
map (`dot` #age) people
)
frag4 = (
point2D `dot` #x
,
point3D `dot` #x
,
(mkR .* #x .= 4) `dot` #x
)
 Pattern Matching  TODO: record patterns
frag5 !r =
sqrt (x^2 + y^2)
where
x = r `dot` #x
y = r `dot` #y
frag6 !r =
age < 50
where
age = r `dot` #age
 Updating R Iecords
frag7 = (
point2D ./* #y .= 1
,
point3D ./* #x .= 0 ./* #y .= 0
,
steve ./* #name .= "Wozniak"
)
rawInput = mkR
.* #name .= "Tom"
.* #country .= "Finland"
.* #age .= "34"
.* #height .= "1.9"
prettify person = person
./* #age .= toInt (person `dot` #age)
./* #height .= toFloat (person `dot` #height)
where
toInt :: String > Maybe Int
toInt = readMaybe
toFloat :: String > Maybe Float
toFloat = readMaybe
input =
prettify rawInput
 R Iecord Types
origin :: R I (Row0 .& "x" .= Float .& "y" .= Float)
origin = mkR
.* #x .= 0
.* #y .= 0
type Point = Row0
.& "x" .= Float
.& "y" .= Float
hypotenuse :: R I Point > Float
hypotenuse !p =
sqrt (x^2 + y^2)
where
x = p `dot` #x
y = p `dot` #y
type Positioned a = a
.& "x" .= Float
.& "y" .= Float
type Named a = a
.& "name" .= String
type Moving a = a
.& "velocity" .= Float
.& "angle" .= Float
lady :: R I (Named (Row0 .& "age" .= Int))
lady = mkR
.* #name .= "Lois Lane"
.* #age .= 31
dude :: R I (Named (Moving (Positioned Row0)))
dude = mkR
.* #x .= 0
.* #y .= 0
.* #name .= "Clark Kent"
.* #velocity .= 42
.* #angle .= 30  degrees
getName ::
(
Lacks a "name"  Necessary difference compared to Elm. Comparable to KnownNat/KnownSymbol/etc.
,
Short (NumCols a)  Merely consequence of particular record implemention.
)
=> R I (Named a) > String
getName !r = r `dot` #name
names :: [String]
names =
[getName dude, getName lady ]
getPos ::
(
Lacks a "y" , Lacks a "x"  Necessary difference compared to Elm. Comparable to KnownNat/KnownSymbol/etc.
,
Short (NumCols a + 1)  Merely consequence of particular record implemention.
)
=> R I (Positioned a) > (Float,Float)
getPos !r = (x,y)
where
x = r `dot` #x
y = r `dot` #y
positions :: [(Float,Float)]
positions =
[getPos origin, getPos dude ]
 BEYOND THE ELM TUTORIAL
vars :: [V I (Row0 .& "x" .= Int .& "y" .= Char .& "z" .= Bool)]
vars = [inj #z True,inj #x 7,inj #y 'h',inj #z False,inj #y 'i',inj #x 3]
pvars = vpartition vars
At the GHCi prompt, those definitions result in the following.
*Main> vars
[<z True>,<x 7>,<y 'h'>,<z False>,<y 'i'>,<x 3>]
*Main> pvars
{(x=[7,3]) (y="hi") (z=[True,False])}
The vpartition
function is not a primitive! The following is its definition inside sculls
.
  Partition a list of variants into in listshaped record of the
 same row.
vpartition :: forall (p :: Row kl *) f. (Foldable f,Short (NumCols p),Short (NumCols p  1)) => f (V I p) > R (F []) p
vpartition = foldr cons (rpure (F []))
where
cons v !acc = velim (f /$\ rhas) v
where
f :: forall (l :: kl) t. (HasCol p :>: I :>: C (R (F []) p)) l t
f = A $ \HasCol > A $ \x > C $ runIdentity $ rlens (Identity . g x) acc
g :: forall (l :: kl) t. I l t > F [] l t > F [] l t
g (I x) (F xs) = F (x:xs)
Unpacking that definition is a helpful overview of the internals of the sculls
library. We'll return to do that after a tour of the basic structures of coxswain
and sculls
.
The Row Type Basics
(I've since generalized Row
to be polykinded in the column type as well as the column name. But I haven't yet updated this section.)
We'll start with the core row type declarations from the coxswain
library.
  Column kind.
data Col (k :: Type)
infix 3 .=
  Column constructor.
type family (l :: k) .= (t :: Type) = (col :: Col k)  col > l t where
  Row kind.
data Row (k :: Type)
  The empty row.
type family Row0 :: Row k where
infixl 2 .&
  Row extension.
type family (p :: Row k) .& (col :: Col k) = (q :: Row k) where
Those declarations are closed empty type families; the type checker plugin is what gives them semantics. So they're just syntax: Row0 .& "a" .= Int .& "b" .= Bool
is a row type with two columns: an Int
named a
and a Bool
named b
. The only row type formers are the empty row and row extension. (Future version might include row union, row intersection, etc.)
The whole point of rows is that column order doesn't matter. So Row0 .& "a" .= Int .& "b" .= Bool
should be equal (really actually equal, as in ~
) to Row0 .& "b" .= Bool .& "a" .= Int
. That's what the type checker plugin achieves, by implementing a wellestablished approach called row unification, which is pretty simple. The engineering effort was to realize it as a plugin to GHC's OutsideIn formalism.
Row unification determines what is in a row, but we usually also need to know what is not in the row. This is the role of the Lacks
constraint. Lacks p l
means that l
is not the name of a column in p
. The cleverest bit about Lacks
constraints is how to evidence them: it's the position in the sorted columns of the concrete row at which l
would be inserted to preserve the sorting. So, presuming intuitive order, Lacks (Row0 .& "b" .= Int) "a"
would be 0, since a
would be inserted at the front. And Lacks (Row0 .& "a" .= Int) "b"
would be 1, since b
would be the second column.
  Evidence of a 'Lacks' constraint.
newtype RowInsertionOffset (p :: Row k) (l :: k) = MkRowInsertionOffset Word16
  The lacks predicate.
class Lacks (p :: Row k) (l :: k) where rowInsertionOffset_ :: RowInsertionOffset p l
  Returns the index in the normal form of @p@ at which @l@ would be inserted.
rowInsertionOffset :: forall p (l :: k). Lacks p l => Proxy# p > Proxy# l > Word16
There's an inductive specification: Lacks Row0 l
is 0, Lacks (p .& l1 .= t) l2
is Lacks p l2
if l2 < l1
and it's Lacks p l2
plus one if l1 > l2
 it's a contradiction if l1 ~ l2
. This is the logic the plugin implements.
That's all of what's covered in most presentations of row types and row unification. But we need more in order to be a full participant in Haskell! For example, you can't use the row types syntax in type class instances, since they're type families! Row types are structural, not nominal, and type families and type classes can only scrutinize nominal types. My solution to that is to have the plugin provide a couple useful interpretations of a row type.
infixl 2 `NExt`
  A normalized row.

 The following invariant is intended, and it is ensure by the 'Normalize' type family.

 INVARIANT: The columns are sorted ascending with respect to an arbitrary total order on the column names.
data NRow k =
NRow0  ^ The empty row.

NExt (NRow k) k Type  ^ A row extension.
  Normalize a row.
type family Normalize (p :: Row k) = (q :: NRow k)  q > p where
  The number of columns in a row.
type family NumCols (p :: Row k) :: Nat where
The plugin makes Normalize
and NumCols
do what you'd expect. The key is that we can index type classes and such by Normalize p
and NumCols p
in order to overload based on the observable structure of the row.
There's one last piece to mention. In Haskell, we're unaccustomed to "negative information" like the Lacks
constraint. What we typically see is positive information, like a "Has" constraint. With this classic approach, positive information is equality information, which row unification lets us use without concern for ordering. (If order does matter, then we don't need rows, we can just use typelevel lists of columns (like NRow
) and GHC's normal unification will suffice. This would be like Python's "named tuples".)
Clearly our rows do have columns, so we should be able to write "Has" constraints, right? Yes, and there are two definitions of "Has" in terms of Lacks
and ~
(at kind Row
).
  @HasRestriction p q l t@ evidences that @p@ is @q@ extended with @l '.=' t@.
data HasRestriction :: Row k > Row k > k > * > * where
HasRestriction :: Lacks q l => HasRestriction (q .& l .= t) q l t
  @HasCol p l t@ evidences that there exists a @q@ such that @p@ is @q@ extended with @l '.=' t@.
data HasCol :: Row k > k > * > * where
HasCol :: Lacks q l => HasCol (q .& l .= t) l t
HasRestriction
could be defined as a type class alias: (Lacks q l,p ~ q .& l .= t) => HasRestriction p q l t
, but HasCol
cannot, because it would require an existential for q
on the equality constraint, which GHC currently does not support.
That's everything in the current coxswain
package! Those are the exposed declarations, and the type checker plugin makes row unification and the Normalize
and NumCols
type families do what they're supposed to.
The Record and Variant Basics
The sculls
package defines types for records and variants. They both have two indices: the row type and the structure of each field.
newtype R (f :: k > * > *) (p :: Row k) = MkR ...  The omission is essentially a named tuple determined by Normalized p, with each component structured by f. (Notably, that's what most existing Haskell record libraries use as records, full stop.)
data V (f :: k > * > *) (p :: Row k) = MkV !Any !Word16  Yes, I use unsafeCoerce here. Sorry.
There are several useful ways to structure the fields.

I l t
ist
 it's the "identity" field structure. 
F f l t
isf t
 it wraps the column type in a functor. 
(f :>: g) l t
isf l t > g l t
 it's a function between field structures. 
C a l t
isa
 a constant field structure. 
D c l t
is a dictionary forc l t
, for when we want field's value to depend on the column types.
You can write your own, of course; it's just a type of kind k > * > *
. (We could overload on the kind of t
too, but I just haven't yet and don't yet have a concrete motivating use case.)
In fact, HasCol p
has that kind, and we'll see below that it can be very useful as a field.
vpartition
Back to Now let's revisit vpartition
to see those pieces in action with some primitive functions on records and variants.
  Partition a list of variants into in listshaped record of the
 same row.
vpartition :: forall (p :: Row kl *) f. (Foldable f,Short (NumCols p),Short (NumCols p  1)) => f (V I p) > R (F []) p
vpartition = foldr cons (rpure (F []))
where
cons v !acc = velim (f /$\ rhas) v
where
f :: forall (l :: kl) t. (HasCol p :>: I :>: C (R (F []) p)) l t
f = A $ \HasCol > A $ \x > C $ runIdentity $ rlens (Identity . g x) acc
g :: forall (l :: kl) t. I l t > F [] l t > F [] l t
g (I x) (F xs) = F (x:xs)
 The
Short (NumCols p)
constraint is an implementation detail of my current choice for the internal representation of theR
type. Feel free to think of it asKnownNat (NumCols p)
. 
R f p
is a record for the rowp
where each fieldl .= t
inhabitsf l t
. 
I l t
is a newtype aroundt
, so anI
structured record is what we normally think of when we hear "record". 
V f p
is a variant, which is a sum of the columns instead ofR
's product of columns.  The
F f l t
field type is a newtype aroundf t
, soR (F []) p
is a record where every field is a list of the column type. 
rpure
is a primitive that creates a record where every field has the given polymorphic value. 
elimV
is a primitive identified by Gaster and Jones (1996) that takes a record of functions with a fixed codomain and a variant and applies the corresponding record to the variant's payload; i.e. it's a case expression where the record is the alternatives and the variant is the discriminant. 
rmap
applies a record of functions to a record of arguments. The record of functions must be built with the:>:
field type; likeI
andF
,f :>: g
is a newtype aroundf l t > g l t.

rHasCol
builds a record where each field is evidence of its own existence! Here the field structure (likeI
andF
) isHasCol p l t
, which is a GADT evidencing that the rowp
has a columnl .= t
.  The
C
field structure just holds a constant, irrespective of the column label and type. 
rlens
is a lens into a field of a record; the expression above with theIdentity
Applicative
achievesover
from thelens
library.
Performance?
[Thank you, Ara Adkins. I forgot my section about performance until your email.]
As usual, the objective is for the library to have minimal runtime overhead. With hundreds of Lacks
constraints floating around, that means  again, as usual  that inlining and specialization are key. Things look promising at this stage.
For example, the vpartition
example from above (repeating here)
vars :: [V I (Row0 .& "x" .= Int .& "y" .= Char .& "z" .= Bool)]
vars = [inj #z True,inj #x 7,inj #y 'h',inj #z False,inj #y 'i',inj #x 3]
pvars :: R (F []) (Row0 .& "x" .= Int .& "y" .= Char .& "z" .= Bool)
pvars = vpartition vars
 at a concrete row type  essentially compiles down to the following Core at O1
, which is pretty good.
Rec {
 RHS size: {terms: 48, types: 197, coercions: 7,299, joins: 0/0}
main_go
main_go
= \ ds_a9PI eta_B1 >
case ds_a9PI of {
[] > eta_B1;
: y_a9PN ys_a9PO >
case y_a9PN of { MkV flt_a9Lz dt3_a9LA >
case dt3_a9LA of {
__DEFAULT >
case eta_B1 `cast` <Co:797> of { V3 a0_a9N8 a1_a9N9 a2_a9Na >
main_go
ys_a9PO
((V3
a0_a9N8
a1_a9N9
((: flt_a9Lz (a2_a9Na `cast` <Co:65>)) `cast` <Co:59>))
`cast` <Co:1512>)
};
0## >
case eta_B1 `cast` <Co:797> of { V3 a0_a9N8 a1_a9N9 a2_a9Na >
main_go
ys_a9PO
((V3
((: flt_a9Lz (a0_a9N8 `cast` <Co:65>)) `cast` <Co:59>)
a1_a9N9
a2_a9Na)
`cast` <Co:1512>)
};
1## >
case eta_B1 `cast` <Co:797> of { V3 a0_a9N8 a1_a9N9 a2_a9Na >
main_go
ys_a9PO
((V3
a0_a9N8
((: flt_a9Lz (a1_a9N9 `cast` <Co:65>)) `cast` <Co:59>)
a2_a9Na)
`cast` <Co:1512>)
}
}
}
}
end Rec }
The V3
constructor is part of something I haven't talked about on this page yet: my representation strategy for the R
type. That representation is a "short vector", which is a tuple of strict Any
s that I coerce into and out of according to the column type. It's a data family indexed by NumCols p
, and the Short (NumCols p)
dictionaries provide operations on it. There are plenty of other options, and which one is right will depend on the situation. But, in my experience, short vectors (up to ~16 or so?) seem to optimize better as algebraic data types than as serialized byte arrays. That's definitely something to revisit eventually, with some hard measurements.
And steak knives!
There are several more primitives. Most notably, records have both Applicative
like and Traversable
like properties, since they're products.
  Record analog of 'pure'.
rpure :: Short (NumCols p) => (forall (l :: k) t. f l t) > R f p
  Record analog of 'fmap'.
rmap :: Short (NumCols p) => (forall (l :: k) t. (a :>: b) l t) > R a p > R b p
  Record analog of '<*>'.
rsplat :: Short (NumCols p) => R (a :>: b) p > R a p > R b p
  Combine all the fields' values. Beware that the fields are combined in an arbitrary order!
rfold :: (Short (NumCols p),Monoid m) => R (C m) p > m
  Traverse all the fields. Beware that the fields are visited in an arbitrary order!
rtraverse :: (Applicative g,Short (NumCols p)) => (forall (l :: k) t. (f :>: F g :.: h) l t) > R f p > g (R h p)
Also, rows are finite, so we can require that a constraint holds for each column.
  Record of evidence that each column exists in the record's row.
rHasCol :: Short (NumCols p) => R (HasCol p) p
  A record of dictionaries for the binary predicate @c@ on column name and column type.
rdictCol :: RAll c p => Proxy# (c :: k > * > Constraint) > R (D c) p
And records are Show
able, Monoid
s, Generic
, etc, etc.
Variants exhibit the dual properties, for the most part.
Together, records and variants have a few useful interactions.
  Eliminate a variant with a functional record. (Gaster and Jones 1996)
velim :: Short (NumCols p) => R (f :>: C a) p > V f p > a
  Eliminate a record with a functional variant. (Gaster and Jones 1996)
relimr :: Short (NumCols p) => V (f :>: C a) p > R f p > a
  Convert each field to a variant of the same row.
rvariants :: Short (NumCols p) => R f p > R (C (V f p)) p
  Partition a list of variants into in listshaped record of the same row.
vpartition :: Short (NumCols p) => [V I p] > R (F []) p
Some Light Core Snorkeling
Simon Peyton Jones gave the following snippet and asks "What does Core look like? I think your answer is “No change to Core, but there are lots of unsafe coerces littered around”. But even then I’m not sure. Somehow in the ??? [below] I have to update field n of a tuple x. How do I do that?".
f :: Lacks r "f" => V (Row (r .& ("f" .= Int))) > V (Row (r .& ("f" .= Int)))
f n x = ???
If I understand the question correctly, the source would look be as follows.
upd :: I "f" Int > I "f" Int
upd (I x) = I (x + 1)
f ::
( Lacks r "f"
, Short (NumCols r) )
=> R I (r .& "f" .= Int)
> R I (r .& "f" .= Int)
f = over rlens upd
 Or (f r = r ./ #f .* #f .= (1 + r `dot` #f)), but that Core is worse.
I suspect the Short
constraint is what Simon was smelling. This class was mentioned a bit in the previous section about performance. Here is what the Short
class looks like, to offer some more insights:
  A short, homogenous, and strict tuple.
data family SV (n :: Nat) :: * > *
type Fin (n :: Nat) = Word16
  Predicate for supported record sizes.
class (Applicative (SV n),Traversable (SV n)) => Short (n :: Nat) where
select :: SV (n + 1) a > Fin (n + 1) > a
lensSV :: Functor f => (a > f a) > SV (n + 1) a > Fin (n + 1) > f (SV (n + 1) a)
extend :: SV n a > a > Fin (n + 1) > SV (n + 1) a
restrict :: SV (n + 1) a > Fin (n + 1) > (a,SV n a)
indices :: SV n (Fin n)
The SV
data family provides the tuples of Any
that I currently use to represent records. For example, the rlens
record primitive is defined by simply coercing the lensSV
method. I generate SV
and Short
instances via Template Haskell. The SV
instance for 2
and its lensSV
method definition are as follows.
data instance SV 3 a = V3 !a !a !a
deriving (Foldable,Functor,Show,Traversable)
instance Short 2 where
...
{# INLINE lensSV #}
lensSV f (V3 a b c) = \case
0 > (\x > V3 x b c) <$> f a
1 > (\x > V3 a x c) <$> f b
_ > (\x > V3 a b x) <$> f c
Thus, the O1 dsuppressall
core for f
is as follows.
 RHS size: {terms: 8, types: 6, coercions: 4, joins: 0/0}
f2
f2
= \ x_a5UG >
case x_a5UG `cast` <Co:4> of { I# x1_a6ax > I# (+# x1_a6ax 1#) }
 RHS size: {terms: 10, types: 53, coercions: 175, joins: 0/0}
f1
f1
= \ @ r_a5QC $dLacks_a5QE $dShort_a5QF eta_B1 >
lensSV
($dShort_a5QF `cast` <Co:25>)
$fFunctorIdentity
(f2 `cast` <Co:41>)
(eta_B1 `cast` <Co:96>)
($dLacks_a5QE `cast` <Co:13>)
 RHS size: {terms: 1, types: 0, coercions: 115, joins: 0/0}
f
f = f1 `cast` <Co:115>
That reveals the necessary dictionary passing for row polymorphic functions. If we specialize the row variable r
, we get something much closer to the ideal Core.
fmono ::
R I (Row0 .& "a" .= a .& "b" .= b .& "c" .= c .& "f" .= Int)
> R I (Row0 .& "a" .= a .& "b" .= b .& "c" .= c .& "f" .= Int)
fmono = f
 That optimizes to:
 RHS size: {terms: 13, types: 9, coercions: 98, joins: 0/0}
fmono2
fmono2
= \ @ c_a5Rb @ b_a5Ra @ a_a5R9 >
case (\ @ kt_X6bA > W16# 0##) `cast` <Co:98> of { W16# x#_a6b2 >
W16# (narrow16Word# (plusWord# x#_a6b2 3##))
}
 RHS size: {terms: 60, types: 89, coercions: 1,925, joins: 0/0}
fmono1
fmono1
= \ @ c_a5Rb @ b_a5Ra @ a_a5R9 eta_B1 >
case eta_B1 `cast` <Co:405> of
{ V4 a0_a6ch a1_a6ci a2_a6cj a3_a6ck >
case a3_a6ck `cast` <Co:45> of wild1_s6fH { I# x_s6fI >
case a2_a6cj `cast` <Co:45> of wild2_s6fK { I# x1_s6fL >
case a1_a6ci `cast` <Co:45> of wild3_s6fN { I# x2_s6fO >
case a0_a6ch `cast` <Co:45> of wild4_s6fQ { I# x3_s6fR >
case fmono2 of { W16# x4_a6cK >
case x4_a6cK of {
__DEFAULT >
(V4
(wild4_s6fQ `cast` <Co:48>)
(wild3_s6fN `cast` <Co:48>)
(wild2_s6fK `cast` <Co:48>)
((I# (+# x_s6fI 1#)) `cast` <Co:46>))
`cast` <Co:145>;
0## >
(V4
((I# (+# x3_s6fR 1#)) `cast` <Co:46>)
(wild3_s6fN `cast` <Co:48>)
(wild2_s6fK `cast` <Co:48>)
(wild1_s6fH `cast` <Co:48>))
`cast` <Co:145>;
1## >
(V4
(wild4_s6fQ `cast` <Co:48>)
((I# (+# x2_s6fO 1#)) `cast` <Co:46>)
(wild2_s6fK `cast` <Co:48>)
(wild1_s6fH `cast` <Co:48>))
`cast` <Co:145>;
2## >
(V4
(wild4_s6fQ `cast` <Co:48>)
(wild3_s6fN `cast` <Co:48>)
((I# (+# x1_s6fL 1#)) `cast` <Co:46>)
(wild1_s6fH `cast` <Co:48>))
`cast` <Co:145>
}}}}}}}
 RHS size: {terms: 4, types: 9, coercions: 268, joins: 0/0}
fmono
fmono = (\ @ a_a5R9 @ b_a5Ra @ c_a5Rb > fmono1) `cast` <Co:268>
I wasn't expecting that worrying number of coercions or that fmono2
declaration. Adding those to the list. Thanks, Simon!
Future Directions
Other Row Relations
For example, SameLabels p q
would not unify the column types. And WiderThan p q
would require that p
is a structural subtype (width
subtyping) of q
: i.e. p
has every column that q
has.
For these two examples at least, the relevant unification could be
realized via actual equalities between adjustments of p
and q
. For
SameLabels
, the adjustment is to replace all column types in at least
one of p
and q
with fresh unification vars. For WiderThan
, it's to
replace the occurrence of Row0
in the narrower row (p
) with a fresh
unification var. Note however that this approach does not provide
actionable evidence! For example, WiderThan p q
should support a
function upcast :: WiderThan p q => R f p > R f q
. The necessary
evidence for that seems to be an offset into p
for each column of q
.
Other Row Operators
Some users might also like to intersect or union their rows. And if we have polykinded column types, then these operators could either unify the colliding column types or they could pair them up.
These operators could currently be handled via type classes on
Normalized rows, but that would be noisier in the type system and less
wellbehaved, I think  e.g. Lacks (p
Union q) l
should imply Lacks p l
.
Set Types
By "set type", I mean a row type where there is no column types. Is there a proper term for this? Whatever it is, it's not useless, e.g. consider homogenous record/variant types, typeindexed records/variants, permissions/privileges trackings, restricted/indexed monads, etc!
In fact, I think such typeindexed records/variants might even be more useful in Haskell than the "full" ones because they're less structural/more nominal and so more conducive to type class overloading etc.
These can encoded within the current implementation (just ignore the
column type... they'll all be Any
eventually)  and particularly
cleanly if we had polykinded column types inhabiting a void kind 
but it'll always be cleaner to have direct support.
FrontEnd Plugins
Would a frontend plugin be able to automate Lacks constraints from manifest row extensions? This would be nicer, but it would also introduce some "invisible" dictionary arguments, and that makes me nervous about transparency.
Also, maybe it could achieve etaexpansion for any errant Col
vars?
Use Cases for Rows, Records, Variants
The Expression Problem
Row polymorphism is a pretty great fit for modularity and extensibility.
Named Arguments
Once a function has even three arguments, it gets pretty confusing to
identify each of the arguments at a call site (especially a few months
later!). f x y z
would become f (mkR .* #foo .= x .* #bar .= y .* #baz .= z)
.
For example, from O'Sullivan's mathfunctions
package, the `newtonRaphson` function has the following signature.
  Solve equation using NewtonRaphson iterations.

 This method require both initial guess and bounds for root. If
 Newton step takes us out of bounds on root function reverts to
 bisection.
newtonRaphson
:: Double
 ^ Required precision
> (Double,Double,Double)
 ^ (lower bound, initial guess, upper bound). Iterations will no
 go outside of the interval
> (Double > (Double,Double))
 ^ Function to finds roots. It returns pair of function value and
 its derivative
> Root Double
Using a record for the parameters might result in the following signature.
newtonRaphson ::
R I (Row0
.& "precision" .= Double
.& "lowerbound" .= Double
.& "guess0" .= Double
.& "upperbound" .= Double
)
 ^ Required precision. Iterations will no go outside of the interval.
> (Double > (Double,Double))
 ^ Function to finds roots. It returns pair of function value and
 its derivative
> Root Double
Someday, maybe Haddock would allow percolumn comments.
VoR Generics
Especially if we had intersection / union / width subtyping, etc  I think (typeindexed?) Variants of (typeindexed?) Records would be an excellent representation type, generalizing the sumofproducts representation.
Along these same lines, I suspect it might be a useful programming practice for some data types to simply be originally implemented as a typeindexed sum where each summand is a nominal record type (i.e. a proper Haskell data type or a newtype wrapped record type).
CommandLine Options Parser
I suspect a Variant of Records would be an excellent center piece of the interface to a commandline option parsing library, building upon Gonzalez's http://hackage.haskell.org/package/options.
YAML/JSON/CSV/etc Format
These popular "humanreadable" interchange/configuration formats all seem to focus on structural subtyping in one way or another.
Might be great, combined with VoR Generics
Modular/Extensible Reader Monad Environment
This one is a classic. Pretty selfexplanatory, I think.
Modular/Extensible Free "Effects" Monad
A typeindexed sum seems like a great fit for the "which effects" index on a free monad.
Row Type for Array Dimensions
I've been pondering using row types as the shape of an
multidimensional array: each dimension would have a stronglytyped
index instead of just an ordinal. Something along the lines of:
matmul :: (Dim x,Dim n,Dim m,Num a) => proxy x > M (Row0 .& m .& x) a > M (Row0 .& n .& x) a > M (n .& m) a
. The most obvious possible
drawback I've thought of here is that the arbitrary ordering of
columns means the inmemory representation (e.g. rowcol vs colrow)
is unpredictable  therefore a "named tuple" (which doesn't require
rows at all) might be better here.
Rough Bibilography
Gaster and Jones 1996  http://web.cecs.pdx.edu/~mpj/pubs/polyrec.html  The fundamentals of row unification and lacks predicates.
Leijen 2004  https://www.microsoft.com/enus/research/publication/firstclasslabelsforextensiblerows/  Lots of inspiring usecases for rows, records, and variants.
Vytiniotis et all 2011  https://www.microsoft.com/enus/research/publication/outsideinxmodulartypeinferencewithlocalassumptions/  Glorious motivation and details of GHC's OutsideIn(X) type checking algorithm. Unfortunately, spares on some details. For example: what is a Derived constraint and where exactly do they come from‽
Gundry 2015  http://adam.gundry.co.uk/pub/typecheckerplugins/ and https://github.com/adamgundry/uomplugin/  The only published type checker plugin I'm aware of. Very helpful.
Gundry et al 2015  https://gitlab.haskell.org/trac/ghc/wiki/Plugins/TypeChecker  The most documentation I could find about the type checker plugin API :(. It's helpful but terse; we'll need more going forward.
Baaij 2016  http://christiaanb.github.io/posts/typecheckerplugin/  A very nice post that overviews the type checker plugin API. Fact: this post made me actually start this project; thanks Christiaan.
Plugin Architecture
This is the key concept for my plugin's architecture.
Do Not Reimplement Substitution and Unification!
GHC is really good and careful at unification and rewriting, better than I am (especially among Given constraints)  so let it do it.
This also makes it possible to interact with other plugins (notably the GHCs typeequality solver to which I just referred!).
Now the interesting question was: How to correctly compel GHC into doing that? Gundry's paper was the most helpful, but the presentation of the interactions between GHC and the plugins was still too far removed from the actual implementation, specifically the split between simplification of given constraints and solving of wanted constraints and the explicit \theta
substitution versus the implicit substitution in GHC.
I seem to have successfully compelled GHC to create my substitution for me, but I'm sadly still not sure that I'm not violating any crucial invariants. Primarily because I don't know what they all are! They're hard to find, and sometimes the listed invariants are perfectly fine to violate (e.g. flatness of Xi
types in "new" Ct
s in TcPluginOk
; this is referenced as "Only canonical constraints that are actually in the inert set carry all the guarantees" in the source Note [zonkCt behaviour]
). Also, they're often outofdate, either wrong or mysteriously referring to source Notes that no longer exist.
Obviously, the plugin needs to simplify Ct
s according to the row unification, Lacks
, Normalize
, and NumCols
semantic rules. (The two type families are interesting because they don't "float to the top" like other constraints  I have to seek them out within all Cts
and rewrite the whole Ct
. I essentially use SYB for that in my current implementation.)
But, in addition to the obvious simplifications (actually, sort of before and after doing those), my plugin uses the following approach in order to achieve row unification.
 Immediately upon receiving Givens, thaw
Row
skolem vars, i.e. replace them by unification vars with the same kind and level. This enables certain GivenGiven interactions, specifically "unification" via the GHC type equality solver rules EQSAME, EQDIFF, etc. especially involving flatten skolems.
This allows GHC's type equality solver to "learn" the equivalences between Row
"skolem" vars for me.

Importantly, when renaming the skolems, I also create some fake Given constraints
Ren p_sk p_tau
wherep_tau
is the temporary replacement ofp_sk
. This is a robust way for me to later recover theRow
var equalities that GHC's solver learned for me. 
When finished simplifying givens (i.e. if I would be returning
TcPluginOk _ []
), replace any remaining thawed variables (I dissatisfyingly filter based on afsLit "$coxswain"
) by original skolems if possible or fresh skolems if not. Such fresh skolems correspond to row restrictions (i.e. removing one or more columns) of one or more original skolems.
The motivation here is that having unification variables in the Givens while simplifying Wanteds is A Bad Thing (e.g. loss of confluence). Also note that you cannot solve/create Givens when simplifying Wanteds, so this step has to happen when simplifying Givens.
I was worried that creating fresh skolems and leaving them in the Givens would be problematic, but it hasn't caused any trouble so far.
Note that I leave the Ren
constraints, for the sake of the next step.
 When solving Wanted constraints, first recover the learning substitution from the
Ren
constraints and apply it to the Wanted constraints.
Other than some care to handle nested Givens (i.e. when a signature with Givens is inside the scope of a signature with its own Givens), that's the whole exercise.
It's most notable to me that I can apparently leave those fresh restriction skolems around, even within the Wanteds. It hasn't caused any trouble at all yet, though I suspect it might lead to confusing error messages. If need be, I can replace them with a closed empty type family for record restrictions, just for the sake of error messages. (The ultimate user should never use record restrictions, because they apparently lose principal types.)
Plugin API Notes
These are things I lost hours learning, because I couldn't find any obviously uptodate documentation.
Do not zonk givens
zonkCt
is not expected to work on givens. (Note: Gundry's uom
plugin does apply zonkCt
to givens.) In particular, zonking does
not see the latest expansion for the flatten skolems. It seems I have to do
the unflattening manually.
(I'm currently wondering if the "outofdate cached expansion" I'm seeing is because I'm creating illformed variables in the Givens. However, there is this quote "NB: we do not expect to see any CFunEqCans, because zonkCt is only called on unflattened constraints." in the source Note [zonkCt behaviour]
.)
CFunEqCan
Preserve Never mutate/discard CFunEqCan
s! Flatten skolems may cache their
own image, but the part of GHC that matches givens and wanteds doesn't
work without the flatten skolems' CFunEqCan
. Also, the caches are not neccesarily uptodate (see above about zonking givens).
Preserve cc_pend_sc
Do not needlessly churn CDictCan
constraints; needlessly toggling the cc_pend_sc
field back to True
leads to infinite loops.
Nat
dictionaries
Inefficient Evidence bindings for KnownNat
are essentially Integer
s, which GHC does a
surprisingly terrible job optimizing (e.g. Core dive print (natVal(Proxy :: Proxy 3))
sometime...). So I've replace the use of EvNum
with explicit
invocation of dictionaries for building Word16
s bit by bit. GHC does a
great job with those. I also made the classes nullary: the Nat
parameter doesn't matter since these classes exist solely so that the
DFunId
can be invoked  there's no actual instance resolution for
these.
What are the ways GHC invokes my plugin?
I wrote a plugin that merely prettyprints its inputs and is a noop otherwise. I use this to inspect the ways in which GHC invokes plugins.
"Backwards" Invocations during Inference
For example, with GHC 8.2.1, the following module
{# OPTIONS_GHC fplugin=Dumper #}
module Test (f) where
f x = [x] == [x] && null (show x)
results in the following output, which shows that for this module the plugin first "solves Wanteds" (without any Givens, because there's no signature, GADT patterns, etc) and then "simplifies givens"  but the "Givens" are just the unsolved Wanteds! This is somewhat backwards compared to what we usually consider: here we're simplifying "Givens" after solving Wanteds.
========== 0 ==========
given
derived
wanted
[WD] $dEq_a2nz {1}:: Eq a0_a2nr[tau:2] (CDictCan)
[WD] $dShow_a2ns {0}:: Show a0_a2nr[tau:2] (CDictCan)
========== 1 ==========
given
[G] $dShow_a2DE {0}:: Show a_a2DD[sk:2] (CDictCan)
[G] $dEq_a2DF {0}:: Eq a_a2DD[sk:2] (CDictCan)
derived
wanted
========== 2 ==========
given
[G] $dShow_a2Dx {0}:: Show a_a2nr[sk:2] (CDictCan)
[G] $dEq_a2Dy {0}:: Eq a_a2nr[sk:2] (CDictCan)
derived
wanted
I don't know why it appears to simplify those Givens twice.
If we add the signature f :: (Eq a,Show a) => a > Bool
and
recompile, then we only see the two Givens simplification invocations.
Nested Declarations
For the following, we see lots of invocations.
f x = bar () where
bar () = [x] == [x] && null (show x)
 Dumps:
========== 0 ==========
given
derived
wanted
[WD] $dEq_a2nL {1}:: Eq (p1_a1Tm[tau:2] > (TYPE {a2n3})_N) (CDictCan)
[WD] $dShow_a2q3 {0}:: Show (p1_a1Tm[tau:2] > (TYPE {a2n3})_N) (CDictCan)
[WD] hole{a2n3} {0}:: (p0_a1Tl[tau:2] :: RuntimeRep) ~# ('LiftedRep :: RuntimeRep) (CNonCanonical)
========== 1 ==========
given
derived
wanted
[WD] $dEq_a2DQ {1}:: Eq (p1_a1Tm[tau:2] > (TYPE {a2n3})_N) (CDictCan(psc))
[WD] $dShow_a2DU {0}:: Show (p1_a1Tm[tau:2] > (TYPE {a2n3})_N) (CDictCan(psc))
[WD] hole{a2n3} {0}:: (p0_a1Tl[tau:2] :: RuntimeRep) ~# ('LiftedRep :: RuntimeRep) (CNonCanonical)
========== 2 ==========
given
derived
wanted
[WD] $dEq_a2DV {1}:: Eq (p1_a1Tm[tau:2] > (TYPE {a2n3})_N) (CDictCan)
[WD] $dShow_a2DW {0}:: Show (p1_a1Tm[tau:2] > (TYPE {a2n3})_N) (CDictCan)
[WD] hole{a2n3} {0}:: (p0_a1Tl[tau:2] :: RuntimeRep) ~# ('LiftedRep :: RuntimeRep) (CNonCanonical)
========== 3 ==========
given
derived
wanted
[WD] $dEq_a2DX {1}:: Eq p0_a1Tm[tau:2] (CDictCan(psc))
[WD] $dShow_a2DY {0}:: Show p0_a1Tm[tau:2] (CDictCan(psc))
========== 4 ==========
given
derived
wanted
[WD] $dEq_a2DX {1}:: Eq p0_a1Tm[tau:2] (CDictCan)
[WD] $dShow_a2DY {0}:: Show p0_a1Tm[tau:2] (CDictCan)
========== 5 ==========
given
[G] $dShow_a2E3 {0}:: Show p_a2E2[sk:2] (CDictCan)
[G] $dEq_a2E4 {0}:: Eq p_a2E2[sk:2] (CDictCan)
[G] $dShow_a2E3 {0}:: Show p_a2E2[sk:2] (CDictCan)
[G] $dEq_a2E4 {0}:: Eq p_a2E2[sk:2] (CDictCan)
derived
wanted
========== 6 ==========
given
[G] $dShow_a2DZ {0}:: Show p_a1Tm[sk:2] (CDictCan)
[G] $dEq_a2E0 {0}:: Eq p_a1Tm[sk:2] (CDictCan)
[G] $dShow_a2DZ {0}:: Show p_a1Tm[sk:2] (CDictCan)
[G] $dEq_a2E0 {0}:: Eq p_a1Tm[sk:2] (CDictCan)
derived
wanted
I was expecting invocations 3 and one for simplifying its unsolved Wanteds as Givens. I don't know levity polymorphism well enough to grok invocations 02. I don't know why 4 duplicates 3. And I don't know what's going on with 5 and 6: why they have redundant givens and why 5 has different variable uniques. (I'm assuming they're the "backwards inference" invocations.)
Adding a signature here makes a huge difference.
f :: (Eq a,Show a,Enum a) => a > Bool
f x = bar () where
bar () = [x] == [x] && null (show x)
 Dumps:
========== 0 ==========
given
[G] $dEq_a2Ml {0}:: Eq a_a2Mk[sk:2] (CDictCan)
[G] $dShow_a2Mm {0}:: Show a_a2Mk[sk:2] (CDictCan)
[G] $dEnum_a2Mn {0}:: Enum a_a2Mk[sk:2] (CDictCan)
derived
wanted
========== 1 ==========
given
derived
wanted
[WD] $dEq_a2Nd {1}:: Eq a_a2Mv[sk:2] (CDictCan)
[WD] $dShow_a2N7 {0}:: Show a_a2Mv[sk:2] (CDictCan)
========== 2 ==========
given
[G] $dEq_a2Mx {0}:: Eq a_a2Mv[sk:2] (CDictCan)
[G] $dShow_a2My {0}:: Show a_a2Mv[sk:2] (CDictCan)
[G] $dEnum_a2Mz {0}:: Enum a_a2Mv[sk:2] (CDictCan)
derived
wanted
We see that only invocation 1 solves Wanteds. What if we split up the method invocations?
f :: (Eq a,Show a,Enum a) => a > Bool
f x = bar () && baz () where
bar () = [x] == [x]
baz () = null (show x)
 Dumps:
========== 0 ==========
given
[G] $dEq_a2Mm {0}:: Eq a_a2Ml[sk:2] (CDictCan)
[G] $dShow_a2Mn {0}:: Show a_a2Ml[sk:2] (CDictCan)
[G] $dEnum_a2Mo {0}:: Enum a_a2Ml[sk:2] (CDictCan)
derived
wanted
========== 1 ==========
given
derived
wanted
[WD] $dShow_a2N5 {0}:: Show a_a2Mw[sk:2] (CDictCan)
========== 2 ==========
given
derived
wanted
[WD] $dEq_a2Np {1}:: Eq a_a2Mw[sk:2] (CDictCan)
========== 3 ==========
given
[G] $dEq_a2My {0}:: Eq a_a2Mw[sk:2] (CDictCan)
[G] $dShow_a2Mz {0}:: Show a_a2Mw[sk:2] (CDictCan)
[G] $dEnum_a2MA {0}:: Enum a_a2Mw[sk:2] (CDictCan)
derived
wanted
We see two separate solveWanteds invocations.
I think that the fact that we see one solveWanteds invocation per
nested declaration (both here and in the previous example) reflects
the fact that GHC (as discussed in the OutsideIn JFP paper) does not
generalize the nested declarations (i.e. making them polymorphic
functions that accept dictionary arguments, which the RHS of f
would
then need to fabricate and supply; instead, those dictionaries'
bindings are floating all the way up to f
, which its signature
happens to provide directly).
Ambiguity Checks
When we're using type families, it becomes possible to write signatures that are ambiguous, because the type variables are only arguments to type families.
I'm struggling to come up with a good example here, so this one is indeed ambiguous.
type family F a
f :: Eq (F a) => F a > Bool
f x = [x] == [x]
 Dumps:
========== 0 ==========
given
[G] $dEq_a1Ui {0}:: Eq fsk0_a1Uo[fsk] (CDictCan)
[G] cobox_a1Up {0}:: (F a_a1Uh[sk:2] :: *) ~# (fsk0_a1Uo[fsk] :: *) (CFunEqCan)
zonk given
[G] $dEq_a1Ui {0}:: Eq (F a_a1Uh[sk:2]) (CDictCan)
derived
wanted
========== 1 ==========
given
[G] $dEq_a1Ui {0}:: Eq fsk0_a1Uo[fsk] (CDictCan)
[G] cobox_a1Up {0}:: (F a_a1Uh[sk:2] :: *) ~# (fsk0_a1Uo[fsk] :: *) (CFunEqCan)
derived
wanted
[W] $dEq_a1Uu {0}:: Eq (F a0_a1Uj[tau:2]) (CDictCan)
[WD] hole{a1Ut} {2}:: (F a0_a1Uj[tau:2] :: *) ~# (F a_a1Uh[sk:2] :: *) (CNonCanonical)
Test.hs:10:6: error:
* Couldn't match type `F a0' with `F a'
Expected type: F a > Bool
Actual type: F a0 > Bool
NB: `F' is a type function, and may not be injective
The type variable `a0' is ambiguous
* In the ambiguity check for `f'
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: Eq (F a) => F a > Bool

10  f :: Eq (F a) => F a > Bool
 ^^^^^^^^^^^^^^^^^^^^^^^
The [WD] hole
Wanted in invocation 1 is GHC's way of determining whether the signature is ambiguous or not.
With the coxswain
plugin, for example, ambiguity constraints like these arise and must be solved via the plugin's extra knowledge about equivalencies involving the .&
and .=
families.
Conclusions
I unfortunately feel too adrift to draw any conclusions beyond "look at these interesting invocations; be wary of assuming how exactly your solver is invoked and in what order"!
Outstanding Questions
These are questions I still don't know the answer to. They keep me up at night.

When/where exactly do Derived constraints arise? I'm not recognizing them in the OutsideIn paper.

Is there a robust way to maintain solver state across related invocations? I'm currently essentially serializing my state (phase and substitution) as spurious constraints. It's seemingly robust but seems wrong. If GHC maintained some kind of "thread of solving" state tokens I could use those to robustly store and recover my custom solver state in response to GHC's invocations of
tcPluginSolve
separately without having to pollute the constraints. 
GHC has various kinds of variable and skolem (e.g. signature skolem) that I'm not recognizing in the OutsideIn paper. Is there a comprehensive discussion of them all?

What would Core need (I'm hoping just
EvTerm
, actually) to remain statically typed instead of all these coercions the plugin and thesculls
library (i.e. records and variants on top of rows) assert?