Stream: Coq devs & plugin devs

Topic: firstn/skipn vs take/drop


view this post on Zulip Hugo Herbelin (Aug 30 2024 at 08:58):

Hi, wishing summer went well!

I see that OCaml 5.3 will introduce functions List.take and List.drop. The Coq file cList.ml seems to be relatively isolated in using the names firstn and skipn. Shall we consider a renaming to take/drop (as in Haskell, Scala and now OCaml)?

Regarding Coq libraries, List.firstn and List.skipn were following clib/cList.ml. These names are used in ext-lib but std++ and math-comp use take/drop. See PR #19478.

view this post on Zulip Gaëtan Gilbert (Aug 30 2024 at 09:09):

firstn/skipn is better IMO

view this post on Zulip Robbert Krebbers (Aug 30 2024 at 15:01):

std++ uses take/drop like Haskell. Good that OCaml followed suit. So +1 for changing the stdlib.

view this post on Zulip Hugo Herbelin (Aug 30 2024 at 15:28):

I personally find (also) that firstn/skipn more explicitly express what they do than take/drop, but indeed, if all of OCaml, Haskell and Scala already opted for take/drop that's probably worth to follow the move. Alternatively, since we won't be able to avoid eventually supporting synonyms, we can also support both pairs of names.

view this post on Zulip Hugo Herbelin (Aug 30 2024 at 15:29):

And ok for keeping firstn/skipn in cList.ml as this concerns only developers.

view this post on Zulip Thomas Lamiaux (Aug 30 2024 at 17:22):

imho, at the end of the day it is just a question of habit so we may as well try to be uniform, it will also make the code more transparent when switching between Coq's implem and working with coq

view this post on Zulip Hugo Herbelin (Aug 30 2024 at 17:44):

Just a question of habits, but there are many different relatively equivalent ways to be uniform and the question of which rules to apply to take uniformity decisions is notoriously difficult. Even probably the most difficult question in living together.

view this post on Zulip Thomas Lamiaux (Aug 30 2024 at 18:12):

Yes and my point is "in which case let's do the same as the others"

view this post on Zulip Théo Winterhalter (Aug 30 2024 at 23:51):

While drop works, take doesn't really convey the idea I think. We should only make a change if it makes sense (ie, the name should convey as best as possible what it represents). Here, it's debatable so keeping both might be the best option.

view this post on Zulip Tomás Díaz (Sep 02 2024 at 21:53):

I always get confused when seeing firstn or skipn thinking that it's g-dropping, as in "hangin there", "walkin' the dog", etc. So basically I read it as "firsting" or "skiping". Might be just me though.


Last updated: Oct 13 2024 at 01:02 UTC