The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Fri, 10 Feb 2012 21:56:25 +0100,
Andrej Bauer 
<andrej.bauer AT andrej.com>
 a écrit :

> Since we are on this topic, can someone please explain to me why Coq
> even bothers with the ugly Obj.t and __? Why not just delete the
> irrelevant stuff instead of dragging it along? My reasoning would be:
> things outside of Set cannot be computed with, so we convert them all
> to unit. We did something like that in RZ.
> 
> With kind regards,
> 
> Andrej

For an easy answer, how would you extract something like:

Fixpoint sum_type (n:nat) : Type :=
 match n with
 | O => nat
 | S m => nat -> (sum_type m)
 end.

Fixpoint sum (n:nat) : nat -> sum_type n :=
 match n with
 | O => fun x => x
 | S m => fun x y => sum m (x+y)
 end.
------------------------------------------
number of terms to add (minus one)
    ↓
sum 0 = λ x · x
sum 0 4 = 4
sum 1 = λ x y · x+y
sum 1 2 = λ x · 2+x
sum 1 6 8 = 14
...

(I didn't tried it, so you may have to patch it to make it working.)

Coq type system is too powerfull to be nicely translated in Ocaml,
Haskell or Scheme.

In particular, sum cannot be typed, since its type depends on a term.
So it is not "irrelevant" (even if some "wrong" ocaml warning tells you
the contrary on the extracted term).

If I well understood, extracting "sum" would give you a "unit->unit",
but extracting "sum 1" would give you a "fun x y -> x+y" with probably
high probabilities that your extracted program won't even type check.

The question I originally asked is also a good counter example.

Record disjunction {A:Type} : Type :=
 { producer : forall (B:Type), B -> B -> A -> B }.

Definition or_bool : disjunction bool :=
 {|producer := fun B iftrue iffalse b =>
               if b then iftrue else iffalse
 |}.

This could (should?) be extracted into:

type 'a disjunction = {producer:'b.'b->'b->'a->'b}
let or_bool = {producer = fun x y z -> if z then x else y}

but as Adam said (if I well understood), there is another way to write
it:

Record disjunction {A:Type} : Type :=
 { producer : A -> forall (B:Type), B -> B -> B }
 (*just changing the place of A*).

Definition or_bool : disjunction bool :=
 {|producer := fun b B iftrue iffalse =>
               if b then iftrue else iffalse
 |}.

which we would like to be extracted as:

type 'a disjunction = {producer:'a->'b.'b->'b->'b}
let or_bool = {producer = fun z x y -> if z then x else y}

but this is not valid ocaml code as terms should be in prenex form
(you cannot have an existential under an arrow; that is the "producer"
field must have a form: ∀ x1..xn· ∃ y1..ym· <unquantified term> if
ocaml allowed to see fields as functions).

Nonetheless for my first post in this thread, I think that extracting
to the "'a.…" would be interesting, since people playing with
extraction should often have in mind the extracted term, so that they
should write their coq code in such a fashion that it could be cleanly
extracted.

I guess that a not worthy choice to manage what Adam said, is to
have:

type ex_producer = {ex_producer_aux : 'b.'b->'b->'b}
type 'a disjunction = {producer:'a->ex_producer}
let or_bool =
 {producer = fun b -> {ex_producer_aux = fun x y -> if b then x else y}}

This way it would replace and not type safe a not pretty __ (not type
safe in regards of the way the user will use it, but the extracted code
itself is type safe), with a fully type safe system (even for the user)
but way too much ugly. So if I ever write a patch, it would only be for
the natural part (ie. for prenexes formulas).