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

Finish and publish the IsSomething article

Browse Source
This commit is contained in:
Danila Fedorin 2023-08-31 22:16:26 -07:00
parent 032453c4d0
commit 48c3105f42
2 changed files with 39 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
code/agda-issomething/example.agda
View File

@ -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 _∙_

39
content/blog/agda_is_pattern.md
View File

@ -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.