π-Ware – M.Sc thesis project
I just defended my M.Sc thesis, and therefore concluded the master programme “Programming Technology” at Utrecht University. Two years of hard work and the most awesome title of all was finally conferred upon me: “Master of Science” ☺
Thus it might be a good time to finally talk here about what was the subject of the thesis project: hardware design. More specifically, I developed a library for hardware description, simulation, synthesis and verification of circuits, and this library was embedded in the dependently-typed Agda programming language.
But what does this all actually mean?
First of all, dependent types: in a language with dependent types, you can have types that depend on values. More specifically, the types of function arguments can depend on the values of other (previous) arguments. Consider, for example, a function to take a prefix of a vector (Vec). The type signature of take in Agda might look as follows:
take : ∀ {α m n} → Vec α (m + n) → Vec α mThat is, given a certain amount of elements to be “taken” (m), we can then require the type of the passed Vec to have a length of at least m (its length is m + n, for some n).
So, by using dependent types in this function, we can guarantee at compile time that it will never be passed an argument with length less than m. Any attempt at a “bad” call anywhere in the program would cause a type error during compilation. In this way, dependent types can help to “constrain” the domain of functions, avoiding unexpected cases during runtime and preventing bugs.
Programming is proving – Proving is programming
Another use of dependent types is to guarantee properties of the returned value of functions. It is known for a long time in Computer Science that a certain “duality” exists between programming language’s type systems and logics. This is often called the Curry-Howard correspondence (or isomorphism), and was reportedly mentioned for the first time by Alonzo Church in the 1930s.
The Curry-Howard correspondence states that each type system of a programming language has a corresponding logic, and so for each type corresponds a logic formula. Terms of a given type can be viewed as proofs of the corresponding formula.
This is all useful when we want, for example, to ensure that a function returns a value satisfying some desired property. A simple example is a function that “splits” a given vector at a given position, returning a pair of the resulting left and right parts. For this “splitting” function to be correct, the concatenation of the returned “left” and “right” parts needs to result in the original vector passed as argument. And we can indeed establish a type for splitAt that returns the “pair of parts” together with a proof that the returned pair satisfies our definition of correctness.
splitAt : (xs : Vec α (m + n)) → ∃₂ λ (ys : Vec α m) (zs : Vec α n) → ys ++ zs ≡ xsThe type of splitAt can be read as:
Given a vector (xs) of length m + n, there is a vector ys of length m
and a vector zs of length n such that ys ++ zs ≡ xs.The library I developed for hardware design – called Π-Ware – uses all aforementioned features of dependently-typed programming in order to ban certain classes of design mistakes, and to provide static guarantees (at compile time) of circuit well-formedness.
For example, well-typed circuit models in Π-Ware can never:
- Have floating wires
- Short-circuit
- Have combinatorial loops
Furthermore, using the Curry-Howard isomorphism we can proof, in Agda itself, properties of circuits described in Π-Ware (such as functional correctness).
TL;DR
For more details about Π-Ware you can consult the M.Sc thesis that I wrote about it ☺, available here.
Π-Ware’s GitHub repository contains the thesis report, slides about Π-Ware from the thesis defense and other presentations, as well as, of course, the full Agda source code of the library (as a git submodule under the agda directory).
