More work on post

projects/Idris/src/LessMacrosMoreTypes/RowPolymorphism.md

@@ -3,6 +3,11 @@
 ```idris hide
 module LessMacrosMoreTypes.RowPolymorphism
 
+import Data.List
+import Data.List.Elem
+import Data.List.Quantifiers
+
+
 import DependentNuggets.FreshLists
 ```
 
@@ -100,18 +105,105 @@ Its tempting to define a `Room` data type and a `Furniture` data type containing
 
 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
+### Pros and Cons
+
+While row polymorphism does come with the downside of loosing proof-of-intentionality[^4] , so to speak, it does come with some major upsides. Two columns in two different tables having the same names and types, doesn't always mean that they are semantically equivalent, but its often a pretty good bet, especially when they are coming from the same source. More importantly, thinking about data types in terms of what values they contain rather than what behavior they implement is often a much better way to think about messy real-world data that was laid out with a dynamically typed language in mind on a good day, and not laid out with computers in mind at all on a bad day.
+
+Like so many things in programming, its a trade off. Low level systems programming, where almost all the data you are working with was generated by the computer, often by systems you also control isn't going to get much benefit from row polymorphic programming. Other tasks like frontend, business logic, and video games quite frequently deal with extremely messy data that has only loosely defined shape and doesn't want to fit neatly into a type hierarchy have a lot to gain from row polymorphism. In the former category, you are more likely to hurt from the loss of semantic guarantees and end up needlessly weakening your type system and tripping over yourself more than you would without it. In the messier situation, you are instead likely to both end up saving type fighting with the type system trying to fit your data to it, and also run into the downsides of row polymorphism much less frequently.
+
+Row polymorphism is also a fantastic way to think about assigning types to code that was originally written for a dynamically typed programming language[^5]. In my personal experience I have found that when an experienced programmer who really seems like they should know better is making some weird sounding arguments about how type systems decrease their productivity and aren't working it, they seem to usually be complaining about the lack of row polymorphism (or the closely related structural subtyping) in the popular statically typed languages, just without having the technical vocabulary for it.
+
+## To Type a Table
+
+One of the core features of row polymorphism is that the labels and types of the columns are determined by a piece of data, a list like structure containing pairs of labels and types. In languages built specifically to be row polymorphic, this data describing the column structure is often implicit. Idris, however, isn't built to be row polymorphic. It's type system just happens to be powerful enough that we can build it on our own, so we will have to build a schema composed of straight up pairs of labels and types.
+
+A more developed library would probably use bespoke types for most of these components, but for the sake of keeping things concise, we'll use regular ol' lists as much as possible.
 
 ### Building the Schema
 
-### Computing Our Table Types
+To make things just a little bit cleaner, we'll define our own data type for the pairs, which we will call `Header`:
 
-## Making and Using tables
+> [!NOTE]
+> Remember that the Idris concept called a `record` is a distinct concept, and Idris `record`s are _not_ the row types we are going to be building.
 
-## Things this blog post's implementation does wrong
+```idris
+public export
+record Header where
+  constructor MkHeader
+  label: String
+  type: Type
+```
+
+The schema itself is really simple, just an alias for a list of headers:
+
+```idris
+public export
+Schema : Type
+Schema = List Header
+```
+
+
+We will also need a way to compute the column types from our schema, turning a list of headers into a list of types:
+
+> [!TIP]
+> This function has an UpperCamelCase name because it is intended to be called in type signatures. This is both conventional, and reduces ambiguity as it can't be confused for a lowercase, implicitly defined, argument name.
+
+```idris
+public export
+ColumnTypes : Schema -> List Type
+ColumnTypes xs = map type xs
+```
+
+### Making a row
+
+A row is a list of the same length as the schema where every list element has a type determined by the header in the same position of the schema:
+
+> [!TIP]
+> `HList` is a standard library type with type constructor `List Type -> type`. Each type in the list of types determines the type of value in that position of the list. Notice this also constrains the length of the list, it must be exactly the same as the length of the list of types. This can be thought of as a more primitive version of the `Row` type we are building.
+
+```idris
+public export
+Row : Schema -> Type
+Row xs = HList (ColumnTypes xs)
+```
+
+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: 
+
+> [!TIP]
+> A value of type `Elem x xs` is a proof that the value `x` is included in the list `xs`, which also encodes its position in the list. The type signature of the `prf` argument thus reads "`h` is an element with known position in `hs`"
+
+```idris
+namespace RowIndex
+  export
+  index : {hs : Schema} -> (h : Header) -> (r : Row hs) -> {auto prf: h `Elem` hs} -> h.type
+  index {hs = (_ :: hs)} h (x :: xs) {prf = Here} = x
+  index {hs = (_ :: hs)} h (y :: ys) {prf = (There x)} = index h ys
+```
+
+### Making a table
+
+## Using our tables
+
+## Row polymorphic functions
+
+### Revisiting our furniture example
+
+### Implementing Regular Interfaces for Row Types
+
+### Generating table types for sql schemas, with runtime example
+
+## Simplifications made for the sake of this blog post
+
+- Hardcoding string as the label type
+- Feilds aren't nullable
+- Not validating the consistency of the schema
 
 [^1]: <https://github.com/brownplt/B2T2>
 
 [^2]: <https://git.sr.ht/~thatonelutenist/Structures>
 
 [^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
+
+[^4]: Generally speaking, with "traditional" data types, an interface typically requires some manual intervention from the programmer to be implemented for a given type. This provides a level of assurance that the implementation over that data type is intentional, and thus likely semantically valid.
+
+[^5]: For instance, typescript's structural subtyping is a very good approximation of row polymorphism, and this is something I believe has contributued just as much to its success as a javascript replacement as its backwards compatibility. A statically typed langauge that could run existing javascript code, but made it a battle to assign types to that existing javascript code, wouldn't be very useful as a transition language.

projects/Idris/todo.org

@@ -0,0 +1,6 @@
+* UX improvements
+** TODO Make headers automatically link to themselves
+** TODO Footnotes on hover
+** TODO Switch to mastodon powered comments
+* Purely cosmetic improvements
+** TODO Make blockquotes fancy

resources/main.css

@@ -96,7 +96,6 @@ body, .post, .series {
 
 
 /* Style the post header, body, and blurbs */
-/* TODO: Style footnotes and get footnote hover working */
 .post-header, .post-body, .series-header {
     display: flex;
     flex-direction: column;
@@ -160,7 +159,6 @@ body, .post, .series {
     border-radius: 0.25em;
 }
 
-/* TODO: Nice fancy blockquotes */
 blockquote {
     width: 90%;
     border-radius: var(--box-radius);