Enrico Tassi (Feb 23 2022 at 21:19): Enrico Tassi (Feb 23 2022 at 21:19):Here a "doodle", please fill in by Friday 5PM Paris time, so that I can announce the date here before W.E.:
https://framadate.org/NCcsXegnmPy57Xwu
Enrico Tassi (Feb 23 2022 at 21:22):CC @Paolo Giarrusso (I don't know how many colleagues of yours read this stream, if they don't please tag them here)
Paolo Giarrusso (Feb 23 2022 at 21:56):Cc @Gregory Malecha @Gordon Stewart @David Swasey @David Swasey
Enrico Tassi (Feb 28 2022 at 21:41):I forgot to announce the best date, it is "Thursday, March 3, 2022 - 2PM (Paris time)"
(4PM has the same votes, but I prefer 2PM, if you don't mind)
Enrico Tassi (Mar 01 2022 at 10:05):It would be nice if a kernel maintainer could attend (CC @Gaëtan Gilbert @Maxime Dénès @Pierre-Marie Pédrot ).
Pierre-Marie Pédrot (Mar 01 2022 at 10:09):I should be there.
Enrico Tassi (Mar 03 2022 at 12:56):https://rendez-vous.renater.fr/coq-engineering
Karl Palmskog (Mar 03 2022 at 13:10):not going to participate in the WG, but I hope I can make one comment: please distinguish between interfaces and their semantics on one hand, and implementation aspects such as separate compilation on the other. In my view, the title of CEP 62 is really misleading
Paolo Giarrusso (Mar 03 2022 at 13:14):@Karl Palmskog "separate compilation" is a semantic concept by Cardelli; even if arguably it's a questionable name, it's standard.
Karl Palmskog (Mar 03 2022 at 13:16):SML modules/functors/signatures is to me the standard of any kind of interfaces, and SML '97 does to my knowledge not even specify anything about compilation.
Paolo Giarrusso (Mar 03 2022 at 13:19):@Karl Palmskog well, http://portal.acm.org/citation.cfm?doid=1159876.1159883 adds separate compilation to Standard ML
Paolo Giarrusso (Mar 03 2022 at 13:20):authors include both "core SML people" (Karl Crary, Robert Harper), and David Swasey who's coauthoring the CEP
Enrico Tassi (Mar 03 2022 at 15:34):Here the toy: https://github.com/gares/coq-defunctor
Paolo Giarrusso (Mar 03 2022 at 22:58):in later discussion, we realized that using opaque ascription (as in Module A : A.interface.) is not strictly necessary, since clients aren’t importing the implementation files. Using Module A <: A.interface. gets closer to the opt-in ascription that @Jason Gross was suggesting.
Paolo Giarrusso (Mar 03 2022 at 23:06):The downside is that Cardelli's "separate compilation" guarantee, or rather the "compositional typechecking" one, is only as good as the import discipline. C++ friend declaration arguably have better ergonomics.
Notification Bot (Mar 04 2022 at 07:17):Enrico Tassi has marked this topic as resolved.
Notification Bot (Mar 04 2022 at 07:17):Enrico Tassi has marked this topic as unresolved.
Enrico Tassi (Mar 04 2022 at 07:19):Paolo Giarrusso said:
in later discussion, we realized that using opaque ascription (as in
Module A : A.interface.) is not strictly necessary, since clients aren’t importing the implementation files. UsingModule A <: A.interface.gets closer to the opt-in ascription that Jason Gross was suggesting.
Indeed. A single file coud implement even two interfaces in one go. This suggests that the link command needs to address more than a 1:1 relation
Paolo Giarrusso (Mar 04 2022 at 08:30):You can already combine module types via Include/<+, and this is somewhat extensively tested by Coq's numeric library.
Paolo Giarrusso (Mar 04 2022 at 08:39):But in general, even if I argued for automatically doing the translation or enforcing it, there are indeed cases needing a more flexible "source language"; so we should just use Link directly, and encode any rules we'd like in a linter.
Paolo Giarrusso (Mar 04 2022 at 08:40):linting infrastructure is also needed, but it'd be a separate discussion
Maxime Dénès (Mar 04 2022 at 08:51):Depending on what you call linter, my current work on having a separate parsing phase for the vernacular language may help. Namely if the linting is done on static criteria that does not require execution.
Last updated: Sep 09 2024 at 05:02 UTC