Dependently typed theorem proving is about using the power of dependent types to provide guarantees over various properties of software programs and mathematical constructs. In dependently typed programming we use dependent types to construct and better reason about the properties of our software programs.
While the former requires that we construct proofs, the latter requires that we construct a usable system. In this post I want to discuss how proving and construction can get in the way of each other and that when programming with dependent types we must recognise and tread carefully the fine line between theorem proving and programming.
A Helper
To help with our example we need a little helper data structure that I like to use. This is a reformulation of a list of dependent pairs, and is analogous to the forall list quantifier.
Setting
Our motivating example will be examining the stopping condition for a simple declarative function-less specificiation language with linear-types. Within our language a specification can end iff all linear types have been used.
The precise terms, their semantics, and how usage types are represented is irrelevant for this dicsussion. What is important is how we represent the context and check for the stopping condition.
Usage types
We encode our usage annotations using the following enumerated type.
Types
Types will be A or B types.
Context
We simply describe the context as a list of name type usage pairings.
The Problem: Accounting for freedom.
Our problem is that we want to ensure that our type-level stopping condition requires that all bound terms in our typing context have been used.
We first see how using a typically straight forward approach leads to a valid program that is not informative for describing what is wrong.
Rather trivially we can represent this as a deciable test on the context.
Stating that Items are used.
First, we describe a predicate to describe in an entry in our context is used:
If the item is linear it must be ‘consumed’.
If the item has unrestricted usage, it has been used.
With ItemIsUsed we can show that a Free variable cannot have neen used:
We can use this ‘fact’ to write a decision procedure that given an item in our context tells us if it has been used or not.
Stating that contexts have been used.
Using ListD we can then provide quantification over a context stating that ALL items have been used.
The decision procedure to check if a context has been used is straightforward.
If the head is free then the context has not all been used.
If the rest of the context has a free item then the context has not all been used.
Simply, a context has been used if all items have been used, otherwise there is too much freedom.
The Real Problem
The real problem here is how can we construct an error message stating which elements in the context are free!
A really simple solution is to perform a value level computation to examine the context and report on the free entries.
However, we can do something a bit more interestingdate: 2020-05-04-DecidablyUninformative.md
Decidably Informative
The Dec data type is a powerful tool in dependently typed programming/proving to represent decidable information.
We have seen this with allUsed.
However a problem with Dec is that it is not informative in the negative case, only the positive.
We can prove the negative case, but not use that to construct error messages. For instance, with entries are free in our context.
Enter the DecInfo
DecInfo is variant of Dec to support construction of useful error messages for the negative case in a decidable procedure.
There is a copy of this in my containers library.
Like Dec if we can prove something true then present evidence.
If we can prove something false then allow us to provide something that helps describe why.
An Example
We illustrate DecInfo with the following example:
Record where in the context the error occurred and report the name of the free variable.
Our new version of allUsed' is minimally modified, we add in the error reporting.
Two examples:
Here we show some examples.
The first demonstrates DecInfo in action showing the result of calling allUsed' on a context with a free variable.
Using this information, we can now use it to construct an error message containing the name of the free variable.
However, there is a problem.
Both Dec and DecInfo are greedy and will return at the first sign of trouble.
With two free variables in the context proof can only be constructed that the first element si free.
Expanding ?rhs will fail to find a solution.
Impact
The Impact here is that one will only discover each free variable in the context in turn as and when you fix the problems. While this might be acceptable to some, to others it is not. Surely we can report each an every free item in the context in a more formal way.
First we must recognise some freedom:
Freedom
Separating the Wheat from the Chaff.
Order preserving encodings (thinnings) are a cool technique to keep account of items at the type-level.
In their simplest form we can use a thinning-like structure to show that items in our context will either be free or be used. We show this as follows.
ShowState records if items in the context are free or not.
Here we have used a simple list structure, perhaps a better one will be a vector with an envariant that the length of free and used is equal to the length of the context.
Empty contexts are okay.
If an item in our context is free, and we have proof of said freedom, then add the entry to the list of free entries.
If an item in our context is not free, and we have proof of said usage, then add the entry to the list of used entries.
A problem with this approach is that we require distinct proofs to show freedom and usage. When writing the corresponding function to construct this view then we do not have a way to show what to do in the negative case. That is, if something is not free then we must test if it is used if it si not used then we must test if it is free and if it is not free then we must test if it has been used ad infinitum.
A better approach would be to go back to our original statement about entry usage and forumlate our thinning as one that keeps proofs that an item is free, and proofs of void representing that an item has been used.
We use this formulation to allow us to preserve the ‘positive proof’ that something is used, and thus retain information required for error reporting.
Our ShowState now becomes:
We use a wrapper data type TheState to remove the need for dependent pairs and type-level quantification of free and used entries.
Further, TheState provides proof of the things that are free, and things that are used.
With TheState we can now construct a function to calculate the view and its proofs:
and with this view use it to return a list of all names of free variables in our context. When using this function in production we can examine the output to determine if there are unused variables, and if so which ones, together with the knowledge that how we do so is robust.
As an example here is a context from before showing isFree in action.
Coda
Programming with dependent types is cool and we can use those types to reason more precisely and informatively about our software programs. When we do theorem proving our proofs do not ‘fail’ once they are written; they are proofs of correctness.
However, and especially when dealing with user input, we need the ability to be able to provide informative error messages in our software programs.
Decision procedures such as Dec and DecInfo are limited in what information they can present to construct error messages, and we need to think more carefully about how we use these tools in our code.
Hopefully, you may have learned something from this.
As a side note:
If we examine the structure of TheState, and its use in calcState and isFree we can see that if is essentially a ‘verified’ version of filter.
Compare with this forumlation that I borrowed from a Frenchman.