Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Issues regarding use of finite map interface (FMapInterface)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Issues regarding use of finite map interface (FMapInterface)


chronological Thread 
  • From: Brian Aydemir <baydemir AT cis.upenn.edu>
  • To: Sunil Kothari <skothari AT uwyo.edu>
  • Cc: <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Issues regarding use of finite map interface (FMapInterface)
  • Date: Sun, 14 Sep 2008 14:14:40 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page