When working the latest incarnation of my System IG compiler, I used a thingy which I now realize ought to be characterized as a design pattern. It substantially changed the way I was thinking about the code, which is what makes it interesting.
Summary: separate an algorithm into certificate constructors and a search algorithm.
A large class of algorithms can be considered, in some way, as search algorithms. It is given a problem and searches for a solution to that problem. For example, typically you wouldn’t phrase the quadratic formula as a search algorithm, but it is—it’s just a very smart, fast one. It is given a,b, and c and searches for a solution to the equation ax2 + bx + c = 0.
The certificate design pattern separates the algorithm into two modules: the certificate module and the algorithm. The certificate module provides constructors for solutions to the problem. For each correct solution, it is possible to construct a certificate, and it is impossible to construct a certificate for an incorrect solution. The certificate module for the quadratic formula algorithm might look like this:
module Certificate (Certificate, certify, solution) where data Certificate = Certificate Double Double Double Double certify :: Double -> Double -> Double -> Double -> Maybe Certificate certify a b c x | a*x^2 + b*x + c == 0 = Just (Certificate a b c x) | otherwise = Nothing solution :: Certificate -> (Double,Double,Double,Double) solution (Certificate a b c x) = (a,b,c,x)
There is only one way to construct a Certificate, and that is to pass it a solution to the quadratic equation. If it is not actually a solution, a certificate cannot be constructed for it. This module is very easy to verify. The algorithm module is obvious:
module Algorithm (solve) where import Certificate import Data.Maybe (fromJust) solve :: Double -> Double -> Double -> Certificate solve a b c = fromJust $ certify a b c ((-b + sqrt (b^2 - 4*a*c)) / (2*a))
Here, we use the quadratic formula and construct a certificate of its correctness. If we made a typo in the formula, then certify would return Nothing and we would get an error when we fromJust it (an error is justified in this case, rather than an exception, because we made a mistake when programming — it’s like an assert).
The client to the algorithm gets a certificate back from solve, and can extract its solution. All the information needed to verify that the certificate is a correct certificate for the given problem should be provided. For example, if Certificate had only contained x instead of a,b,c,x, then we could have implemented solve like:
solve a b c = certify 0 0 0 0
Because that is a valid solution, but we have not solved the problem. The client needs to be able to inspect that a,b,c match the input values. Maximally untrusting client code might look like this:
unsafeSolve a b c = let (a',b',c',x) = solution (solve a b c) in assert (a == a' && b == b' && c == c') x where assert True x = x assert False _ = error "Assertion failed"
Here we can give any function whatsoever for solve, and we will never report an incorrect answer (replacing the incorrectness with a runtime error).
This is certainly overkill for this example, but in the System IG compiler it makes a lot of sense. I have a small set of rules which form well-typed programs, and have put in much effort to prove this set of rules is consistent and complete. But I want to experiment with different interfaces, different inference algorithms, different optimizations, etc.
So my Certificate implements combinators for each of the rules in my system, and all the different algorithms plug into that set of rules. So whenever I write a typechecker algorithm, if it finds a solution, the solution is correct by construction. This gives me a lot of freedom to play with different techniques.
Verification rules can be more involved than this single function that constructs a certificate. In the System IG compiler, there are 12 construction rules, most of them taking other certificates as arguments (which would make them certificate “combinators”). I’ll show an example of more complex certificate constructors later.
What is interesting about this pattern, aside from the added correctness and verification guarantees, is that is changed the way I thought while I was implementing the algorithm. Instead of being master of the computer, and telling it what to do, it was more like a puzzle I had to solve. In some ways it was harder, but I attribute that to redistributing the workload; it’s harder because I am forced to write code that is correct from the get-go, instead of accidentally introducing bugs and thinking I’m done.
The other interesting mental change was that it often guided my solution. I would look at the certificate I’m trying to create, and see which constructors could create it. This gave me an idea of the information I was after. This information is the information necessary to convince the client that my solution is correct; I cannot proceed without it.
Theoretically, the algorithm part could be completely generic. It might just do a generic search algorithm like Dijkstra. If it finds a certificate, then it has solved your problem correctly. Solutions for free! (But this will not be practical in most cases — it might not yield a correct algorithm by other criteria, such as “always halts”).
Here’s an example of a more complex certificate. The domain is SK combinator calculus, and a Conversion is a certificate that holds two terms. If a Conversion can be constructed, then the two terms are convertible.
module Conversion ( Term(..), Conversion , convId, convCompose, convFlip , convS, convK, convApp) where infixl 9 :* data Term = S | K | Term :* Term deriving (Eq) data Conversion = Term :<-> Term convTerms (a :<-> b) = (a,b) convId t = t :<-> t convCompose (a :<-> b) (b' :<-> c) | b == b' = Just $ a :<-> c | otherwise = Nothing convFlip (a :<-> b) = b :<-> a convS (S :* x :* y :* z) = Just $ (S :* x :* y :* z) :<-> (x :* z :* (y :* z)) convS _ = Nothing convK (K :* x :* y) = Just $ (K :* x :* y) :<-> x convK _ = Nothing convApp (a :<-> b) (c :<-> d) = (a :* c) :<-> (b :* d)
The export list is key. If we had exported the (:<->) constructor, then it would be possible to create invalid conversions. The correctness of a certificate module is all about what it doesn’t export.
I’m wondering what the best way to present this as an object-oriented pattern is, so I can insert it into popular CS folklore (assuming it’s not already there ;-).