Daniel's Blog

Agda is a functional programming language with a relatively Haskell-like syntax and feature set, so coming into it, I relied on my past experiences with Haskell to get things done. However, the languages are sufficiently different to leave room for useful design patterns in Agda that can’t be brought over from Haskell, because they don’t exist there. One such pattern will be the focus of this post; it’s relatively simple, but I came across it by reading the standard library code. My hope is that by writing it down here, I can save someone the trouble of 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. I should say that this may not be the only motivation for this pattern; it’s just how I arrived at seeing its value.

Suppose you wanted to define a type class for “a type that has an associative binary operation”. In Haskell, this is the famous Semigroup class. Here’s a definition I lifted from the Haskell docs:

class Semigroup a where
  (<>) :: a -> a -> a
  a <> b = sconcat (a :| [ b ])

It says that a type a is a semigroup if it has a binary operation, which Haskell calls (<>). The language isn’t expressive enough to encode the associative property of this binary operation, but we won’t hold it against Haskell: not every language needs dependent types or SMT-backed refinement types. If we translated this definition into Agda (and encoded the associativity constraint), we’d end up with something like this:

 9
10
11
12
13

    record Semigroup (A : Set a) : Set a where
        field
            _∙_ : A → A → A

            isAssociative : ∀ (a₁ a₂ a₃ : A) → a₁ ∙ (a₂ ∙ a₃) ≡ (a₁ ∙ a₂) ∙ a₃

So far, so good. Now, let’s also encode a more specific sort of type-with-binary-operation: one where the operation is associative as before, but also has an identity element. In Haskell, we can write this as:

class Semigroup a => Monoid a where
    mempty :: a

This brings in all the requirements of Semigroup, with one additional one: 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 snippet.

In Agda, there isn’t really a special syntax for “superclass”; we just use a field. The “transliterated” implementation is as follows:

15
16
17
18
19
20
21
22
23
24

    record Monoid (A : Set a) : Set a where
        field semigroup : Semigroup A

        open Semigroup semigroup public

        field
            zero : A

            isIdentityLeft : ∀ (a : A) → zero ∙ a ≡ a
            isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a

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. 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 being contrived: I am trying to avoid introducing too many definitions and concepts just for the sake of a motivating case. Suppose you are trying to specify a type in which the binary operation has two properties (e.g. it’s a monoid and something else). Since the only two type classes I have so far are Monoid and Semigroup, I will use those; note that in this particular instance, using both is a contrivance, since one contains the latter.

26
27
28
29
30
31
32

    record ContrivedExample (A : Set a) : Set a where
        field
            -- first property
            monoid : Monoid A

            -- second property; Semigroup is a stand-in.
            semigroup : Semigroup A

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 constraint:

26
27
28
29
30
31
32
33
34

    record ContrivedExample (A : Set a) : Set a where
        field
            -- first property
            monoid : Monoid A

            -- second property; Semigroup is a stand-in.
            semigroup : Semigroup A

            operationsEqual : Monoid._∙_ monoid ≡ Semigroup._∙_ semigroup

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, 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 pain point of the original approach is data flow. The way it’s written, 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 these constraints, in addition to having an identity element”. To provide the binary operation to a field, we use type application; this would look something like this:

42

            isSemigroup : IsSemigroup _∙_

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 record header:

37
38

    record IsSemigroup {A : Set a} (_∙_ : A → A → A) : Set a where
        field isAssociative : ∀ (a₁ a₂ a₃ : A) → a₁ ∙ (a₂ ∙ a₃) ≡ (a₁ ∙ a₂) ∙ a₃

We can define an IsMonoid similarly:

40
41
42
43
44
45
46
47

    record IsMonoid {A : Set a} (zero : A) (_∙_ : A → A → A) : Set a where
        field
            isSemigroup : IsSemigroup _∙_

            isIdentityLeft : ∀ (a : A) → zero ∙ a ≡ a
            isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a

        open IsSemigroup isSemigroup public

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:

49
50
51
52
53
54
55

    record IsContrivedExample {A : Set a} (zero : A) (_∙_ : A → A → A) : Set a where
        field
            -- first property
            monoid : IsMonoid zero _∙_

            -- second property; Semigroup is a stand-in.
            semigroup : IsSemigroup _∙_

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:

57
58
59
60
61
62
63
64
65
66

    record Semigroup (A : Set a) : Set a where
        field
            _∙_ : A → A → A
            isSemigroup : IsSemigroup _∙_

    record Monoid (A : Set a) : Set a where
        field
            zero : A
            _∙_ : A → A → A
            isMonoid : IsMonoid zero _∙_

Agda calls records that include both the operation and its IsSomething record bundles (see Algebra.Bundles, for example). 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.

One annoying thing about our definitions above is that we had to accept our binary operation, and sometimes the zero element, as an argument to each one, 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. 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, IsSemigroup, and IsContrivedExample code could look like this:

68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87

module ThirdAttempt {A : Set a} (_∙_ : A → A → A) where
    record IsSemigroup : Set a where
        field isAssociative : ∀ (a₁ a₂ a₃ : A) → a₁ ∙ (a₂ ∙ a₃) ≡ (a₁ ∙ a₂) ∙ a₃

    record IsMonoid (zero : A) : Set a where
        field
            isSemigroup : IsSemigroup

            isIdentityLeft : ∀ (a : A) → zero ∙ a ≡ a
            isIdentityRight : ∀ (a : A) → a ∙ zero ≡ a

        open IsSemigroup isSemigroup public

    record IsContrivedExample (zero : A) : Set a where
        field
            -- first property
            monoid : IsMonoid zero

            -- second property; Semigroup is a stand-in.
            semigroup : IsSemigroup

The more IsSomething records you declare, the more effective this trick becomes.

That’s all I have! The pattern I’ve described shows up all over the Agda standard library; the example that made me come across it was the Algebra.Structures module. I hope you find it useful.

Happy (dependently typed) programming!