Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Minor wording updates to the Agda post.

Browse Source
This commit is contained in:
Danila Fedorin 2023-08-31 22:30:36 -07:00
parent 48c3105f42
commit 6b24d67409
1 changed files with 8 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
content/blog/agda_is_pattern.md
View File

@ -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 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 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 ### Type Classes for Related Operations
Suppose you wanted to define a type class for "a type that has an associative 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 >}} {{< 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 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), (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 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 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). _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 Notice that the bundles don't rely on other bundles to define properties; that
to the "bottom-up" data flow in which a parent record has to access the operations and would lead right back to the "bottom-up" data flow in which a parent record has
values stored in its fields. Thus, bundles occur only at the top level; you use to access the operations and values stored in its fields. Hower, bundles do
them if they represent _the whole_ algebraic structure you need, rather than sometimes "contain" (via a definition, not a field) smaller bundles, in case,
an aspect of it. for example, you need _only_ a semigroup, but you have a monoid.
### Bonus: Using Parameterized Modules to Avoid Repetitive Arguments ### Bonus: Using Parameterized Modules to Avoid Repetitive Arguments