The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Dear Coq-Club:

I'm trying to specify an object-oriented framework as a Coq typeclass. 

The typeclass has fields of type Set that I'd expect to be extracted as generic type parameters, and some fields of function types. As in an object-oriented framework, some of these function-valued fields have implementations in the typeclass, to capture functionality shared across all instances of the framework. I'd expect these to be extracted as fields with function implementations as values. Other function-valued fields of the typeclass are not given values. I'd expect these to be extracted as function-valued parameters that need to be initialized.

Clearly I don't yet fully understand Record/Typeclass extraction in Coq. Consider the following very simple example.

== START EXAMPLE === 

Extraction Language Haskell.

Class Foo := {

    ftp: Set

  ; fcfn (t: ftp): ftp := t 

  ; fafn (t:  ftp): ftp. 

}.

Extraction Foo.

=== END EXAMPLE

Here's the extracted code

=== START EXTRACTED CODE

...

type Foo =

  () -> ()

  -- singleton inductive, whose constructor was Build_Foo

=== END EXTRACTED CODE

What's the problem? We'll the generic/type parameter ftp has completely disappeared in the extracted code, as has the function fcfn (a function with a provided implementation). The only thing remaining in the extracted code is a signature for fafn, a function field without a value defined in the typeclass.

Questions: Why is the extraction procedure erasing these fields? What am I not understanding about extraction? Is there something simple that I'm missing that, if done, would produce extracted code that's at least closer to what I'm expecting?

Thanks!

Kevin