diff --git a/projects/Idris/src/LessMacrosMoreTypes/RowPolymorphism.md b/projects/Idris/src/LessMacrosMoreTypes/RowPolymorphism.md
index 3848edd..6763000 100644
--- a/projects/Idris/src/LessMacrosMoreTypes/RowPolymorphism.md
+++ b/projects/Idris/src/LessMacrosMoreTypes/RowPolymorphism.md
@@ -7,13 +7,14 @@ import Data.List
import Data.List.Elem
import Data.List.Quantifiers
+import System
import DependentNuggets.FreshLists
```
Sometimes, especially when dealing with business logic, we have to deal with data that comes in from the real world, or elsewhere, naturally very messily typed, leading to nasty type signatures and messes of macros or code generation to build data structures from a schema. Row polymorphism can help us by abstracting over the fields contained in a record type in the type signature, letting us define records based on data, concatenate records together, and define functions that are generic across any record containing the required fields, all without macros.
-This article is inspired by my work on implementing the _Brown Benchmark for Table Types_(B2T2)[^1] for my _Structures_[^2] library, an update for which will be released soon, providing a much more comprehensive collection of types for row-polymorphic programming.
+This article is inspired by my work on implementing the _Brown Benchmark for Table Types_[^1] for my _Structures_[^2] library, an update for which will be released soon, providing a much more comprehensive collection of types for row-polymorphic programming.
## What is Row Polymorphism
@@ -75,9 +76,11 @@ Imagine you are helping your friend move and they need to figure out what furnit
| room → String | length → Double | width → Double |
|---------------|-----------------|----------------|
-| Bedroom | 3.00 | 6.00 |
-| Kitchen | 2.50 | 2.00 |
-| Bathroom | 1.50 | 1.00 |
+| Bedroom | 3.65 | 3.35 |
+| Living Room | 4.87 | 3.35 |
+| Dining Room | 2.44 | 2.44 |
+| Kitchen | 3.35 | 2.44 |
+| Bathroom | 3.65 | 2.44 |
@@ -93,9 +96,12 @@ Imagine you are helping your friend move and they need to figure out what furnit
| item → String | length → Double | width → Double | height → Double |
|---------------|-----------------|----------------|-----------------|
-| Dresser | 1.00 | 0.25 | 0.80 |
-| Chair | 0.50 | 0.50 | 1.00 |
-| Nightstand | 0.75 | 0.50 | 0.50 |
+| Dresser | 1.00 | 0.60 | 0.76 |
+| Bed | 2.00 | 1.50 | 0.50 |
+| Nightstand | 0.60 | 0.48 | 0.75 |
+| Dinner Table | 1.80 | 0.90 | 0.80 |
+| TV Stand | 1.93 | 0.42 | 0.90 |
+| Coffee Table | 1.81 | 0.81 | 0.46 |
@@ -132,6 +138,11 @@ record Header where
constructor MkHeader
label: String
type: Type
+
+export infixr 8 :>
+public export
+(:>) : String -> Type -> Header
+(:>) str x = MkHeader str x
```
The schema itself is really simple, just an alias for a list of headers:
@@ -151,7 +162,8 @@ We will also need a way to compute the column types from our schema, turning a l
```idris
public export
ColumnTypes : Schema -> List Type
-ColumnTypes xs = map type xs
+ColumnTypes [] = []
+ColumnTypes (h :: hs) = h.type :: ColumnTypes hs
```
### Making a row
@@ -164,7 +176,7 @@ A row is a list of the same length as the schema where every list element has a
```idris
public export
Row : Schema -> Type
-Row xs = HList (ColumnTypes xs)
+Row hs = HList (ColumnTypes hs)
```
We will also want a way of indexing the values in a row by their columns, instead of by their positions. We only want this function to be callable when the row actually _has_ that column, so we also require an inclusion proof, as an auto-implicit so the compiler can generate it for us when possible:
@@ -182,11 +194,163 @@ namespace RowIndex
### Making a table
+The table itself is pretty simple, its just a list of rows:
+
+```idris
+public export
+Table : Schema -> Type
+Table hs = List (Row hs)
+```
+
## Using our tables
-## Row polymorphic functions
+Now that we have a way to describe the type signature of a table, let's go ahead and translate our previous table examples into code:
-### Revisiting our furniture example
+```idris
+Rooms : Schema
+Rooms = ["room" :> String, "length" :> Double, "width" :> Double]
+
+rooms : Table Rooms
+rooms =
+ [ ["Bedroom", 3.65, 3.35]
+ , ["Living Room", 4.87, 3.35]
+ , ["Dining Room", 2.44, 2.44]
+ , ["Kitchen", 3.35, 2.44]
+ , ["Bathroom", 3.65, 2.44]
+ ]
+```
+
+```idris
+Furniture : Schema
+Furniture = ["item" :> String, "length" :> Double, "width" :> Double, "height" :> Double]
+
+furniture : Table Furniture
+furniture =
+ [ ["Dresser", 1.00, 0.60, 0.76]
+ , ["Bed", 2.00, 1.50, 0.50]
+ , ["Nightstand", 0.60, 0.48, 0.75]
+ , ["Dinner Table", 1.80, 0.90, 0.80]
+ , ["TV Stand", 1.93, 0.42, 0.90]
+ , ["Coffee Table", 1.81, 0.81, 0.46]
+ ]
+```
+
+### A simple row polymorphic function
+
+With our tables defined, it's time to revisit our `area` function. The schema will be an implicit variable in the type signature, and we'll constrain it such that both the length and width fields are elements of the schema. These constraints allow us to simply call the `index` function with the given fields on the provided row:
+
+> [!TIP]
+> In a type signature, `x =>` is equivalent to `{auto _ : x} ->`
+
+```idris
+area : {hs : Schema} -> "length" :> Double `Elem` hs => "width" :> Double `Elem` hs =>
+ Row hs -> Double
+area x =
+ let length = ("length" :> Double) `index` x
+ width = ("width" :> Double) `index` x
+ in length * width
+```
+
+Without any further work, we can now call this function on both our room and furniture tables and it works as expected:
+
+> [!NOTE]
+> In this specific context, we do have to explicitly provide the schema to the `area` function to disambiguate, but this can be worked around and should be considered more of an artifact of the limited implementation in this blog post then an intrinsic ergonomics concern.
+
+```idris hide
+-- @@test map area rooms
+mapAreaRooms : IO Bool
+mapAreaRooms = do
+ pure $
+```
+
+
+```idris
+ map (area {hs = Rooms}) rooms == [12.2275, 16.314500000000002, 5.9536, 8.174, 8.905999999999999]
+```
+
+
+```idris hide
+-- @@test map area furniture
+mapAreaFurniture : IO Bool
+mapAreaFurniture = do
+ pure $
+```
+
+
+```idris
+ map (area {hs = Furniture}) furniture == [0.6, 3.0, 0.288, 1.62, 0.8106, 1.4661000000000002]
+```
+
+
+### Building a new column
+
+Just being able to access the fields in a row polymorphic way is pretty neat, but its also not really that impressive. We have much more interesting capabilities at our disposal, like adding new fields. We can take a function that consumes a row and produces a new value, along with a name for the new value, and use that to add a new column to each row in the table:
+
+```idris
+buildColumn : {hs : Schema}
+ -> (f : Row hs -> t) -> (name : String) -> Table hs -> Table (hs ++ [name :> t])
+buildColumn f name table = map buildColumnRow table
+ where
+ addToEnd : {name' : String} -> {hs' : Schema}
+ -> t -> Row hs' -> Row (hs' ++ [name' :> t])
+ addToEnd {hs' = []} x [] = [x]
+ addToEnd {hs' = (y :: ys)} x (x' :: xs) = x' :: addToEnd x xs
+ buildColumnRow : {name' : String} -> Row hs -> Row (hs ++ [name' :> t])
+ buildColumnRow row = addToEnd (f row) row
+```
+
+With this new under our belt, we can make new tables derived from our previous ones, such as adding an area column to our previous two tables:
+
+```idris
+roomsWithArea : Table (Rooms ++ ["footprint" :> Double])
+roomsWithArea = buildColumn {hs = Rooms} (area {hs = Rooms}) "footprint" rooms
+```
+
+```idris hide
+-- @@test roomsWithArea
+roomsWithAreaTest : IO Bool
+roomsWithAreaTest = do
+ pure $
+```
+
+
+```idris
+ roomsWithArea ==
+ [ ["Bedroom", 3.65, 3.35, 12.2275]
+ , ["Living Room", 4.87, 3.35, 16.314500000000002]
+ , ["Dining Room", 2.44, 2.44, 5.9536]
+ , ["Kitchen", 3.35, 2.44, 8.174]
+ , ["Bathroom", 3.65, 2.44, 8.905999999999999]
+ ]
+```
+
+
+```idris
+furnitureWithArea : Table (Furniture ++ ["footprint" :> Double])
+furnitureWithArea = buildColumn {hs = Furniture} (area {hs = Furniture}) "footprint" furniture
+```
+
+```idris hide
+-- @@test furnitureWithArea
+furnitureWithAreaTest : IO Bool
+furnitureWithAreaTest = do
+ pure $
+```
+
+
+```idris
+ furnitureWithArea ==
+ [ ["Dresser", 1.0, 0.6, 0.76, 0.6]
+ , ["Bed", 2.0, 1.5, 0.5, 3.0]
+ , ["Nightstand", 0.6, 0.48, 0.75, 0.288]
+ , ["Dinner Table", 1.8, 0.9, 0.8, 1.62]
+ , ["TV Stand", 1.93, 0.42, 0.9, 0.8106]
+ , ["Coffee Table", 1.81, 0.81, 0.46, 1.4661000000000002]
+ ]
+```
+
+
+### Select
### Implementing Regular Interfaces for Row Types