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.
firstn/skipn is better IMO
std++ uses take/drop like Haskell. Good that OCaml followed suit. So +1 for changing the stdlib.
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.
And ok for keeping firstn/skipn in cList.ml
as this concerns only developers.
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
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.
Yes and my point is "in which case let's do the same as the others"
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.
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