The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

(I only referred to the Require handling below when I said "module system", 
but
probably should have used more precise terminology.
I think the rest of the module system is rather hard to use well [for someone
with basically no OCaml or SML background], but much of that is because Coq
resources usually don't teach you how to use it properly -- with the benefit 
of
hindsight I think I would know better now how to design a library that
profitably uses the Coq module system. Oh and there's the problem that Coq is
very stateful so import order matters a lot, but I doubt that part is 
inherited.)

; Ralf

On 18.09.20 16:54, Andrew Appel wrote:
> Oops, let me clarify.
> 
> The sloppiness of Require paths, which is the subject of this thread, has
> bothered me for years.  That's the +1.
> 
> Regarding the Coq module system -- I love the Coq module system, which is 
> based
> on the OCaml module system, which is based on the Standard ML module 
> system, a
> landmark achievement in computer science developed primarily by David 
> MacQueen
> between 1984 and 1995, with contributions from Mads Tofte and Xavier Leroy.
> 
> -- Andrew
> 
> 
> --------------------------------------------------------------------------------
> 
>     *From: *"appel" <appel AT princeton.edu>
>     *To: *"coq-club" <coq-club AT inria.fr>
>     *Sent: *Friday, September 18, 2020 10:50:00 AM
>     *Subject: *Re: [Coq-Club] option to disable partially qualified Require 
> Imports
> 
>     +1
> 
>     
> --------------------------------------------------------------------------------
> 
>         *From: *"Ralf Jung" <jung AT mpi-sws.org>
>         *To: *"coq-club" <coq-club AT inria.fr>, "Guillaume Melquiond"
>         <guillaume.melquiond AT inria.fr>
>         *Sent: *Friday, September 18, 2020 10:46:09 AM
>         *Subject: *Re: [Coq-Club] option to disable partially qualified 
> Require
>         Imports
> 
>         Seriously though, I do not understand this attitude.  No other 
> language
>         that I
>         know of has a module system as strange as Coq's (maybe this is 
> inherited
>         from
>         OCaml?), and yet you claim that it's the library author's fault for 
> not
>         taking
>         care in designing their library to work around this quirk, rather 
> than the
>         language designer's fault for having designed something strange.
>          (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.)
> 
>         This is not about malicious users, it is about people coming to Coq 
> with
>         what I
>         consider reasonable expectations having their code break for reasons
>         that are
>         really hard to figure because Coq violates assumptions formed when 
> learning
>         pretty much any other language. Even the notoriously sloppy 
> JavaScript
>         requires
>         precise imports! I still remember my surprise when I learned about 
> "-R"
>         semantics... it remains a mystery to me how it seemed like a good 
> idea
>         to just
>         recursively slap everything into the global namespace. And then when
>         "From ...
>         Require" was introduced I was very surprised to learn about its path
>         matching
>         semantics, I had not even realized that regular "Require" was not 
> doing
>         full-path matching either. For what is otherwise a system that is 
> extremely
>         picky about which terms it accepts (for good reasons!), this stands 
> out
>         like a
>         sore thumb.
> 
>         There probably is a reasonable explanation for this. But dismissing 
> the
>         concern
>         as only affecting "dumb" users is not reasonable.
> 
>         Kind regards,
>         Ralf
> 
> 

-- 
Website: https://people.mpi-sws.org/~jung/