Especially in languages with nominally \"strong\" type systems, like Rust, macros are quite frequently needed to work around the type system to avoid needless repetition when consuming an API, generate formulaic boilerplate that only exists to please the type system, or work around the lack of variadic functions for things like printf. Lets explore the ways we can use dependently typed constructs to eliminate the need for such macros.",
"post-ids": [
- 5
+ 5,
+ 9
],
"title": "Less Macros, More Types"
}
\ No newline at end of file
diff --git a/lib/DB/IdrisPost.rakumod b/lib/DB/IdrisPost.rakumod
index 1e229ac..2e0f094 100644
--- a/lib/DB/IdrisPost.rakumod
+++ b/lib/DB/IdrisPost.rakumod
@@ -81,7 +81,7 @@ sub katla(*@args --> Str:D) {
unless $katla;
# Modify the output to use our styling instead of katla's
# Remove the style block and line breaks
- $katla-out ~~ s:g/''//;
+ $katla-out ~~ s:g/''//;
$katla-out ~~ s:g/'
'//;
# Use
blocks for the code and inject our own class for idris code
$katla-out ~~ s:g/'' \s*//;
diff --git a/projects/Idris/Idris.ipkg b/projects/Idris/Idris.ipkg
index 20285d8..7766dde 100644
--- a/projects/Idris/Idris.ipkg
+++ b/projects/Idris/Idris.ipkg
@@ -19,6 +19,7 @@ authors = "Nathan McCarty"
modules = Idris
, Posts.HelloWorld
, LessMacrosMoreTypes.Printf
+ , LessMacrosMoreTypes.RowPolymorphism
, DependentNuggets.FreshLists
, TipsAndTricks.ProofSearchAndNonEquality
diff --git a/projects/Idris/src/LessMacrosMoreTypes/RowPolymorphism.md b/projects/Idris/src/LessMacrosMoreTypes/RowPolymorphism.md
new file mode 100644
index 0000000..746924c
--- /dev/null
+++ b/projects/Idris/src/LessMacrosMoreTypes/RowPolymorphism.md
@@ -0,0 +1,117 @@
+# Row Polymorphic Programming
+
+```idris hide
+module LessMacrosMoreTypes.RowPolymorphism
+
+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.
+
+
+## What is Row Polymorphism
+
+At time of writing, the [Wikipedia page](https://en.wikipedia.org/wiki/Row_polymorphism) for row polymorphism starts with
+> In programming language type theory, row polymorphism is a kind of polymorphism that allows one to write programs that are polymorphic on row types such as record types and polymorphic variants.
+and then leads into some mathematical notation heavy text that doesn't really elucidate much, and what the hell does "polymorphic on row types" even mean?
+
+Consider a basic `record` in Idris as an example:
+```idris
+record ImACat where
+ constructor MkCat
+ name : String
+ age : Nat
+ meows_a_lot : Bool
+```
+
+This certainly seems like it might fit the bill, it says `record` right there. But what are these "row types"?
+
+### Row Types
+
+Row types often are called records in other contexts, and while "record" may be a somewhat more intuitive name for someone approaching this from the perspective of many common programming languages, I will continue to largely use the name "row type" as it will make more sense in the tabular data context I will be framing the rest of this post in terms of.
+
+Consider some tabular data, say a table in a database, or a spread sheet. Tabular data is composed of a 2d grid of rows and columns, typically with each column having a name and potentially a type constraint on the values in that column. Consider this example of some tabular data:
+
+
+
+Cats
+
+| name → String | age → Nat | meows_a_lot → Bool |
+|---------------|-----------|---------------------|
+| Cricket | 11 | False |
+| Cookie-Dough | 4 | True |
+| Mango | 0 | False |
+| Creampuff | 5 | True |
+
+
+
+A row type is parameterized by a list of `(label, Type)` pairs, represented by the header of the table. We can see that the labels and types in our *Cats* table are identical to the fields of our `ImACat` record from earlier. Under this view, each row in the table can be thought of as an instance of the `ImACat` record.
+
+That parameterization on a schema, however, makes row types a bit more flexible, as well as a bit more complicated. We can perform the usual operations, like accessing a column in a row by name, but we can also perform new operations that enable a sort of limited, type-safe reflection over row types, such as selecting a specific set of columns from a row to produce a new row type, or concatenating the schemas of two rows to create a new row type expressing the result of joining the two rows.
+
+### The Mysterious Row Polymorphism
+
+Imagine you are helping your friend move and they need to figure out what furniture will fit in what rooms. The current property owner of their new place has graciously provided a table containing the length and width of each room, and their furniture suppler has provided a table detailing the lengths, widths, and heights of the bounding cuboids for each piece of furniture. Let's say the tables look a bit like this:
+
+
+
+Rooms
+
+| room → String | length → Double | width → Double |
+|---------------|-----------------|----------------|
+| Bedroom | 3.00 | 6.00 |
+| Kitchen | 2.50 | 2.00 |
+| Bathroom | 1.50 | 1.00 |
+
+
+
+
+
+Furniture
+
+| 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 |
+
+
+
+One thing that's going to be critical to determine is how much floor space is left in a room after the furniture's been placed in it. After all, a room isn't of much use if there's not even enough free floor space to stand in it. You notice that both of these tables contain the information needed to calculate the available area and the foot prints of the furniture, the `length` and `width` columns.
+
+Its tempting to define a `Room` data type and a `Furniture` data type containing each table's respective columns as fields, and describe the surface area/footprint via an `Area` interface. However, this approach has several drawbacks. It requires implementing the interface manually for each data type[^3], can hide certain categories of error like inadvertently using the wrong field to calculate the area, and is potentially quite fragile if the structure of the tables changes on us or we need to add more tables to our system.
+
+We can do better. With our parameterized row types we can write an `area` function that is defined to work on any row type that has a `length` and a `width` column of type `Double`. This is the essence of row polymorphism, writing code that's generic not over what interfaces a type implements, but instead is generic over what fields the type contains.
+
+## Building our own Runtime Reflection
+
+### Building the Schema
+
+### Computing Our Table Types
+
+## Making and Using tables
+
+## Things this blog post's implementation does wrong
+
+[^1]:
+
+[^2]:
+
+[^3]: At best, we might be able to get away with something like a derive macro, but that's still something we have to invoke manually
diff --git a/resources/colors.css b/resources/colors.css
index 4b0bf8c..6f9fecc 100644
--- a/resources/colors.css
+++ b/resources/colors.css
@@ -112,6 +112,37 @@ footer > div {
background-color: var(--bg-2);
}
+/* Color table elements */
+
+.md-table {
+ background-color: var(--bg-1);
+}
+.md-table .md-table-title {
+ background-color: var(--bg-0);
+ /* color: var(--dim-0); */
+}
+
+.md-table tbody tr:nth-child(odd) {
+ background-color: var(--bg-2);
+}
+
+.md-table th, .md-table td {
+ border-left-color: var(--cyan);
+}
+
+.md-table th {
+ color: var(--fg-1);
+ background-color: var(--bg-0);
+ border-top-color: var(--green);
+ border-bottom-color: var(--green);
+}
+.md-table thead tr th:first-child {
+ border-left-color: var(--green);
+}
+.md-table thead tr th:last-child {
+ border-right-color: var(--green);
+}
+
/* Formatting for special pages */
.special-post h2 {
color: var(--green);
@@ -120,6 +151,7 @@ footer > div {
color: var(--red);
}
+
/* Colorization for idris code blocks */
code {
color: var(--code-fg-0);
diff --git a/resources/main.css b/resources/main.css
index 787e907..208ca53 100644
--- a/resources/main.css
+++ b/resources/main.css
@@ -167,6 +167,66 @@ blockquote {
padding: var(--box-padding-vert) var(--box-padding-horz);
}
+.md-table {
+ /* width: 90%; */
+ min-width: 60%;
+ max-width: 90%;
+ display: block;
+ padding: var(--box-margin-vert) var(--box-margin-horz);
+ gap: var(--box-gap);
+ border-radius: var(--box-radius);
+ display: flex;
+ align-items: center;
+ justify-content: center;
+ flex-direction: column;
+}
+
+.md-table-title {
+ padding: var(--box-margin-vert) var(--box-padding-horz);
+ border-radius: var(--box-radius);
+ font-weight: 800;
+ font-size: 1.25rem;
+}
+
+table {
+ table-layout: auto;
+ width: 100%;
+ border-collapse: collapse;
+}
+
+th, td {
+ border-left: 0.1rem dotted;
+}
+
+table th, table td {
+ padding: 0.5rem 0.5rem;
+}
+
+th {
+ border-top: 0.2rem solid;
+ border-bottom: 0.2rem solid;
+
+}
+
+thead tr th:first-child {
+ border-left: 0.2rem solid;
+}
+thead tr th:last-child {
+ border-right: 0.2rem solid;
+}
+
+tbody tr td:first-child {
+ border-left: 0.1rem dotted;
+}
+
+tbody tr td:last-child {
+ border-right: 0.1rem dotted;
+}
+
+tbody tr:last-child td {
+ border-bottom: 0.1rem dotted;
+}
+
/* Style the tags blurbs and page */
.tags {
display: flex;