The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

On 19/9/20 1:01 am, Guillaume Melquiond wrote:
> Le 18/09/2020 à 16:46, Ralf Jung a écrit :
> > (Probably the
> > language designer had a good reason and this was solving a concrete problem, 
> > but
> > putting the blame on the library is just unfair. And you haven't argued for 
> > why
> > Coq's semantics make any sense, either.)
> The reason is the standard library of Coq. It is important to understand
> how painful it would be to use if Imports had to be fully qualified.
> Here is a quiz for you. Which of the following are correct?
>
> 1.a Require Coq.List.List.
> 1.b Require Coq.Lists.List.

If the Coq module system really were based to a significant extent on 
the SML module system, surely the answer would be both are correct, with 
a trivial amount of extra code.  I think the code would look something 
like this

structure Coq = struct
  structure List = struct
    <the stuff in List>
  end ; (* structure List *)
  structure Lists = List ;
(* or, if that does more than you want
  structure Lists = struct
    structure List = List.List ;
  end ; (* structure Lists *)
end ; (* structure Coq *)

One of the problems, as I understood it (accepting that it seems so 
bizarre that I might well be mistaken) is that to compile a Coq source 
file, you have to know where in the logical hierarchy of logical paths 
it is going to be used.  Which is certainly not something I've 
experienced in 25 years using SML (though this, admittedly, would 
potentially vary between SML implementations).

Jeremy