From 6b24d6740907974951c0f7cba5a2edf416f69ac3 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 31 Aug 2023 22:30:36 -0700 Subject: [PATCH] Minor wording updates to the Agda post. --- content/blog/agda_is_pattern.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/content/blog/agda_is_pattern.md b/content/blog/agda_is_pattern.md index 48d7aba..a7f994a 100644 --- a/content/blog/agda_is_pattern.md +++ b/content/blog/agda_is_pattern.md @@ -16,7 +16,8 @@ recognizing it and understanding its purpose. The pattern is "unique" to Agda (in the sense that it isn't present in Haskell) because it relies on dependent types. In my head, I call this the `IsSomething` pattern. Before I introduce it, let -me try to provide some motivation. +me try to provide some motivation. I should say that this may not be the +only motivation for this pattern; it's just how I arrived at seeing its value. ### Type Classes for Related Operations Suppose you wanted to define a type class for "a type that has an associative @@ -78,7 +79,7 @@ using both is a contrivance, since one contains the latter. {{< codelines "Agda" "agda-issomething/example.agda" 26 32 >}} -However, note the problem: nothing in the above definition ensures that the +However, there's a problem: nothing in the above definition ensures that the binary operations of the two fields are the same! As far as Agda is concerned (as one would quickly come to realize by trying a few proofs with the code), the two operations are completely separate. One could perhaps add an equality @@ -138,11 +139,11 @@ original `Semigroup` and `Monoid` instances. Here's what that would look like: Agda calls records that include both the operation and its `IsSomething` record _bundles_ (see [`Algebra.Bundles`](https://agda.github.io/agda-stdlib/Algebra.Bundles.html), for example). -Notice that the bundles don't contain other bundles; that would lead right back -to the "bottom-up" data flow in which a parent record has to access the operations and -values stored in its fields. Thus, bundles occur only at the top level; you use -them if they represent _the whole_ algebraic structure you need, rather than -an aspect of it. +Notice that the bundles don't rely on other bundles to define properties; that +would lead right back to the "bottom-up" data flow in which a parent record has +to access the operations and values stored in its fields. Hower, bundles do +sometimes "contain" (via a definition, not a field) smaller bundles, in case, +for example, you need _only_ a semigroup, but you have a monoid. ### Bonus: Using Parameterized Modules to Avoid Repetitive Arguments