The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

On Sep 14, 2008, at 13:07, Sunil Kothari wrote:
>    I want to use finite maps in my formalization. I have looked at  
> the various implementations of finite maps available in the CoQ  
> library. However,
>  I don't want to restrict my code to any particular implementation.  
> I have a few queries:
>
>   1. In programming languages, we are taught to program against an  
> interface and not to an implementation. Can I formalize by  
> programming against the finite map interface ?  Is there anything  
> wrong in doing so ?
As long as the interface is implementable (which is the case here), I  
think you'll be fine to work against an interface.

>   2. I tried to import the finite map interface  but none of the  
> interface definitions are available in the CoqIde. However, if I  
> import a particular implementation, all the definitions (in that  
> particular implementation) are visible in the CoqIde. Is that  
> intentional ?

I'll leave it to the implementers of Coq to speak on whether that is  
intentional or not.  In the meantime, here are two idioms that should  
let you do what you want.  (I haven't tried this code myself, but  
hopefully it conveys the idea.)

Idiom #1: Do everything in a functor.  For example,

<<
Module Foo (X : FMapInterface.S)

        (* Here, you know that you have some module
           X satisfying the interface, but you have
           no information about how it's implemented. *)

End Foo.
>>

Idiom #2: Use the signature to hide the details of the implementation.

<<
Module SomeFMapImpl : FMapInterface.S with E := Foo :=
  FMapList.Make Foo.
>>

The ": FMapInterface.S with E := Foo" is key.  Without it, you'll be  
able to see the gory details of the implementation.  With it, you'll  
know only what FMapInterface.S reveals.

Cheers,
Brian