Dependently typed Under
Marshall Lochbaum’s BQN array language language’s Under modifier is nifty. I use it for my blog’s templating engine (GitHub: barbell).
In Structural vs. Mathematical “Under” Morten Kromberg notes that he’s “very uneasy” by the fact that BQN overloads both structural and mathematical Under.
I have been thinking about what an array programming language built around recursion schemes would look like. I ended up approaching this with Lean 4.
In doing so, I ended up thinking what a dependently typed Under would look like. I split the definition into three variants depending on how lawful each is:
- Obverse: a lawless Under
- Section: has a left inverse
- Iso: has both left and right inverse
I then used explicit complement types to define structural Under. This defines that Structural Under is either:
- Structural Section
- Structural Iso
The Section variants permits encoding e.g. filter operations such that the complement (i.e., values which did not pass the filter) gets smuggled into inverse operator later. The iso variant takes the “usual” approach, which requires that the forward pass masks values.
To enforce shape preservation, I ended up using F-algebra homomorphisms. The homomorphism is a proof obligation that works extrinsically. This means that it’s a sort of refinement type, which says that two F-algebras must produce the same result. For shape preservation this is the length.
That is, there is a simple F-algebra which just counts the elements in a list. Then some operation that does a structural transformation must meet at the same result produced by the counting algebra.
When structural operations are composed together, we can reason whether the selections operate on disjoint parts of the array. This disjointness can be reasoned from the viewpoint of complement types, so it works for structural Sections and Isos. This allows the disjointness of such compositions to be reasoned similar to how concurrent separation logic reasons about parallelism. So, we can write theorems in Lean 4 whether some program made of structural Unders can be run in parallel.
Anyway, a working draft is available at https://preprint.juuso.dev/ch2.pdf