Rubrication

I’ve mentioned a number of times that given a sufficiently rich type theory we can use the type to provide a specification for the function, such that the function is correct by construction. I’d like to give a simple example of how this works in the Coq proof assistant.

The following code is an illustration of how the type theory of Coq allows you to fully specify the behaviour of functions. Kragen Sitaker made the comment that there weren’t too many reasonable interpretations of the function of the type given to the assoc function:

A -> list (A * B) -> option B

that is, a function taking an element of type A, a list of pairs of A and B, to the possibility of a B (and possible failure). That got me wondering how hard it would be to tighten the noose so that there was only one way to interpret the type but still possibly many implementations that satisfy the type, all of which will yield the same result.

The following code illustrates that this is indeed possible to do in Coq.

Require Import List.
Parameter A : Set.
Parameter B : Set.
Definition assoc_list := list (A * B)%type.
Parameter eq_dec : forall (x:A) (y:A),{x=y}+{x<>y}.

Theorem assoc :
  forall (x:A) (l: assoc_list),
    {y | In (x,y) l} + {forall (y:B), ~In (x,y) l}.
  refine
    (fix assoc (x:A) (l:assoc_list) {struct l}
      : {y | In (x,y) l} + {forall (y:B), ~In (x,y) l}
      := match l
           return {y | In (x,y) l} + {forall (y:B), ~In (x,y) l}
           with
           | nil => inright _ (fun y => (fun p : In (x,y) nil => _))
           | ((x',y)::t) =>
             match eq_dec x x' with
               | left lft => inleft _ (exist _ y _)
               | right rgt => match assoc x t with
                                | inleft (exist y p) => inleft _ (exist _ y _)
                                | inright inrgt => inright _ _
                              end
             end
         end) ; clear assoc ; eauto ; subst. constructor. reflexivity.
  firstorder. intros. intro. inversion H ; clear H. firstorder. congruence.
  apply (inrgt y0). assumption.
Defined.

This isn’t the most beautiful code but what it lacks in beauty of implementation it makes up for in ease of reading. There are only a couple of lines that you need to understand to be assured that this is in fact the correct implementation.

Theorem assoc :
  forall (x:A) (l: assoc_list),
    {y | In (x,y) l} + {forall (y:B), ~In (x,y) l}.

This function has a type that takes an “x” of type “A”, a list of pairs and supplies a value “y” of type “B” with a proof that it came from a pair in which the x provided occurs *AND* that that pair exists in the list l. If the function can’t find a pair from which to supply a y, it must supply a proof that no such pair exists in the list.

First a bit of the notation so you can read this theorem properly

{ y | P y }

Can be read: “there exists a y such that the property P holds of y”.

The notation:

A + {B}

Means that we must supply an A or a proof of B.

The “In” predicate is an inductive predicate which specifies membership in a list and is provided by the Coq library.

With a little practice reading types, we can see that the two lines are correct. We can then run Coq on this code to check that the proof is correct and we can be assured of the correctness of the implementation WITHOUT EVER READING THE CODE! This means we have reduced the problem of correctness to two simple lines of completely declarative statements.

This function is more complicated than a normal assoc function because it carries all of these proof terms along with it. However, because of the clever people involved in writing Coq we have actually mixed two different type universes together. One (called Set) for values and one (called Prop) for proofs. Coq uses this fact to do something very clever. The {y|P y} existential type and the A+{B} type are designed such that the “P y” proof and the {B} proof disappear when we extract (compile) our code. As an illustration of this amazing fact look at the following ocaml code which has been automatically extracted from our definition:

let rec assoc x = function
  | Nil -> Inright
  | Cons (p, t) ->
      let Pair (x', y) = p in
      (match eq_dec x x' with
         | Left -> Inleft y
         | Right -> assoc x t)

Voila! Not only are the proof terms gone, but this is pretty much the code you probably would have written yourself. Notice that “Inright” is a constructor with no information (other than failure), basically implementing the “Nothing” of a Maybe type, and the “Inleft” as the “Just” of a Maybe type.

We have extracted a provably terminating, well specified, totally correct function that runs in ocaml! And to top it off we can also compile to Haskell!!

assoc :: A -> Assoc_list -> Sumor B
assoc x l =
  case l of
    Nil -> Inright
    Cons p t ->
      (case p of
         Pair x' y ->
           (case eq_dec x x' of
              Left -> Inleft y
              Right -> assoc x t))

So it isn’t as if this isn’t without some cost. There is a huge learning curve on Coq and I’m by no means an expert. The proofs can be arduous, and although this one only took me a couple of minutes, it took far longer than it would have to implement the function directly in ocaml. However as I gain experience with Coq, I increasingly believe the approach will scale better than traditional approaches to software design.

In addition to these caveats there is more than one function that satisfies this type. Namely there is an assoc which starts returning from the end of the list, instead of the beginning. We could get rid of this problem by specifying which of the elements should be returned, returning all of them, or restricting formation of assoc’s such that they are mappings. The latter is very elegant, but somewhat more involved than what we have done.

Functional programming reduces the difficulty of writing correct software by reducing the ways in which bugs can occur. However, most functional programming languages are unable to put complex constraints like “this is a sorted list” or “implements an assoc function” into the language. When other functions rely on the behaviour all kinds of funny things can happen.

I recently had a nasty non-termination bug in SML because a function *required* that the input list be sorted or the function wouldn’t terminate. My sort routine made use of a bogus less-than-equal predicate over a data-type which I had neglected to write properly. This caused hours of very difficult debugging.

I’m acting on the thesis that I can avoid these problems and I am rewriting a large program in Coq as an experiment. I’ll let you know how it goes.

In my last post I described how unbelievably cool modules are in Coq. Well it turns out that there is some disagreement in the community about whether one should even use them!

Why? Because the type system in Coq is so powerful we hardly even need them. In fact with a bit of syntactic sugar for inductively defined types and the generation of constructors we magically get something like first class modules (first-class meaning modules that are actually values that can be passed around to functions etc…). Enter the Record.

Record MonadBind : Type :=
  { M : forall (A : Type), Type;
    bind : forall (A B : Type), M A -> (A -> M B) -> M B;
    ret : forall (A : Type), A -> M A;
    left_unit : forall (A B : Type) (f : A -> M B) (a : A),
      bind A B (ret A a) f = f a;
    right_unit : forall (A B : Type) (m : M A),
      bind A A m (ret A) = m;
    bind_assoc : forall (A B C : Type) (m : M A) (f : A -> M B) (g : B -> M C) (x : B),
      bind B C (bind A B m f) g = bind A C m (fun x => bind B C (f x) g)
  }.

This implements exactly the same strict controls on the instantiation of a Monad that were given with our MONAD signature in the previous post. Each type can rely on previously defined types in the record giving us the full dependent type system needed to specify a proper monad. With a little bit of work we can rewrite our module to be an instantiation of a record.

Look here for the example code

How cool is that!

I’ve been playing with the Coq proof assistant over the past few days, following closely on some frustrations that I’ve been having with using SML’s module system and a bit of toying with type-classes in Haskell.

The gist of the problem is this. Although you can define type-classes and modules such that external users of these modules/type-classes see a uniform interface, consistency is left as an exercise for the implementer. This is not really acceptable in my view. When you are writing software, often times *you* are the implementer. What you really want is for these modules not just to provide a consistent interface to outsiders, but to guarantee the correctness of the implementation! Isn’t that the whole point of types? If we can’t do that, why are we using types?

Ok, so in Coq I *can* get the properties I’ve been wanting out of SML’s module system. For instance take the following implementation of the Monad signature:

Module Type MONAD.
Set Implicit Arguments. 

Parameter M : forall (A : Type), Type.
Parameter bind : forall (A B : Type),
  M A -> (A -> M B) -> M B.
Parameter ret : forall (A : Type),
  A -> M A.

Infix ">>=" := bind (at level 20, left associativity) : monad_scope.
Open Scope monad_scope.

Axiom left_unit : forall (A B : Type) (f : A -> M B) (a : A),
  (ret a) >>= f = f a.
Axiom right_unit : forall (A B : Type) (m : M A),
  m >>= (fun a : A => ret a) = m.
Axiom bind_assoc : forall (A B C : Type) (m : M A) (f : A -> M B) (g : B -> M C) (x : B),
  (m >>= f) >>= g = m >>= (fun x => (f x) >>= g).

End MONAD.

This signature describes something much like the monad that is given by the type-class in haskell. I neglected some stuff like implementing join from bind etc, but we can safely ignore that for now. The point is that users of the MONAD signature can’t just fake a monad by supplying an implementation that is nominally the same. i.e. In order to implement this MONAD you actually have to have the right signature for “>>=” *AND* you have to satisfy the monad laws. So what does an implementation look like? Here is an example:

Module ListMonad < : MONAD. 

Require Import List.

Set Implicit Arguments.

Definition M := list.

Fixpoint bind (A : Type) (B : Type) (l : M A) (f : A -> M B) {struct l} : M B :=
  match l with
    | nil => nil
    | h::t => (f h)++(bind t f)
  end.

Infix “>>=” := bind (at level 20, left associativity) : monad_scope.
Open Scope monad_scope.

Definition ret (A : Type) := fun a : A => a::nil.

Lemma left_unit : forall (A B : Type) (f : A -> M B) (a : A),
 (ret a) >>= f = f a.
Proof.
  intros. simpl. rewrite app_nil_end. reflexivity.
Defined. 

Lemma right_unit : forall (A B : Type) (m : M A),
  m >>= (fun a : A => ret a) = m.
Proof.
  simple induction m.
    simpl. reflexivity.
    intros. simpl.
    cut (bind l (fun a0 : A => ret a0) = l).
      intros. rewrite H0. reflexivity.
      exact H.
Defined. 

Lemma bind_assoc : forall (A B C : Type) (m : M A) (f : A -> M B) (g : B -> M C) (x : B),
  (m >>= f) >>= g = m >>= (fun x => (f x) >>= g).
Proof.
  simple induction m.
    intros. simpl. reflexivity.
    intros. simpl.
    cut (l >>= f >>= g = l >>= (fun x0 : A => f x0 >>= g)).
      intros. rewrite < - H0.
      induction (f a).
        simpl. reflexivity.
        simpl. rewrite IHm0. rewrite app_ass. reflexivity.
      apply H. exact x.
Defined.

End ListMonad.

(* Example *)
Import ListMonad.
Require Import Peano.
Require Import List.

Fixpoint downfrom (n : nat) {struct n} : (list nat) :=
  match n with
    | 0 => n::nil
    | S m => n::(downfrom m)
  end.

Eval compute in (1::2::3::4::nil) >>= downfrom.
  = 1 :: 0 :: 2 :: 1 :: 0 :: 3 :: 2 :: 1 :: 0 :: 4 :: 3 :: 2 :: 1 :: 0 :: nil
     : M nat

Ok, That took me about an hour to write. I’m not really that good at using Coq, so presumably you could do this more elegantly and in less time. In any case it would be nice if the proofs could be automated a bit more. That aside this is a *much* better situation than we have in SML and Haskell. We have provided a monad that is guaranteed to actually be one!

I’m of the growing opinion that software that is forced to meet specifications will end up being less trouble in the end than the current state of free-wheeling wild-west style implementation.

Coq gives a civilized alternative to the current free-for-all. Coq can help us make good on the promise that “well typed programs can’t go wrong”.