This blog post and after action report is three months overdue, but I participated in Zurich hack 2022. Zurich hack is a voluntary hackaton organized in Rapperswil-Jona ³, with as theme improving the Haskell ecosystem and socializing. Naturally I chose to work on the most research-y project I could find. Sandy was happy to oblige with his denotational design project. Here we build an “infinite” baseless chip design, with a homomorphism in natural numbers to proof correctness, more on this in the proofs and programs section.

Our presentation was surprisingly good considering we slapped it together in 30 minutes. However, I think we could’ve done a better job at explaining denotational design, and we could’ve elaborated more on why proving matters. I shall use this post to fill in these gaps. For starters the presentation can be seen here:

I helped presenting¹, however most of the implementation was done by Sandy and Nathan. I wish I could’ve done more, but my Agda isn’t good enough yet. I helped with cheering on their proving efforts and coming up with ideas for the design.

Denotational design

Let’s begin on what denotational design is. You could watch a video on this, but summarized in my own words:

• We should decompose parts when possible.
• Abstractions shouldn’t leak.
• We should look for elegance.

The first point is “We should decompose parts when possible”. This means breaking up our design in such a way we can re-use parts into a larger whole. For example in Zurich hack, our first designs was a large record for multiplication that had everything baked into it. Then someone had the idea to split that record into a separate addition and multiplication records and re-express multiplication into addition. This allows us to work with the simpler problem of addition, before tackling multiplication. Which is what we eventually settled upon as well. I don’t think decomposition has been stated as an explicit goal of denotational design before, but it feels implied. Perhaps in Conals talk, “principled construction of correct implementation” can be interpreted as such.

The point about “Abstractions shouldn’t leak” is quite interesting. We wish to provided a simplified view of the world to the user through abstraction. In practice this means we should hide the implementation from the user. I once suggested for example to add a xor operation to our record to get rid of the carry bit in certain cases. After some discussion we settled on not doing this because xor isn’t really a thing you care about when thinking in terms of semirings³. In other words, when thinking in terms of multiplication and addition, you don’t want to care about the bit representation. For more examples of “abstractions shouldn’t leak” I recommend the book algebra driven design.

The final point is “We should look for elegance”. Which should serve as a compass upon iteration. Here again I’ve an example from just after Zurich hack: The overflow bit in our addition record bugged me. It kind off exposes the internals of addition. So I decided to delete it in favor of doing a full co-product instead. Doing this would break both multiplication and addition records, the proofs have to be redone, I’m not even sure if it’s possible. So there is definitely a cost. ⁴ However I like that design, it’s more elegant because this would make multiplication have a product type as input, and addition a sum type. Which would have some nice symmetry. This is something we didn’t drive home enough in the Zurich hack presentation. The proof we presented looked impressive, but this isn’t something you necessarily want. An elegant proof and design is what you want.

Proofs and programs

I pondered on proofs in software and how dependent types interplay. Is the design I dreamed up correct? How do you know this? We used a property called a homomorphism to prove correctness. In mortal words, our chip design was interpreted into natural numbers and we showed that addition and multiplication would be the same for our chip, as it is in natural numbers.

To start talking about proofs, we need a design and implementation to proof correctness for. In our case this was a chip design in Agda. This Adder⁶ is something we settled upon after several iterations of design, but I’m cutting that part out for brevity:⁵

record Adder {τ : Set} {size : ℕ} (μ : τ → Fin size) : Set where
  constructor adds
  field
    add : Fin 2 × τ × τ → τ × Fin 2 -- 1
    zeroA : τ -- 2
    proof-add -- 3
      : (mnp : Fin 2 × τ × τ)
      → toℕ (digitize (P.map μ id (add mnp))) 
      ≡ toℕ (addF'3 (P.map id (P.map μ μ) mnp)) 
open Adder

Here we’re saying, to define an adder you need 3 things. You need an add operation 1, you need a zero 2 ⁸, and you need a proof of addition 3. The proof of addition is the homomorphism from our chip to the natural numbers. Furthermore we don’t specify the input type, which is represented by τ. This is done because we want a baseless chip design. We’re fine with arbitrary inputs, As long as we can interpreted this, represented by μ. In μ the Fin size indicates a finite size, which we need because we want to map our design to the real world, which is finite.

Not shown from the record is that we’re able to make a bigger adder out of a smaller one trough composition of two adders. composition chips allows us to “grow” this size without needing to re-prove correctness. We only need to prove composition is correct. All of this also holds for our eventual multiplication design. which is build from an adder and composition of other multiplication chips. We shall see that proving correctness of composition isn’t easy. Once done, all compositions will provably correct however. ⁷

A concrete example of μ would be an interpertation into binary values:

interpretBF : Bool → Fin 2
interpretBF false = zero
interpretBF true  = suc zero

If we put this into the Adder then τ = Bool. interpretBF in this case interprets our code as a boolean value in natural numbers. In other words the homomorphism. This says what value a true and a false are in natural numbers. Now can define how to add bits:

add2 : Adder interpretBF -- 1
add add2 (zero , false , false)     = false , zero -- 2
...
add add2 (suc zero , true , true)   = true  , suc zero
zeroA add2 = false -- 3

Here we first define the type of add2 at 1. This uses the previously defined interpretBF to set τ = Bool. Then we start giving an implementation for add at 2, which is a simple pattern match into values. finally we give an implementation of zeroA at 3.

You can do a quick correctness check before doing a full prove. For example, in multiplication we didn’t do the full on homorphism prove at first. It looked daunting, so we settled on making a unit test instead. If we map out all possible inputs to all possible outputs we got a crummy proof:

_ : (V.map -- 1
        (toℕ ∘ pairμ (pairμ interpretBF) ∘ uncurry (mult mul2x2)) $ 
        composeTheValues allBools2x2 allBools2x2
    )
        ≡ (0 ∷ 0 ∷ 0 ∷ 0 ∷  -- 2
           0 ∷ 1 ∷ 2 ∷ 3 ∷
           0 ∷ 2 ∷ 4 ∷ 6 ∷
           0 ∷ 3 ∷ 6 ∷ 9 ∷ [])
_ = refl

At 1 we put our chip design into the interpretation, and at 2 we expect a multiplication table as result. Is this test complete? No, this only works for binary values up to 9, we’ve not tested for trits or pentits or higher values. We did prove however the chip behaves like we expect for these values. If you’re building a chip company where you only need multiplication up to 9 in base 2 this is good enough. As far unit tests go this is incredibly thorough because we’re testing against all possible values in the chip design. The more common approach is to sample a couple values and call it a day.

Which lead to an alternative approach called property testing. Here you would generate two random inputs on one side, interpret it trough the homomorphism and then see if the multiplication in natural numbers is the same as the test. We didn’t do this because it’s sort of difficult to do in Agda.⁹ Now you need to figure out how to get your source of randomness. Also time was a serious constraint, and we had a more powerful and interesting technique, proving! A proof doesn’t have to be hard, for example consider the correctness prove for our add2 chip:

  proof-add add2 (zero , false , false) = refl
  ...
  proof-add add2 (suc zero , true  , true)  = refl

refl means, reflexivity. In other words, the statement is simple enough that Agda can just look at the definition to figure out what it means. In this case all we do is list out all possible input values, and tell agda to look at the definition. proof-add‘s type signature ensures the implementation is correct. This is only possible because Agda is dependently typed. What we proved is that the homorphism is the same under composition for the addition.

This will work for the add2 chip. However the add2 chip is kindoff useless by itself since it can only add 2 bits. Our idea was to compose these adders into bigger adders so that any size can be represented. To do this we first define the type signature:

bigger-adder : {σ τ : Set} {σ-size τ-size : ℕ} {μ : σ → Fin σ-size} {ν : τ → Fin τ-size}
  → Adder μ -- 1
  → Adder ν -- 2
  → Adder (uncurry combine ∘ P.map μ ν) -- 3

Here we’re putting in a low adder 1, a high adder 2 which results into a combined adder 3. μ and ν are placeholders for different adders. This allows us to for example add trits to bits. The resulting adder 3 maps over both sides of the resulting tuple¹⁵ with the interpertation.

If you squint a little, the implementation looks like a circuit:

add (bigger-adder x y) -- 1
  (cin , (mhi , mlo) , (nhi , nlo)) -- 2
  = let -- 3
      (lo , cmid) = y .add $ cin , mlo , nlo 
      (hi , cout) = x .add $ cmid , mhi , nhi
    in ((hi , lo) , cout) -- 4

At 1 we’re copattern matching on bigger-adder so we can get the underlying μ and ν adders as x and y respectively. At 2 we’re getting the actual arguments into the bigger adder. The type of this is $ Fin _2 \times (\sigma \times \tau) \times (\sigma \times \tau)$ this is where the carry comes into play as argument since an adder needs to be able to tell when it overflows ¹⁴. The actual addition in 3 we pawn off to the underlying adders x and y, all we do is hook in the carry¹⁶. In 4 we emit the results.

Once we were reasonably confident of our implementation, we want to prove this correctness. This is a bit more involved than proving the boolean interpretation:

proof-add (bigger-adder {σ-size = σ-size} {τ-size = τ-size} {μ = μ} {ν = ν} x y)
          (cin , (mhi , mlo) , (nhi , nlo))
  with y .add (cin , mlo , nlo) in y-eq
... | (lo , cmid) with x .add (cmid , mhi , nhi) in x-eq
... | (hi , cout) =
  let x-proof = proof-add x (cmid , mhi , nhi) -- 3
      y-proof = proof-add y (cin  , mlo , nlo)
      size = σ-size
  in begin
  begin
    toℕ (cast _ (combine cout (combine (μ hi) (μ lo)))) -- 1
  ≡⟨ toℕ-cast _ (combine cout (combine (μ hi) (μ lo))) ⟩
    toℕ (combine cout (combine (μ hi) (μ lo)))
  ≡⟨ toℕ-combine cout _ ⟩
    size * size * toℕ cout + toℕ (combine (μ hi) (μ lo))
  ≡⟨ cong (\ φ → size * size * toℕ cout + φ) (toℕ-combine (μ hi) (μ lo)) ⟩
    size * size * toℕ cout + (size * toℕ (μ hi) + toℕ (μ lo))
  ≡⟨ {! taneb !} ⟩
    toℕ (addF' cin (combine (μ mhi) (μ mlo))) + toℕ (combine (μ nhi) (μ nlo))
  ≡⟨ sym $ toℕ-addF' (addF' cin (combine (μ mhi) (μ mlo))) (combine (μ nhi) (μ nlo)) ⟩
    toℕ (addF' (addF' cin (combine (μ mhi) (μ mlo))) (combine (μ nhi) (μ nlo))) -- 2
  ∎

Note I drastically shortened this proof to make it fit ¹². What do is making the first line (indicated by 1) be the same as the last line (indicated by 2) through steps with equational reasoning. Every step is small, and the process is almost fully mechanical pattern matching. A step is anything within ≡⟨ ⟩, which does some small syntax transformation. The ≡⟨ {! taneb !} ⟩ is a missing step, called a hole. In this case we request taneb¹⁰, to figure out what goes here. In 3, we’re summoning the proofs from the x and y adders to use in the proof later. We’re making a bigger proof out of smaller ones.

If this proof is incorrect, you’ll get a compile error.¹¹ This is similar to property tests, although it doesn’t use randomness and shrinking, but rather the structure of the implementation through dependent types. This is a big step up in terms off correctness compared to property tests. No longer can you have stochastic issues like insufficient sampling, or biased distributions. Furthermore smaller proofs compose into larger ones (with the right design). We can see that for example with x-proof in the above block. Not just that, but every step between ≡⟨ ⟩ is a prove being re-used. Property tests however aren’t as composable as proofs. A value generator may be re-used, however care must be taken the sampling and bias doesn’t become unacceptable. Finally we’re able to prove on polymorphic type variables, which property tests can’t do. If you have software that /needs/ to be correct, I think this dependently typed prove approach is a very good option to consider. I also think Agda is an good choice for a language that supports that.

Parting words

Denotational design is an excellent topic of study if you’re struggling with questions like “how do I make my code be more pretty?”, or “how do I design nice and easy to understand libraries?”. Furthermore, even for commercial code bases we can have correctness proofs. This is a much more powerful technique than mere property tests, and puts all that hype around dependent types to work. We don’t need to rely on hand wavy laws asserted merely by stochastic approximations of proofs, we can do the real deal! Please reach out if you’re in a domain where correctness like this is important. I’d love to chat :).

Finally I especially want to thank to both Nathan and Sandy for giving useful feedback on my humble writings. I also wish thank all other volunteers who participated, I had a great time.