wiki:Plugins/TypeChecker/RowTypes/Coxswain

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.

  • -fplugin-opt=Coxswain:summarize This will dump out the "before-and-after" constraints of each time GHC gives the plugin a "task" (e.g. solve the Wanted constraints in some definition's RHS).
  • -fplugin-opt=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").
  • -fplugin-opt=Coxswain:logfile=<file> This will write that output to the specified file instead of to the default of stderr.

Demonstration

Comparison to the Nice Elm Overview

To get a basic sense of what the library feels like, the following code block imitates the well-written and beginner-friendly 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 row-types and the RowTypes module and record-types 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 -fconstraint-solver-iterations=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 list-shaped 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 well-established 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 type-level 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 is t -- it's the "identity" field structure.
  • F f l t is f t -- it wraps the column type in a functor.
  • (f :->: g) l t is f l t -> g l t -- it's a function between field structures.
  • C a l t is a -- a constant field structure.
  • D c l t is a dictionary for c 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.

Back to vpartition

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 list-shaped 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 the R type. Feel free to think of it as KnownNat (NumCols p).
  • R f p is a record for the row p where each field l .= t inhabits f l t.
  • I l t is a newtype around t, so an I-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 of R's product of columns.
  • The F f l t field type is a newtype around f t, so R (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; like I and F, f :->: g is a newtype around f l t -> g l t.
  • rHasCol builds a record where each field is evidence of its own existence! Here the field structure (like I and F) is HasCol p l t, which is a GADT evidencing that the row p has a column l .= 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 the Identity Applicative achieves over from the lens 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 run-time 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 Anys 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 Showable, Monoids, 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 list-shaped 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 -dsuppress-all 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 well-behaved, 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, type-indexed records/variants, permissions/privileges trackings, restricted/indexed monads, etc!

In fact, I think such type-indexed 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.

Front-End Plugins

Would a front-end 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 eta-expansion 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 math-functions package, the `newtonRaphson` function has the following signature.

-- | Solve equation using Newton-Raphson 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 per-column comments.

VoR Generics

Especially if we had intersection / union / width subtyping, etc --- I think (type-indexed?) Variants of (type-indexed?) Records would be an excellent representation type, generalizing the sum-of-products 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 type-indexed sum where each summand is a nominal record type (i.e. a proper Haskell data type or a newtype wrapped record type).

Command-Line Options Parser

I suspect a Variant of Records would be an excellent center piece of the interface to a command-line option parsing library, building upon Gonzalez's http://hackage.haskell.org/package/options.

YAML/JSON/CSV/etc Format

These popular "human-readable" 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 self-explanatory, I think.

Modular/Extensible Free "Effects" Monad

A type-indexed 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 multi-dimensional array: each dimension would have a strongly-typed 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 in-memory representation (e.g. row-col vs col-row) 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/en-us/research/publication/first-class-labels-for-extensible-rows/ - Lots of inspiring use-cases for rows, records, and variants.

Vytiniotis et all 2011 - https://www.microsoft.com/en-us/research/publication/outsideinx-modular-type-inference-with-local-assumptions/ - 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/typechecker-plugins/ and https://github.com/adamgundry/uom-plugin/ - The only published type checker plugin I'm aware of. Very helpful.

Gundry et al 2015 - https://ghc.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/type-checker-plugin/ - 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 Re-implement 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 type-equality 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" Cts 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 out-of-date, either wrong or mysteriously referring to source Notes that no longer exist.

Obviously, the plugin needs to simplify Cts 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.

  1. Immediately upon receiving Givens, thaw Row skolem vars, i.e. replace them by unification vars with the same kind and level. This enables certain Given-Given 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.

  1. Importantly, when renaming the skolems, I also create some fake Given constraints Ren p_sk p_tau where p_tau is the temporary replacement of p_sk. This is a robust way for me to later recover the Row var equalities that GHC's solver learned for me.
  1. When finished simplifying givens (i.e. if I would be returning TcPluginOk _ []), replace any remaining thawed variables (I dissatisfyingly filter based on a fsLit "$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.

  1. 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 up-to-date 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 "out-of-date cached expansion" I'm seeing is because I'm creating ill-formed 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].)

Preserve CFunEqCan

Never mutate/discard CFunEqCans! 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 up-to-date (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.

Inefficient Nat dictionaries

Evidence bindings for KnownNat are essentially Integers, 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 Word16s 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 pretty-prints its inputs and is a no-op 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 0-2. 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 solve-Wanteds invocations.

I think that the fact that we see one solve-Wanteds 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 the sculls library (i.e. records and variants on top of rows) assert?
Last modified 2 months ago Last modified on Sep 18, 2017 3:48:15 PM