CoqExtraction/LetouzeyOverview/4

#4 Key features of extraction

Let us summarize now the current status of Coq extraction. The theoretical extraction function described in 7 is still relevant and used as the core of the extraction system. This function collapses (but cannot completely remove) both logical parts (living in sort Prop) and types. A complete removal would induce dangerous changes in the evaluation of terms, and can even lead to errors or nontermination in some situations. Terms extracted by this theoretical function are untyped λ-terms with inductive constructions, they cannot be accepted by Coq in general, nor by ML-like languages. Two separate studies of correctness have been done for this theoretical phase.

The correctness of this theoretical phase is justied in several steps. First, we prove that the reduction of an extracted term is related to the reduction of the initial term in a bisimulation-alike manner (see 7 or Sect. 2.3 of 8. Since this rst approach is really syntactic and cannot cope for instance with the presence of axioms, we then started a semantical study based on realizability (see Sect. 2.4 of 8). Finally, dierences between theoretical reduction rules and the situation in real languages have been investigated, especially in the case of Haskell (see Sect. 2.6 of 8).

Even if the actual implementation of the extraction mechanism is based on this theoretical study, it also integrates several additional features. First, the untyped λ-terms coming from the theoretical phase are translated to Ocaml, Haskell or Scheme syntax. In addition, several simplications and optimizations are performed on extracted terms, in order to compensate the frequent awkward aspect of terms due to the incomplete pruning of logical parts. Indeed, complete removal of proof parts is often unsafe. Consider for instance a partial application of the div function of section 2.5, such as div 0 0 : 0<>0 -> nat. This partial application is quite legal in Coq, even if it does not produce much, being blocked by the need of an impossible proof of 0<>0. On the opposite, an extraction that would brutally remove all proof parts would produce div 0 0 : nat for this exemple, leading to an innite computation. The answer of our theoretical model of extraction is to be very conservative and produce anonymous abstractions corresponding to all logical preconditions such as this Hy:y<>0. The presence of these anonymous abstractions permits a simple and safe translation of all terms, including partial applications. At the same time, dangerous partial applications are quite rare, so our actual implementation favors the removal of these anonymous abstractions, at least in head position of extracted functions, leading here to the expected div of type nat!nat!nat, whereas a special treatment is done for corresponding partial applications: any occurrences of div 0 0 would become fun _ -> div 0 0, preventing the start of an innite loop during execution.

Moreover, the extraction embeds an type-checker based on 5 whose purpose is to identify locations of ML type errors in extracted code. Unsafe type cast Obj.magic or unsafeCoerce are then automatically inserted at these locations. This type-checking is done accordingly to a notion of approximation of Coq types into ML ones (see Chap. 3 of 8). In addition, Coq modules and functors are supported by the Ocaml extraction, while coinductive types can be extracted into Ocaml, Haskell or Scheme.