From 48c3105f42e1e2af2188d8e5a5b51a914c9aee2b Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 31 Aug 2023 22:16:26 -0700 Subject: [PATCH] Finish and publish the IsSomething article --- code/agda-issomething/example.agda | 16 ++++++++++++ content/blog/agda_is_pattern.md | 39 ++++++++++++++++++------------ 2 files changed, 39 insertions(+), 16 deletions(-) diff --git a/code/agda-issomething/example.agda b/code/agda-issomething/example.agda index 0b7b177..81fd591 100644 --- a/code/agda-issomething/example.agda +++ b/code/agda-issomething/example.agda @@ -46,6 +46,14 @@ module SecondAttempt where open IsSemigroup isSemigroup public + record IsContrivedExample {A : Set a} (_∙_ : A → A → A) : Set a where + field + -- first property + monoid : IsMonoid _∙_ + + -- second property; Semigroup is a stand-in. + semigroup : IsSemigroup _∙_ + record Semigroup (A : Set a) : Set a where field _∙_ : A → A → A @@ -69,3 +77,11 @@ module ThirdAttempt {A : Set a} (_∙_ : A → A → A) where isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a open IsSemigroup isSemigroup public + + record IsContrivedExample : Set a where + field + -- first property + monoid : IsMonoid _∙_ + + -- second property; Semigroup is a stand-in. + semigroup : IsSemigroup _∙_ diff --git a/content/blog/agda_is_pattern.md b/content/blog/agda_is_pattern.md index b0fec6b..48d7aba 100644 --- a/content/blog/agda_is_pattern.md +++ b/content/blog/agda_is_pattern.md @@ -1,7 +1,6 @@ --- title: "The \"Is Something\" Pattern in Agda" -date: 2023-08-28T21:05:39-07:00 -draft: true +date: 2023-08-31T22:15:34-07:00 tags: ["Agda"] description: "In this post, I talk about a pattern I've observed in the Agda standard library." --- @@ -49,24 +48,24 @@ class Semigroup a => Monoid a where ``` This brings in all the requirements of `Semigroup`, with one additional one: -an element `mempty`, which is intended to be said identity element for `(<>)`. +an element `mempty`, which is intended to be the aforementioned identity element for `(<>)`. Once again, we can't encode the "identity element" property; I say this only -to explain the lack of any additional code in the preceding code snippet. +to explain the lack of any additional code in the preceding snippet. In Agda, there isn't really a special syntax for "superclass"; we just use a field. The "transliterated" implementation is as follows: {{< codelines "Agda" "agda-issomething/example.agda" 15 24 >}} -This code might require a little bit of explanation. Like I said, the "parent" -class is brought in as a field, `semigroup`. Then, every field of `semigroup` +This code might require a little bit of explanation. Like I said, the base class +is brought in as a field, `semigroup`. Then, every field of `semigroup` is also made available within `Monoid`, as well as to users of `Monoid`, by using an `open public` directive. The subsequent fields mimic the Haskell definition amended with proofs of identity. We get our first sign of awkwardness here. We can't refer to the binary operation very easily; it's nested inside of `semigroup`, and we have to access its fields -to get ahold of (∙). It's not too bad at all -- it just cost us an extra line. +to get ahold of `(∙)`. It's not too bad at all -- it just cost us an extra line. However, the bookkeeping of what-operation-is-where gets frustrating quickly. I will demonstrate the frustrations in one final example. I will admit to it @@ -89,14 +88,14 @@ constraint: However, this will get tedious quickly. Proofs will need to leverage rewrites (via the `rewrite` keyword, or via `cong`) to change one of the binary operations -into the other. As you build up more and more complex algebraic structures, on +into the other. As you build up more and more complex algebraic structures, in which the various operations are related in nontrivial ways, you start to look for other approaches. That's where the `IsSomething` pattern comes in. ### The `IsSomething` Pattern: Parameterizing By Operations The pain point of the original approach is data flow. The way it's written, -data (operations, elements, etc.) flows from the fields of a type to the record -that contains them: `Monoid` has to _read_ the (∙) operation from `Semigroup`. +data (operations, elements, etc.) flows from the fields of a record to the record +itself: `Monoid` has to _read_ the `(∙)` operation from `Semigroup`. The more fields you add, the more reading and reconciliation you have to do. It would be better if the data flowed the other direction: from `Monoid` to `Semigroup`. `Monoid` could say, "here's a binary operation; it must satisfy @@ -109,7 +108,7 @@ something like this: Here's the part that's not possible in Haskell: we have a `record`, called `IsSemigroup`, that's parameterized by a _value_ -- the binary operation! This new record is quite similar to our original `Semigroup`, except that it doesn't need a field -for (∙): it gets that from outside. Note the additional parameter in the +for `(∙)`: it gets that from outside. Note the additional parameter in the `record` header: {{< codelines "Agda" "agda-issomething/example.agda" 37 38 >}} @@ -118,17 +117,24 @@ We can define an `IsMonoid` similarly: {{< codelines "Agda" "agda-issomething/example.agda" 40 47 >}} -Note that we want to make an "is" version for each algebraic property; this way, +We want to make an "is" version for each algebraic property; this way, if we want to use "monoid" as part of some other structure, we can pass it the required binary operation the same way we passed it to `IsSemigroup`. +Finally, the contrived motivating example from above becomes: -Of course, these new records are not quite original to our original ones. They +{{< codelines "Agda" "agda-issomething/example.agda" 49 55 >}} + +Since we passed the same operation to both `IsMonoid` and `IsSemigroup`, we +know that we really do have a _single_ operation with _both_ properties, +no strange equality witnesses or anything necessary. + +Of course, these new records are not quite equivalent to our original ones. They need to be passed a binary operation; a "complete" package should include the binary operation _in addition_ to its properties encoded as `IsSemigroup` or `IsMonoid`. Such a complete package would be more-or-less equivalent to our original `Semigroup` and `Monoid` instances. Here's what that would look like: -{{< codelines "Agda" "agda-issomething/example.agda" 49 58 >}} +{{< codelines "Agda" "agda-issomething/example.agda" 57 66 >}} 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). @@ -146,9 +152,10 @@ and to thread it through to all the fields that require it. Agda has a nice mechanism to help alleviate some of this repetition: [parameterized modules](https://agda.readthedocs.io/en/latest/language/module-system.html#parameterised-modules). We can define a _whole module_ that accepts the binary operation as an argument; it will be implicitly passed as an argument to all of the definitions within. -Thus, our entire `IsMonoid` and `IsSemigroup` code could look like this: +Thus, our entire `IsMonoid`, `IsSemigroup`, and `IsContrivedExample` code could +look like this: -{{< codelines "Agda" "agda-issomething/example.agda" 60 71 >}} +{{< codelines "Agda" "agda-issomething/example.agda" 68 87 >}} The more `IsSomething` records you declare, the more effective this trick becomes.