The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 13/02/2012 16:23, Andrej Bauer a écrit :
> [...] Let me first say why I think that in
> principle it should be possible to extract more than Coq currently
> does. Coq uses a typed realizability model (a.k.a. modified
> realizability, but that's a really awful name) to extract terms from
> proofs. [...]

The extraction currently in Coq does not use a typed realizability model.

The only type-theoretic thing that is checked during extraction of a
(sub)term (remember that proofs are represented as CIC terms) is Prop
membership of its type, to decide whether to keep it in the extracted
version. Once the decision is made, all types are forgotten and the term
is syntactically (and recursively) transformed, or replaced with __. The
target language remains pretty abstract at this stage; for example, it
has reduction rules for __ (beta-like and iota-like).

Then, some of the __ are removed (it is not correct to remove blindly
all of them). When universe polymorphism is not used, it seems that only
the beta-like reduction for __ (i.e. __ t ---> __) is needed, which can
be implemented in the runtime of target languages.

When the target language is OCaml or Haskell, types are added back, in a
third phase, on a best-effort basis. The Obj.magic (or unsafeCoerce)
appearing are part of this best-effort; no cheating on theoretical
isomorphisms should be seen there.

I'm not saying that all this could not be related to your way of
presenting extraction, but I don't consider your way the "primary" one,
as you seem to assert.

The philosophy of Coq's extraction is to rely on Coq for type-checking,
and on the target language for execution. OCaml- or Haskell- level
type-checking is an additional bonus, but not an initial goal in the design.


Cheers,

-- 
Stéphane