coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Christopher Ernest Sally <christopherernestsally AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Incompatible Module Types
- Date: Sat, 14 Jun 2014 00:01:17 +0800
Hmm,
For Records vs classes vs Modules, I have heard that argument quite a few times, but our prjt requires modules...
"Module Import. End Import." doesn't work, but it is a valid name for a Module Type. I suppose because as module name it could clash, but not as a module type. (because the "Import" would always be to the left of the colon, while types to the right)
Ah, fortunately the issue has been resolved. (see my second example: module_eg.v) It was necessary in the standard library because they often build weak versions of sets/maps first, without the keys being members of Orders.OrderedType. Now that I understand that better (or at least am getting my script to type check, which in some contexts is almost as good as understanding ;) )
Warm regards
Chris
On 13 June 2014 15:18, Cedric Auger <sedrikov AT gmail.com> wrote:
Ok, I was not aware of the Import feature. I still find it a weird place to have it, as it can be mistaken with what I thought it was.
I do not have Coq under my hand here, so I cannot test if "Module Import. End Import." is also rejected, but I guess it is.
The Coq site seems down for now, but as far as I remember, there is a 'with' annotation for module types which can be useful for you (read the documentation on modules when documentation becomes available back).
Clearly in your original example, at no point you made it clear to Coq that in your Implementation module, "ht = list …". You may not require to put it in your A module but in this case as Beta said, but in this case you will probably need to use intermediate parametric modules.
I also suggest to take a look on Record/Class alternatives. In Ocaml and many other languages, types are not first class citizens, so you need stuff like modules to manipulate them. In Coq, types are regular values, so you can put them inside of regular records, and I find it often a lot more convenient than using the module mechanism, and I find it also a lot easier to learn/read/write/understand. (Still there are cases where you do not have much choice, e.g. when you want to use a Coq library using modules.)
2014-06-13 1:16 GMT+02:00 Christopher Ernest Sally <christopherernestsally AT gmail.com>:Hi Cedric
Oh, you mean like forall (x y : nat) etc etc? Then both x and y are nats?
Yes, that is what I meant, but the remaining part of your mail shows me that I was wrong.
What I meant in the previous email is that the import would allow us to have the variables, k v and m, which would serve as abstract types for Interface', but still allow us to make them concrete later in Interface. (but _how_ that works, I'm not sure)
I don't quite understand how Import works, but if I run this script
Module Type A.
Parameter a : Type.
End A.
Module Type B (T: A).
Check T.a.
(*Check Import.a. *) (* Error: The reference Import.a was not found in the current environment. *)
(*Parameter x : a.*)(*Error: The reference a was not found in the current environment.*)
End B. Print Module Type B.
Module Type C (Import T: A).
Parameter x : a.
End C. Print Module Type C.
Module Type D (Import : A). (*Gives an error. Seems "Import" is reserved *)
"Import" as a module doesn't seem to show up in C. And while one can "Check" T.a in both B & C, you can only use it in C.
Warm regards
Chris
--
.../Sedrikov\...
- [Coq-Club] Incompatible Module Types, Christopher Ernest Sally, 06/04/2014
- Re: [Coq-Club] Incompatible Module Types, Beta Ziliani, 06/04/2014
- Re: [Coq-Club] Incompatible Module Types, Christopher Ernest Sally, 06/11/2014
- Re: [Coq-Club] Incompatible Module Types, Cedric Auger, 06/11/2014
- Re: [Coq-Club] Incompatible Module Types, Christopher Ernest Sally, 06/13/2014
- Re: [Coq-Club] Incompatible Module Types, Cedric Auger, 06/13/2014
- Re: [Coq-Club] Incompatible Module Types, Christopher Ernest Sally, 06/13/2014
- Re: [Coq-Club] Incompatible Module Types, Cedric Auger, 06/13/2014
- Re: [Coq-Club] Incompatible Module Types, Christopher Ernest Sally, 06/13/2014
- Re: [Coq-Club] Incompatible Module Types, Cedric Auger, 06/11/2014
- Re: [Coq-Club] Incompatible Module Types, Christopher Ernest Sally, 06/11/2014
- Re: [Coq-Club] Incompatible Module Types, Beta Ziliani, 06/04/2014
Archive powered by MHonArc 2.6.18.