CoqExtraction/LetouzeyOverview/3

#3 Examples beyond ML type system

All our experiments on dening and extracting a division algorithm lead to legitimate Ocaml (or Haskell) code. But the type system of Coq allows us to build objects that have no counterparts in Ocaml nor Haskell. In this case, the type-checkers of these systems are locally bypassed by unsafe type casts (Obj.magic or unsafeCoerce). These unsafe type casts are now automatically inserted by the extraction in the produced code. We present now two of the various situations where such type casts are required.

##3.1 Functions of variable arity

In Coq, a type may depend on an object such as a number. This allows us to write the type nArrow of n-ary functions (over nat), such that nArrow 0 = nat and nArrow 1 = nat -> nat and so on.

Fixpoint nArrow n : Set := match n with
| O => nat
| S n => nat -> nArrow n
end.

Furthermore, we can write a function nSum whose rst parameter determines the number of subsequent parameters this function will accept (and sum together):

Fixpoint nSum n : nArrow (S n) :=
  match n return nArrow (S n) with
  | O => fun a => a
  | S m => fun a b => nSum m (a+b)
  end.

Eval compute in (nSum 2) 3 8 5.

The example (nSum 2) expects (S 2) = 3 arguments and computes here 3+8+5=16. Without much of a surprise nSum cannot be typecheked in ML, so unsafe type casts are inserted during extraction:

let rec nSum n x =
  match n with
  | O -> Obj.magic x
  | S m -> Obj.magic (fun b -> nSum m (plus x b))

##3.2 Existential structures

Another situation is quite common in developments on algebra: records can be used in Coq to define structures characterized by the existence of various elements and operations upon a certain type, with possibly some constraints on these elements and operations. For instance, let’s define a structure of monoid, and show that (nat,0,+) is indeed a monoid:

Record aMonoid : Type :=
 { dom : Type;
   zero : dom;
   op : dom -> dom -> dom;
   assoc : forall x y z:dom, op x (op y z) = op (op x y) z;
   zerol : forall x:dom, op zero x = x;
   zeror : forall x:dom, op x zero = x }.

Definition natMonoid :=
  Build_aMonoid nat 0 plus plus_assoc plus_0_l plus_0_r.

Proofs concerning monoids can then be done in a generic way upon an abstract object of type aMonoid, and be applied to concrete monoids such as natMonoid. This kind of approach is heavily used in CoRN development at Nijmegen. For the point of view of extraction, this aMonoid type hides from the outside the type placed in its dom field. Such dependency is currently translated to unsafe cast by extraction:

let natMonoid =
  { zero = (Obj.magic O); op = (Obj.magic plus) }

In the future, it might be possible to exploit recent and/or planned extensions of Haskell and Ocaml type-checkers to allow a nicer extraction of this example. Considering Haskell Type Classes and/or Ocaml’s objects might also help.