Add article about the 'deeply embedded expression' pattern

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

.gitmodules

@@ -13,3 +13,6 @@
 [submodule "code/compiler"]
 	path = code/compiler
 	url = https://dev.danilafe.com/DanilaFe/bloglang.git
+[submodule "code/agda-spa"]
+	path = code/agda-spa
+	url = https://dev.danilafe.com/DanilaFe/agda-spa.git

code/agda-spa

@@ -0,0 +1 @@
+Subproject commit f0da9a902005b24db4e03a89c2862493735467c4

config-gen.toml

@@ -1,5 +1,8 @@
 [params]
   [params.submoduleLinks]
+    [params.submoduleLinks.agdaspa]
+      url = "https://dev.danilafe.com/DanilaFe/agda-spa/src/commit/f0da9a902005b24db4e03a89c2862493735467c4"
+      path = "agda-spa"
     [params.submoduleLinks.aoc2020]
       url = "https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020/src/commit/7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82"
       path = "aoc-2020"

content/blog/agda_expr_pattern.md

@@ -0,0 +1,229 @@
+---
+title: "The 'Deeply Embedded Expression' Trick in Agda"
+date: 2024-03-11T14:25:52-07:00
+tags: ["Agda"]
+---
+
+I've been working on a relatively large Agda project for a few months now,
+and I'd like to think that I've become quite proficient. Recently, I came
+up with a little trick to help simplify some of my proofs, and it seems like
+this trick might have broader applications.
+
+In my head, I call this trick 'Deeply Embedded Expressions'. Before I introduce
+it, let me explain the part of my work that motivated developing the trick.
+
+### Proofs about Map Operations
+
+A part of my Agda project is the formalization of simple key-value maps.
+I model key-value maps as lists of key-value pairs. On top of this, I implement
+two operations: `join` and `meet`, which in my code are denoted using `⊔` and `⊓`.
+When "joining" two maps, you create a new map that has the keys from both input ones.
+If a key is only present in one of the input maps, then the new "joined" map
+has the same value for that key as the original. On the other hand, if the key
+is present in both maps, then its value in the new map is the result of "joining"
+the original values. The "meet" operation is similar, except instead of taking
+keys from either map, the result only has keys that were present in both maps,
+"meeting" their values. In a way, "join" and "meet" are similar to set union
+and intersection --- but they also operate on the values in the map.
+
+Given these operations, I need to prove certain properties of these operation.
+The most inconvenient to prove is probably associativity:
+
+{{< codelines "agda" "agda-spa/Lattice/Map.agda" 752 752 >}}
+
+This property is, in turn, proven using two 'subset' relations on maps, defined
+in the usual way.
+
+{{< codelines "agda" "agda-spa/Lattice/Map.agda" 755 755 >}}
+{{< codelines "agda" "agda-spa/Lattice/Map.agda" 774 774 >}}
+
+The reason this property is so inconvenient to prove is that there are a
+lot of cases to consider. That's because your claim, in words, is something
+like:
+
+> Suppose a key-value pair `k , v` is present in `(m₁ ⊔ m₂) ⊔ m₃`. Show
+> that `k , v` is also in `m₁ ⊔ (m₂ ⊔ m₃)`.
+
+The only thing you can really do with `k , v` is figure out how it got into
+the three-way union map: did it come from `m₁`, `m₂`, or `m₃`, or perhaps
+several of them? The essence of the proof boils down to repeated uses
+of the fact that for a key to be in the union, it must be in at least one
+of the two maps. You end up with witnesses, repeated application of the same
+lemmas, lots of `let`-expressions or `where` clauses. It's relatively tedious
+and, what's more frustrating, __driven entirely by the structure of the
+map operations__. It seems like one shouldn't have to mimic that structure
+using boilerplate lemmas. So I started looking at other ways.
+
+### Case Analysis using GADTs
+
+A "proof by cases" in a dependently typed language like Agda usually brings
+to mind pattern matching. So, here's an idea: what if for each expression
+involving `⊔` and `⊓`, we had some kind of data type, and that data type
+had exactly as many inhabitants as there are cases to analyze? A data type
+corresponding to `m₁ ⊔ m₂` might have three cases, and the one for
+`(m₁ ⊔ m₂) ⊔ m₃` might have seven. Each case would contain the information
+necessary to perform the proof.
+
+A data type whose "shape" depends on an expression in the way I described above
+is said to be _indexed by_ that expression. In Agda, GADTs are used to create
+indexed types. My initial attempt was something like this:
+
+```Agda
+data Provenance (k : A) : B → Map → Set (a ⊔ℓ b) where
+    single : ∀ {v : B} {m : Map} → (k , v) ∈ m → Provenance k v m
+    in₁ : ∀ {v : B} {m₁ m₂ : Expr} → Provenance k v e₁ → ¬ k ∈k m₂ → Provenance k v (e₁ ⊔ e₂)
+    in₂ : ∀ {v : B} {m₁ m₂ : Expr} → ¬ k ∈k m₁ → Provenance k v m₂ → Provenance k v (e₁ ⊔ e₂)
+    bothᵘ : ∀ {v₁ v₂ : B} {m₁ m₂ : Expr} → Provenance k v₁ m₁ → Provenance k v₂ m₂ → Provenance k (v₁ ⊔ v₂) (e₁ ⊔ e₂)
+    bothⁱ : ∀ {v₁ v₂ : B} {m₁ m₂ : Expr} → Provenance k v₁ m₁ → Provenance k v₂ m₂ → Provenance k (v₁ ⊓ v₂) (e₁ ⊓ e₂)
+```
+
+I was planning on a proof of associativity (in one direction) that looked
+something like the following --- pattern matching on cases from the new
+`Provenance` type.
+
+```Agda
+⊔-assoc₁ : ((m₁ ⊔ m₂) ⊔ m₃) ⊆ (m₁ ⊔ (m₂ ⊔ m₃))
+⊔-assoc₁ k v k,v∈m₁₂m₃
+    with get-Provenance k,v∈m₁₂m₃
+...   | in₂ k∉km₁₂ (single v∈m₃) = ...
+...   | in₁ (in₂ k∉km₁ (single v∈m₂)) k∉km₃ = ...
+...   | bothᵘ (in₂ k∉km₁ (single {v₂} v₂∈m₂)) (single {v₃} v₃∈m₃) = ...
+...   | in₁ (in₁ (single v₁∈m₁) k∉km₂) k∉km₃ = ...
+...   | bothᵘ (in₁ (single {v₁} v₁∈m₁) k∉km₂) (single {v₃} v₃∈m₃) = ...
+...   | in₁ (bothᵘ (single {v₁} v₁∈m₁) (single {v₂} v₂∈m₂)) k∉ke₃ = ...
+...   | bothᵘ (bothᵘ (single {v₁} v₁∈m₁) (single {v₂} v₂∈m₂)) (single {v₃} v₃∈m₃) = ...
+```
+
+However, this doesn't work. Agda has trouble figuring out which cases of
+the `Provenance` GADT are allowed, in which aren't. Is `m₁ ⊔ m` a single map,
+fit for the `single` case, or should it be broken up into more cases like
+`in₁` and `in₂`? In general, is some expression of type `Map` the "bottom"
+of our recursion, or should it be analyzed further?
+
+The above hints at what's wrong. The mistake here is requiring Agda to infer
+the shape of our "join" and "meet" expressions from arbitrary terms.
+The set of expressions that we want to reason about is much more restricted --
+each expression will always be of three components: "meet", "join", and base-case maps being
+combined using these operations.
+
+### Defining an Expression Data Type
+If you're like me, and have spent years of your life around programming language
+theory and domain specific languages (DSLs), the last sentence of the previous
+section may be ringing a bell. In fact, it's eerily similar to how we describe
+recursive grammars:
+
+> An expression of interest is either,
+> * A map
+> * The "join" of two expressions
+> * The "meet" of two expressions
+
+Mathematically, we might write this as follows:
+
+{{< latex >}}
+\begin{array}{rcll}
+    e & ::= & m & \text{(maps)} \\
+      &  |  & e \sqcup e & \text{(join)} \\
+      &  |  & e \sqcap e & \text{(meet)}
+\end{array}
+{{< /latex >}}
+
+And in Agda,
+
+{{< codelines "agda" "agda-spa/Lattice/Map.agda" 543 546 >}}
+
+In the code, I used the set union and intersection operators
+to avoid overloading the `⊔` and `⊓` more than they already are.
+
+We have just defined a very small expression language. In computer science,
+a language is called _deeply embedded_ if a data type (or class hierarchy, or
+other 'explicit' representation) is defined for its syntax in the _host_
+language (Agda, in our case). This is in contrast to a _shallow embedding_, in
+which expressions in the (new) language are just expressions in the host
+language.
+
+In this sense, our `Expr` is deeply embedded --- we defined new container for it,
+and `_∪_` is a distinct entity from `_⊔_`. Our first attempt was a shallow
+embedding. That fell through because the Agda language is much broader than
+our expression language, which makes case analysis very difficult.
+
+An obvious thing to do with an expression is to evaluate it. This will be
+important for our proofs, because it will establish a connection between
+expressions (created via `Expr`) and actual Agda objects that we need to
+reason about at the end of the day. The notation \\(\\llbracket e \\rrbracket\\)
+is commonly used in PL circles for evaluation (it comes from
+[Denotational Semantics](https://en.wikipedia.org/wiki/Denotational_semantics)).
+Thus, my Agda evaluation function is written as follows:
+
+{{< codelines "agda" "agda-spa/Lattice/Map.agda" 586 589 >}}
+
+On top of this, here is my actual implementation of the `Provenance` data type.
+This time, it's indexed by expressions in `Expr`, which makes it much easier to
+pattern match on instances:
+
+{{< codelines "agda" "agda-spa/Lattice/Map.agda" 591 596 >}}
+
+Note that we have to use the evaluation function to be able to use
+operators such as `∈`. That's because these are still defined on maps,
+and not expressions.
+
+With this, I was able to write my proof in the way that I had hoped. It has
+the exact form of my previous sketch-of-proof.
+
+{{< codelines "agda" "agda-spa/Lattice/Map.agda" 755 773 "" "**(click here to see the full example, including each case's implementation)**" >}}
+
+### The General Trick
+
+So far, I've presented a problem I faced in my Agda proof and a solution for
+that problem. However, it may not be clear how useful the trick is beyond
+this narrow case that I've encountered. The way I see it, the "deeply embedded
+expression" trick is applicable whenever you have data that is constructed
+from some fixed set of cases, and when proofs about that data need to follow
+the structure of these cases. Thus, examples include:
+
+* **Proofs about the origin of keys in a map (this one):** the "data" is the
+  key-value map that is being analyzed. The enumeration of cases for this
+  map is driven by the structure of the "join" and "meet" operations used
+  to build the map.
+* **Automatic derivation of function properties:** suppose you're interested
+  in working with continuous functions. You also know that the addition,
+  subtraction, and multiplication of two functions preserves continuity.
+  Of course, the constant function \\(x \\mapsto c\\) and the identity function
+  \\(x \\mapsto x\\) are continuous too. You may define an expression data type
+  that has cases for these operations. Then, your evaluation function could
+  transform the expression into a plain function, and a proof on the
+  structure of the expression can be used to verify the resulting function's
+  continuity.
+* **Proof search for algebraic expressions:** suppose that you wanted to
+  automatically find solutions for certain algebraic (in)equalities. Instead
+  of using some sort of reflection mechanism to inspect terms and determine
+  how constraints should be solved, you might represent the set of operations
+  in you equation system as cases in a data type. You can then use regular
+  Agda code to manipulate terms; an evaluation function can then be used
+  to recover the equations in Agda, together with witnesses justifying the
+  solution.
+
+There are some pretty clear commonalities about examples above, which
+are the ingredients to this trick:
+
+* __The expression:__ you create a new expression data type that encodes all
+  the operations (and bases cases) on your data. In my example, this is
+  the `Expr` data type.
+* __The evaluation function__: you provide a way to lower the expression
+  you've defined back into a regular Agda term. This connects your (abstract)
+  operations to their interpretation in Agda. In my example, this is the
+  `⟦_⟧` function.
+* __The proofs__: you write proofs that consider only the fixed set of cases
+  encoded by the data type (`Expr`), but state properties about the
+  _evaluated_ expression. In my example, this is `Provenance` and
+  the `Expr-Provenance` function. Specifically, the `Provenance` data type connects
+  expressions and the terms they evaluate to, because it is indexed by expressions,
+  but contains data in the form `k ∈k ⟦ e₂ ⟧`.
+
+### Conclusion
+I'll be the first to admit that this trick is quite situational, and may
+not be as far-reaching as the ["Is Something" pattern](https://danilafe.com/blog/agda_is_pattern/)
+I wrote about before, which seems to occur far more in the wild. However, there
+have now been two times when I personally reached for this trick, which seems
+to suggest that it may be useful to someone else.
+
+I hope you've found this useful. Happy (dependently typed) programming!

themes/vanilla

@@ -1 +1 @@
-Subproject commit 4a5dfac221a6cd0d16f82079c49991d1b576749e
+Subproject commit 9b9a6dca5fb3993ee60e0eb71192fb0a318b6e35