The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jeff,

 

> > This is e.g done by working in the computational world with types without dependent restrictions and formulate the restrictions as separate lemmas and group the two together with modules or typeclasses.

 

> Do you have an example which illustrates this way of working?

 

I guess many or even most things done in Coq work this way. A good introductory example is this paper by Andrew W. Appel on red black trees http://www.cs.princeton.edu/~appel/papers/redblack.pdf.

 

It specifies, implements and verifies a red black tree in 4 steps:

 

1.)    Define a module type specifying a Set of elements (which need to have an order)

2.)    Define programs which implement such a set as a red black trees

3.)    Provide Lemmas which show that the red-black tree implementation actually fulfills the specification given in 1).

4.)    Give a module implementation for the module type defined in 1.) using the implementations and lemmas from 2.) and 3.)

Step 2 is in the not dependently typed computational world – it would look very similar in OCaml. Step 1 and 3 are in the dependently typed proof term world and in a way step 4 puts the two worlds together and checks if everything is done properly. In this approach pretty much all of the complicated dependently typed terms are opaque proof terms, automatically created with tactics and never looked at by the user -  very different from the AGDA approach.

 

One can do this in other ways with increasing level of usage of dependent types. E.g. one could have defined the red black tree type such that it must always maintain the order of the keys. As done in the paper above, the definition of the red black tree type (Inductive tree) has no such restriction. Having such restrictions can be tricky because then even intermediate results must maintain this property, and you can’t use any algorithms which violate the key order just temporarily. As done above only the output of an algorithm must maintain this property, if its input does. On the other hand it could be helpful to do it in a dependently typed way – it might guide you to the correct implementation of the algorithm.

 

The next step would be to define the red black tree type such that it always must maintain the red-black tree property. And yet another way of doing it would be to define a type implementing a set as specified in step 1.) right away.

 

The more advanced dependent types you use in computational code, the more advanced dependent types constructs you have to write down (manually) to implement your programs. On the other hand, the more the type checker can help you to do things properly right away (rather than proving correctness afterwards). And the features in Coq to automate parts of this are increasing.

 

As I said, I am still in the process of finding out which level of usage of dependent types works best in a highly automated industrial environment. It is a tricky design decision. The book by Adam Chlipala I linked in my previous post is probably still the best introduction to the topic, but IMHO won’t get you far enough to take the right decisions for larger projects.

 

Another difficult decision is the mix of modules, type classes and canonical instances you use to encapsulate specifications (what you give in step 1. above).

 

My advice would be to experiment with this, e.g. try to do the red black tree example with different levels of usage of dependent types. The example is advanced enough to show you where the issues are.

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928