RFC: Making naming in the standard library consistent

[ahmadsalim]

As an extension to the mail I sent to the mailing list, I am now gathering together all type constructors and data constructors with inconsistent naming and listing them here in a table with suggested fixes.

Package prelude:

Module	Current name	Suggested name	Note	Action
built in	()	Unit	allow both versions	both accessible
built in	()	MkUnit	allow both versions	both accessible
built in	refl	Refl		renamed
built in	(a , b)	Pair a b	allow both versions	both accessible
built in	(a , b)	MkPair a b	allow both versions	both accessible
built in	|	Void	allow both versions	renamed, only Void accessible
Builtins	FalseElim	VoidElim		renamed to void, which is the only version accessible
Builtins	Sg_Into	MkSigma		renamed
Bool	so	So		renamed
Bool	oh	Oh		renamed
Pairs	evidence	Evidence		renamed
Pairs	element	Element		renamed
Fin	fZ	Z	alternatively FZ	renamed to FZ
Fin	fS	S	alternatively FS	renamed to FS
Nat	lteZero	Z	alternatively LTEZero	renamed to LTEZero
Nat	lteSucc	S	alternatively LTESucc	renamed to LTESucc
Nat	cmpLT	CmpLT		renamed
Nat	cmpEQ	CmpEQ		renamed
Nat	cmpGT	CmpGT		renamed

Package base:

Module	Current name	Suggested name	Note	Action
Decidable.Order	nEqn	Z	or merge with LTE.Z	merged with LTE equivalent
Decidable.Order	nLTESm	S	or merge with LTE.S	merged with LTE equivalent
System.Concurrency.Process	lift	Lift		renamed
IdrisNet.Socket	AF_UNSPEC	Unspecified	keep C name	none
IdrisNet.Socket	AF_INET	IPv4	keep C name	none
IdrisNet.Socket	AF_INET6	IPv6	keep C name	none

[ahmadsalim]

@edwinb I am unsure if you want to keep the conventions in the effect package, but I could suggest new conventions if you are interested.

[ahmadsalim]

If anyone sees that I have missed something, please add a comment.
Thank you.

[JanBessai]

Since it was mentioned:
There is also an overlap between LTE and NatLTE.
They are essentially the same, but latter is tailored to fit the order theoretic constructs from earlier in the file and allows easy lifting to Fin via injectivity. Its constructors would also have to be renamed though.

[david-christiansen]

Thanks for being so systematic!

Personally, I am in favor of some of these, but not all of them. I like the idea of capitalizing the currently-lowercase constructor and type names, and I think it's worth seeing if renaming the Fin constructors from FZ and FS to Z and S is sufficiently easy for the elaborator to figure out. I suspect that it might get irritating at the REPL, but that's just a guess.

Giving the product and unit constructors user-accessible names might be useful. I've certainly wanted to use them that way. For some reason MkUnit rubs me the wrong way, but it is consistent, which is nice.

I don't think prim__IO should be renamed. It's a scary internal thing, so it should follow the convention of other scary internal things in my opinion.

The names in the sockets lib come from the underlying C API, don't they? If so, I think we should leave them be, for the sake of familiarity.

[jfdm]

Just a +1 on this. I see no real problems with the suggestions.

I somewhat agree with @david-christiansen's stance on the naming of sockets lib. It is a good idea to keep them as is for familiarity; the socket names have been directly lifted from the underlying C implementation. However, I also think that the alternatives are sufficient enough to warrent a change. Note that the list for socket names is incomplete, and there is another field IIRC.

Also I think internals should be kept as scary as possible. It makes them standout easierly.

[ahmadsalim]

OK, I will update the table accordingly.
Thank you for the feedback.

[david-christiansen]

I vote "do it now", if @edwinb doesn't have any objections. Perhaps we can do this, then get a release out, and given that we don't have a migration warnings system, just eat the temporary support overhead?

[ahmadsalim]

@david-christiansen I am trying to do it, but unfortunately I am having issues with the renaming.
Perhaps, we should take a look at it together when you have time.

[ahmadsalim]

How would people feel if I made _|_ accessible as Void, similar to the others.

[ahmadsalim]

Also FalseElim as VoidElim to match.

[david-christiansen]

I'm not a fan of changing _|_ like that, TBH, at least not in this way. It's nice to have an accessible constructor for pairs, because tuple sections would make the language insane and \x:Nat ->(Z, x) is not equal to the (Nat -> (Nat, Nat)) (MkPair Z) due to the lack of eta. It also makes it a bit easier to do some kinds of proof automation, because we can write Refine "MkPair".

These things don't seem to be the case for _|_. It's a bit difficult to type, and I would have nothing against following the Haskell lead and just renaming it to Void, but having two names for it seems a bit excessive.

[ahmadsalim]

Updated the table with corresponding action.
Everything is pretty much resolved except the issue with _|_, which I personally do not find that important again.

[Melvar]

Huh, but LTE and NatLTE are not the same – they can be proven equivalent, but the former is a prefix and the latter a suffix representation, with correspondingly different recursion patterns.

[ahmadsalim]

Melvar: I have reproven everything for LTE

[edwinb]

As far as I can tell, this is all done now. Can I close this?

[ahmadsalim]

Yes, sure. I will close this issue.