Djinn, Coq, Monad and a bit of Haskell

Posted by alpheccar - May 24 2007 at 20:37 CEST

Even if your are a beginner in functional programming, you have probably heard of the program-as-proof correspondence, also known as the Curry-Howard isomorphism. It is a bridge between the world of logic and the world of computation.

A type is a specification and a program is a proof of that type. Typechecking is just checking the proof. Types can be used to specify lots of constraints about your programs. With sophisticated type systems like the ones in Ocaml and Haskell you can really do wonderful stuff.

But, those type systems are not powerful enough. We may dream of extracting a program from its specification. But, for that we need to be able to express very rich specifications. It is possible with the calculus of constructions which is the type system implemented in Coq.

First contact with Coq

But, before experimenting with Coq, let's see a simple example of code extraction in Djinn which is a well known tool in the Haskell world. Then, we will compare with the same example in Coq.

Enter the following command in Djinn:

flip ? (a -> b -> c) -> b -> a -> c

You get:

flip :: (a -> b -> c) -> b -> a -> c
flip a b c = a c b

A possible Haskell function for the given type. Now, let's see the same example in Coq. Load the coqtop and enter each of the following lines:

Definition flip : forall (a b c : Set), (a -> b -> c) -> b -> a -> c.
Proof.
tauto.
Defined.

With that kind of simple type, the program can be generated automatically. It is done by the command "tauto" which is using the same method as the one used by Djinn. Now, you can check that the generated code is indeed the same:

Print flip.

And, you should get:

flip = 
fun (a b c : Set) (H : a -> b -> c) (H0 : b) (H1 : a) =>
let H2 := H H1 in let H3 := H2 H0 in H3
     : forall a b c : Set, (a -> b -> c) -> b -> a -> c

Which is the same if you ignore the type information.

To convince you that it is the same, let's ask Coq to generate the Haskell code !

Extraction Language Haskell.
Extraction flip.

And you should get:

flip :: (a1 -> a2 -> a3) -> a2 -> a1 -> a3
flip h h0 h1 =
  h h1 h0

Which is indeed the same.

Coq philosophy

If we want the system to be useful we need to be able to express much more complex types. The calculus of constructions is introducing lot of additional flexibility allowing to:

• Have dependent types. For instance, we may want to define a bitfield type that would depend on a number : the size of the bitfield. Then, bitfield 8 and bitfield 16 would be two different types ;
• Use more complex expressions in a type like a test n < p, or prime n where prime would be a function of type nat -> Prop.

With this flexibility we cannot anymore generate a function from the type in an automatic way. We need to help Coq to build a proof of the type. For that, we use tactics. Tactics are proof generator/transformers that you use to build a proof. You can also look at tactics as program generators/transformers that you use to build a program respecting the specification.

The specifications can be weak or strong. With a weak specification, you write your program and then you prove that it is respecting some constraints which are expressed as theorems but are not encoded in the type of your program.

With a strong specification, the program is not only generating a result n, but also a proof that the result is satisfying a property P n. In that case, the output type of the program is {n : SomeType | P n}. So the function is generating a value and a certificate.

The extraction process will extract the computational part : the value generation and it will forget the certificate one. That's why the flip example has used the sort Set and not the sort Prop or Type. Otherwise the extraction would have returned nothing.

Indeed :

 flip : forall (a b c : Prop), (a -> b -> c) -> b -> a -> c.

Is a function returning a value of type c which is a proposition. So, this flip is building a certificate and not data. The certificate being a proof of the proposition c. The extraction process applied to this type is giving:

flip :: ()
flip =
  __

Now, let's see a real example : a weak specification of the Maybe monad.

Maybe Monad.

First, like in Haskell, we need to define the Monad module (the monad class in Haskell)

Module Type MONAD.
 Set Implicit Arguments.
 Parameter M : forall (A : Type), Type.
 Parameter ret : forall (A : Type), A -> (M A).
 Parameter bind : forall (A B : Type), M A -> (A -> M B) -> M B.

So far, it is looking similar to the Haskell definition. To make the code clearer, let's introduce, inside the module definition, a syntactical improvement:

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

Now ! a great innovation !! : we are able to express the Monad laws inside the Monad module !! Any implementation of the Monad module will have to provide a proof that the Monad laws are satisfied:

 Axiom left_neutral : forall (A B : Type) (f : A -> M B) (a : A), 
   (ret a) >>= f = f a.
 Axiom right_neutral : forall (A B : Type) (m : M A), 
   m >>= (fun a : A => ret a) = m.
 Axiom assoc : forall (A B C : Type) (m : M A) (k : A -> M B)(h : B -> M C),
   m >>= (fun x : A => k x >>= h) = (m >>= k) >>= h.

We can close the module definition.

End MONAD.

Now, let's define a Maybe type. The definition is very similar to the Haskell one:

Inductive Maybe (A:Type) : Type := 
  | Nothing : Maybe A
  | Just : A -> Maybe A.

Now, we are ready to give an implementation of the MaybeMonad. A remark : types are values in the calculus of construction. When I write:

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

I mean that the monad return is taking TWO parameters : a type and a value of that type. But I don't want to have to write : ret nat 4. I prefer to write ret 4 and let Coq infer the value of the type. That's why you see Set Implicit Arguments. in the MaybeMonad definition.

So, we create a new module:

Module MaybeMonad <: MONAD. 
  Set Implicit Arguments.

We specify that the implementation chosen for M is Maybe:

  Definition M := Maybe.

Then we give implementations for the monad return and bind. The definitions are very similar to the Haskell ones:

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

  Fixpoint bind (A : Type) (B : Type) (l : M A) (f : A -> M B) {struct l} : M B :=
  match l with
    | Nothing => Nothing B
    | Just a => f a
  end.

(Fixpoint because in Coq there is a distinction between the recursive and corecursive functions)

A syntax extensions before expressing the monad lwas:

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

The proofs of the monad laws for the Maybe monad. It looks complex but it is because it is essentially interactive. You HAVE to type the tactics in the Coq read-eval-loop to see how the proof is built.

  Lemma left_neutral : forall (A B : Type) (f : A -> M B) (a : A), 
   (ret a) >>= f = f a.
  Proof.
   intros.
   simpl.
   reflexivity.
  Defined.
  
  Lemma right_neutral : forall (A B : Type) (m : M A), 
    m >>= (fun a : A => ret a) = m.
  Proof.
    intros.
    induction m.
     simpl.
      reflexivity.
    simpl.
      auto.
  Defined.
  
  Lemma assoc : forall (A B C : Type) (m : M A) (k : A -> M B)(h : B -> M C),
   m >>= (fun x : A => k x >>= h) = (m >>= k) >>= h.
  Proof.
    intros.
    induction m.
     simpl.
       reflexivity.
    simpl.
      reflexivity.   
 Defined.

End MaybeMonad.

You can't extract a module to Haskell code. It is not yet implemented. But, you can extract the functions :

Extraction Language Haskell.

Extraction MaybeMonad.ret.

ret :: a1 -> Maybe a1
ret a =
  Just a

Extraction MaybeMonad.bind.

bind :: (M a1) -> (a1 -> M a2) -> M a2
bind l f =
  case l of
    Nothing -> Nothing
    Just a -> f a

WARNING : When I am writing on my blog it is often because I am learning something new and because I want to check what is understood. And, trying to explain something is the best way to check if you have understood. Coq is very new to me (one week old). I have attempted to avoid obvious big errors in this post but if you think I have said something wrong then please tell me.

After writing this post, I made a search on Google and found another blog writing about the List Monad in Coq. I borrowed the syntactical trick for >>= from that other blog.

Tags haskell | ocaml | coq | djinn