Moving Data.List.HasLength into base #2844
Conversation
|
@gallais i thought you might have an opinion about the (re-)ordering of the parameters on the If you don't have an opinion or objection, I will merge this soon. |
| ||| f1 : (n : Nat) -> (0 _ : HasLength xs n) -> P xs | ||
| ||| f2 : (n : Subset n (HasLength xs)) -> P xs | ||
| ||| f1 : (n : Nat) -> (0 _ : HasLength n xs) -> P xs | ||
| ||| f2 : (n : Subset n (flip HasLength xs)) -> P xs |
There was a problem hiding this comment.
I'd say it can be written (`HasLength` xs) but the punning does not work anymore with the new argument order. 😅
There was a problem hiding this comment.
It risks being obvious, but "xs does have a length" ;)
There was a problem hiding this comment.
Oh, I think I see what you mean. xs HasLength n used to read well.
Maybe HasLength n xs should have been named IsLength to remain reminiscent of English. I wouldn't vote for renaming now, though.
|
Shouldn't the TODOs say |
|
@clayrat The todos say “after 0.6.0” which was my intention in this case, whether that’s 0.6.1 or 0.7.0 or 1.0.0 |
Per the conclusion documented in https://github.com/idris-lang/Idris2/wiki/%5BLanguage%5D-Contrib-Organisation,
Data.List.HasLengthis being moved into the base library and removed from the contrib library.With the move, I took the liberty of adopting some naming from contrib that I liked (will result in small refactoring of the compiler library after the next release of the base library). I also took the liberty of adopting the type signature from the compiler as opposed to the one in contrib (they take parameters in reverse-order from each other). I figured the compiler codebase represented the more real-world use-case and gave the ergonomics that have worked well for the compiler codebase the win on this one.
As a side note, I would have loved to have used the
%deprecatefeature in the compiler codebase for the functions that will be removed next version, but we have warnings-as-errors turned on for the compiler build process (which is good) so we cannot produce deprecation warnings in that codebase!I've sanity checked that removing all of the functions marked for removal after the next release will work by deleting them and building the Idris compiler locally against the new base library
HasLength.Should this change go in the CHANGELOG?
CHANGELOG.md(and potentially alsoCONTRIBUTORS.md).